From 21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 1 Feb 2021 18:53:04 +0100 Subject: bits to float --- riscV/Asm.v | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'riscV/Asm.v') diff --git a/riscV/Asm.v b/riscV/Asm.v index 599002e7..d1946a06 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -256,8 +256,10 @@ Inductive instruction : Type := (* floating point register move *) | Pfmv (rd: freg) (rs: freg) (**r move *) - | Pfmvxs (rd: ireg) (rs: freg) (**r move FP single to integer register *) - | Pfmvxd (rd: ireg) (rs: freg) (**r move FP double to integer register *) + | Pfmvxs (rd: ireg) (rs: freg) (**r bitwise move FP single to integer register *) + | Pfmvxd (rd: ireg) (rs: freg) (**r bitwise move FP double to integer register *) + | Pfmvsx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP single *) + | Pfmvdx (rd: freg) (rs: ireg) (**r bitwise move integer register to FP double*) (* 32-bit (single-precision) floating point *) | Pfls (rd: freg) (ra: ireg) (ofs: offset) (**r load float *) @@ -924,6 +926,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#d <- (ExtValues.bits_of_single rs#s))) m | Pfmvxd d s => Next (nextinstr (rs#d <- (ExtValues.bits_of_float rs#s))) m + + | Pfmvsx d s => + Next (nextinstr (rs#d <- (ExtValues.single_of_bits rs#s))) m + | Pfmvdx d s => + Next (nextinstr (rs#d <- (ExtValues.float_of_bits rs#s))) m (** Pseudo-instructions *) -- cgit