diff options
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index b22ea100..cf7d1ef1 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -98,6 +98,7 @@ Inductive instruction : Type := | Pcvtl2w (rd rs: ireg) (**r Convert Long to Word *)
| Psxwd (rd rs: ireg) (**r Sign Extend Word to Double Word *)
| Pzxwd (rd rs: ireg) (**r Zero Extend Word to Double Word *)
+ | Pfloatwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer *)
(** Arith RI32 *)
| Pmake (rd: ireg) (imm: int) (**r load immediate *)
@@ -194,6 +195,7 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmblock.Psxwd rd rs => Psxwd rd rs
| PArithRR Asmblock.Pzxwd rd rs => Pzxwd rd rs
| PArithRR Asmblock.Pfnegd rd rs => Pfnegd rd rs
+ | PArithRR Asmblock.Pfloatwrnsz rd rs => Pfloatwrnsz rd rs
(* RI32 *)
| PArithRI32 Asmblock.Pmake rd imm => Pmake rd imm
|