diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 26c6cc02..55138a3f 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -80,6 +80,11 @@ Inductive instruction : Type := | Pwfxl (n: int) (src: ireg)
| Pwfxm (n: int) (src: ireg)
| Pldu (dst: ireg) (addr: ireg)
+ | Pawait
+ | Psleep
+ | Pstop
+ | Pbarrier
+ | Pfence
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
|