diff options
Diffstat (limited to 'riscV/Asm.v')
| -rw-r--r-- | riscV/Asm.v | 11 |
1 files changed, 9 insertions, 2 deletions
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 *) |