diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 18:53:04 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 18:53:04 +0100 |
| commit | 21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47 (patch) | |
| tree | c1068ba7e0aad0744ecd851050317a1967686f91 /riscV/Asm.v | |
| parent | 2e635ffa6693be77004e398f7dd3c2ed6bb6bca0 (diff) | |
| download | compcert-kvx-21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47.tar.gz compcert-kvx-21aaf9c53b2bb0c6d376c2ce436d6dd7f5442a47.zip | |
bits to float
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 *) |