diff options
Diffstat (limited to 'kvx/Asm.v')
| -rw-r--r-- | kvx/Asm.v | 12 |
1 files changed, 12 insertions, 0 deletions
@@ -163,6 +163,8 @@ Inductive instruction : Type := | Pfloatuwrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (u32 -> 32) *) | Pfloatudrnsz (rd rs: ireg) (**r Floating Point Conversion from unsigned integer (64 bits) *) | Pfloatdrnsz (rd rs: ireg) (**r Floating Point Conversion from integer (64 bits) *) + + (* round to zero *) | Pfixedwrzz (rd rs: ireg) (**r Integer conversion from floating point *) | Pfixeduwrzz (rd rs: ireg) (**r Integer conversion from floating point (f32 -> 32 bits unsigned *) | Pfixeddrzz (rd rs: ireg) (**r Integer conversion from floating point (i64 -> 64 bits) *) @@ -170,6 +172,12 @@ Inductive instruction : Type := | Pfixedudrzz (rd rs: ireg) (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *) | Pfixedudrzz_i32 (rd rs: ireg) (**r unsigned Integer conversion from floating point (u32 -> 64 bits) *) + (* round to nearest, prefer even numbers *) + | Pfixedwrne (rd rs: ireg) (**r Integer conversion from floating point *) + | Pfixeduwrne (rd rs: ireg) (**r Integer conversion from floating point (f32 -> 32 bits unsigned *) + | Pfixeddrne (rd rs: ireg) (**r Integer conversion from floating point (i64 -> 64 bits) *) + | Pfixedudrne (rd rs: ireg) (**r unsigned Integer conversion from floating point (u64 -> 64 bits) *) + (** Arith RI32 *) | Pmake (rd: ireg) (imm: int) (**r load immediate *) @@ -357,6 +365,10 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmvliw.Pfixedudrzz rd rs => Pfixedudrzz rd rs | PArithRR Asmvliw.Pfixeddrzz_i32 rd rs => Pfixeddrzz_i32 rd rs | PArithRR Asmvliw.Pfixedudrzz_i32 rd rs => Pfixedudrzz_i32 rd rs + | PArithRR Asmvliw.Pfixedwrne rd rs => Pfixedwrne rd rs + | PArithRR Asmvliw.Pfixeduwrne rd rs => Pfixeduwrne rd rs + | PArithRR Asmvliw.Pfixeddrne rd rs => Pfixeddrne rd rs + | PArithRR Asmvliw.Pfixedudrne rd rs => Pfixedudrne rd rs (* RI32 *) | PArithRI32 Asmvliw.Pmake rd imm => Pmake rd imm |