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 a9a88d75..f679335c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -80,6 +80,9 @@ Inductive instruction : Type := | Pwfxl (n: int) (src: ireg)
| Pwfxm (n: int) (src: ireg)
| Pldu (dst: ireg) (addr: ireg)
+ | Plbzu (dst: ireg) (addr: ireg)
+ | Plhzu (dst: ireg) (addr: ireg)
+ | Plwzu (dst: ireg) (addr: ireg)
| Pawait
| Psleep
| Pstop
@@ -94,6 +97,8 @@ Inductive instruction : Type := | Pdzerol (addr: ireg)
| Pafaddd (addr: ireg) (incr_res: ireg)
| Pafaddw (addr: ireg) (incr_res: ireg)
+ | Palclrd (dst: ireg) (addr: ireg)
+ | Palclrw (dst: ireg) (addr: ireg)
(** Loads **)
| Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
|