From 4f7d6d6a081de52fe1151a29d44221f4fc35f7be Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 Dec 2021 17:31:41 +0100 Subject: Asm level --- kvx/Asm.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'kvx/Asm.v') diff --git a/kvx/Asm.v b/kvx/Asm.v index fd20316c..333854cf 100644 --- a/kvx/Asm.v +++ b/kvx/Asm.v @@ -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 *) @@ -352,6 +360,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 -- cgit