aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJessica Clarke <jrtc27@jrtc27.com>2021-11-22 18:02:40 +0000
committerGitHub <noreply@github.com>2021-11-22 18:02:40 +0000
commit085cfcd3fc3be92aaa86b4caabf9d248eae5f83e (patch)
tree03c8408dd35adcc2fa2d28707aeb9867fa6de056
parent43e0dd239f64b0c330f807fed15e639c25c9fda6 (diff)
downloadsail-riscv-085cfcd3fc3be92aaa86b4caabf9d248eae5f83e.zip
sail-riscv-085cfcd3fc3be92aaa86b4caabf9d248eae5f83e.tar.gz
sail-riscv-085cfcd3fc3be92aaa86b4caabf9d248eae5f83e.tar.bz2
Implement support for Zfinx (#130)
NB: Smstateen support is missing in the model so enabling the Zfinx extension provides an architectural covert channel via FCSR if privileged software is not aware of Zfinx's existence. Co-authored-by: Jessica Clarke <jrtc27@jrtc27.com> Co-authored-by: Ibrahim Abu Kharmeh <abukharmeh@gmail.com>
Diffstat
-rw-r--r--c_emulator/riscv_platform.c3
-rw-r--r--c_emulator/riscv_platform.h1
-rw-r--r--c_emulator/riscv_platform_impl.c1
-rw-r--r--c_emulator/riscv_platform_impl.h1
-rw-r--r--c_emulator/riscv_sim.c7
-rw-r--r--handwritten_support/0.11/riscv_extras.lem4
-rw-r--r--handwritten_support/0.11/riscv_extras_sequential.lem4
-rw-r--r--handwritten_support/riscv_extras.lem4
-rw-r--r--handwritten_support/riscv_extras_sequential.lem4
-rw-r--r--model/riscv_csr_map.sail2
-rw-r--r--model/riscv_fdext_control.sail6
-rw-r--r--model/riscv_fdext_regs.sail106
-rw-r--r--model/riscv_insts_dext.sail313
-rw-r--r--model/riscv_insts_fext.sail312
-rw-r--r--model/riscv_sys_control.sail3
-rw-r--r--model/riscv_sys_regs.sail14
-rw-r--r--ocaml_emulator/platform.ml1
17 files changed, 452 insertions, 334 deletions
diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index a528bee..2572dbc 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -18,6 +18,9 @@ bool sys_enable_next(unit u)
bool sys_enable_fdext(unit u)
{ return rv_enable_fdext; }
+bool sys_enable_zfinx(unit u)
+{ return rv_enable_zfinx; }
+
bool sys_enable_writable_misa(unit u)
{ return rv_enable_writable_misa; }
diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
index f2a1c70..5335a90 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -4,6 +4,7 @@
bool sys_enable_rvc(unit);
bool sys_enable_next(unit);
bool sys_enable_fdext(unit);
+bool sys_enable_zfinx(unit);
bool sys_enable_writable_misa(unit);
bool plat_enable_dirty_update(unit);
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index 946b2ba..b1504a7 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -4,6 +4,7 @@
/* Settings of the platform implementation, with common defaults. */
bool rv_enable_pmp = false;
+bool rv_enable_zfinx = false;
bool rv_enable_rvc = true;
bool rv_enable_next = false;
bool rv_enable_writable_misa = true;
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index 094cf3e..165fb94 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -8,6 +8,7 @@
#define DEFAULT_RSTVEC 0x00001000
extern bool rv_enable_pmp;
+extern bool rv_enable_zfinx;
extern bool rv_enable_rvc;
extern bool rv_enable_next;
extern bool rv_enable_fdext;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index a1e4075..a2d1bce 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -127,6 +127,7 @@ static struct option options[] = {
{"trace", optional_argument, 0, 'v'},
{"no-trace", optional_argument, 0, 'V'},
{"inst-limit", required_argument, 0, 'l'},
+ {"enable-zfinx", no_argument, 0, 'x'},
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c'},
#endif
@@ -236,6 +237,7 @@ char *process_args(int argc, char **argv)
"V::"
"v::"
"l:"
+ "x"
#ifdef SAILCOV
"c:"
#endif
@@ -325,6 +327,11 @@ char *process_args(int argc, char **argv)
case 'l':
insn_limit = atoi(optarg);
break;
+ case 'x':
+ fprintf(stderr, "enabling Zfinx support.\n");
+ rv_enable_zfinx = true;
+ rv_enable_fdext = false;
+ break;
#ifdef SAILCOV
case 'c':
sailcov_file = strdup(optarg);
diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem
index 2182940..2509057 100644
--- a/handwritten_support/0.11/riscv_extras.lem
+++ b/handwritten_support/0.11/riscv_extras.lem
@@ -87,6 +87,10 @@ val sys_enable_fdext : unit -> bool
let sys_enable_fdext () = true
declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`
+val sys_enable_zfinx : unit -> bool
+let sys_enable_zfinx () = false
+declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
+
val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_ram_base () = wordFromInteger 0
declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem
index 827f601..0c23651 100644
--- a/handwritten_support/0.11/riscv_extras_sequential.lem
+++ b/handwritten_support/0.11/riscv_extras_sequential.lem
@@ -75,6 +75,10 @@ val sys_enable_rvc : unit -> bool
let sys_enable_rvc () = true
declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
+val sys_enable_zfinx : unit -> bool
+let sys_enable_zfinx () = false
+declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
+
val sys_enable_next : unit -> bool
let sys_enable_next () = true
declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem
index b0737e5..93f19ab 100644
--- a/handwritten_support/riscv_extras.lem
+++ b/handwritten_support/riscv_extras.lem
@@ -155,6 +155,10 @@ val sys_enable_fdext : unit -> bool
let sys_enable_fdext () = true
declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`
+val sys_enable_zfinx : unit -> bool
+let sys_enable_zfinx () = false
+declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
+
val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_ram_base () = wordFromInteger 0
declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem
index 5c883bf..ddfe74f 100644
--- a/handwritten_support/riscv_extras_sequential.lem
+++ b/handwritten_support/riscv_extras_sequential.lem
@@ -143,6 +143,10 @@ val sys_enable_rvc : unit -> bool
let sys_enable_rvc () = true
declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
+val sys_enable_zfinx : unit -> bool
+let sys_enable_zfinx () = false
+declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
+
val sys_enable_next : unit -> bool
let sys_enable_next () = true
declare ocaml target_rep function sys_enable_next = `Platform.enable_next`
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 87211ea..31872d3 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -186,5 +186,5 @@ val ext_read_CSR : csreg -> option(xlenbits) effect {rreg}
scattered function ext_read_CSR
/* returns new value (after legalisation) if the CSR is defined */
-val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg}
+val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg, escape}
scattered function ext_write_CSR
diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
index c47e562..7e299a7 100644
--- a/model/riscv_fdext_control.sail
+++ b/model/riscv_fdext_control.sail
@@ -77,9 +77,9 @@
/* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg} */
-function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveDExt()
-function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveDExt()
-function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveDExt()
+function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx()
+function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx()
+function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx()
function clause ext_read_CSR (0x001) = Some (EXTZ (fcsr.FFLAGS()))
function clause ext_read_CSR (0x002) = Some (EXTZ (fcsr.FRM()))
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
index 13de44d..4f48b3e 100644
--- a/model/riscv_fdext_regs.sail
+++ b/model/riscv_fdext_regs.sail
@@ -74,6 +74,34 @@
/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */
/* **************************************************************** */
+/* NaN boxing/unboxing. */
+/* When 32-bit floats (single-precision) are stored in 64-bit regs */
+/* they must be 'NaN boxed' (upper 32b all ones). */
+/* When 32-bit floats (single-precision) are read from 64-bit regs */
+/* they must be 'NaN unboxed'. */
+
+function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000
+function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000
+
+val nan_box : bits(32) -> flenbits effect {escape}
+function nan_box val_32b = {
+ assert(sys_enable_fdext());
+ if (sizeof(flen) == 32)
+ then val_32b
+ else 0x_FFFF_FFFF @ val_32b
+}
+
+val nan_unbox : flenbits -> bits(32) effect {escape}
+function nan_unbox regval = {
+ assert(sys_enable_fdext());
+ if (sizeof(flen) == 32)
+ then regval
+ else if regval [63..32] == 0x_FFFF_FFFF
+ then regval [31..0]
+ else canonical_NaN_S()
+}
+
+/* **************************************************************** */
/* Floating point register file */
register f0 : fregtype
@@ -110,12 +138,19 @@ register f30 : fregtype
register f31 : fregtype
function dirty_fd_context() -> unit = {
+ assert(sys_enable_fdext());
mstatus->FS() = extStatus_to_bits(Dirty);
mstatus->SD() = 0b1
}
+function dirty_fd_context_if_present() -> unit = {
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext() then dirty_fd_context()
+}
+
val rF : forall 'n, 0 <= 'n < 32. regno('n) -> flenbits effect {rreg, escape}
function rF r = {
+ assert(sys_enable_fdext());
let v : fregtype =
match r {
0 => f0,
@@ -157,6 +192,7 @@ function rF r = {
val wF : forall 'n, 0 <= 'n < 32. (regno('n), flenbits) -> unit effect {wreg, escape}
function wF (r, in_v) = {
+ assert(sys_enable_fdext());
let v = fregval_into_freg(in_v);
match r {
0 => f0 = v,
@@ -210,6 +246,58 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {
overload F = {rF_bits, wF_bits, rF, wF}
+val rF_or_X_S : bits(5) -> bits(32) effect {escape, rreg}
+function rF_or_X_S(i) = {
+ assert(sizeof(flen) >= 32);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then nan_unbox(F(i))
+ else X(i)[31..0]
+}
+
+val rF_or_X_D : bits(5) -> bits(64) effect {escape, rreg}
+function rF_or_X_D(i) = {
+ assert(sizeof(flen) >= 64);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then F(unsigned(i))
+ else if sizeof(xlen) >= 64
+ then X(i)[63..0]
+ else {
+ assert(i[0] == bitzero);
+ if i == zeros() then zeros() else X(i + 1) @ X(i)
+ }
+}
+
+val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
+function wF_or_X_S(i, data) = {
+ assert(sizeof(flen) >= 32);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then F(i) = nan_box(data)
+ else X(i) = EXTS(data)
+}
+
+val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
+function wF_or_X_D(i, data) = {
+ assert (sizeof(flen) >= 64);
+ assert(sys_enable_fdext() != sys_enable_zfinx());
+ if sys_enable_fdext()
+ then F(i) = data
+ else if sizeof(xlen) >= 64
+ then X(i) = EXTS(data)
+ else {
+ assert (i[0] == bitzero);
+ if i != zeros() then {
+ X(i) = data[31..0];
+ X(i + 1) = data[63..32];
+ }
+ }
+}
+
+overload F_or_X_S = { rF_or_X_S, wF_or_X_S }
+overload F_or_X_D = { rF_or_X_D, wF_or_X_D }
+
/* register names */
val freg_name_abi : regidx <-> string
@@ -289,6 +377,12 @@ mapping freg_name = {
0b11111 <-> "ft11"
}
+val freg_or_reg_name : bits(5) <-> string
+mapping freg_or_reg_name = {
+ reg if sys_enable_fdext() <-> freg_name(reg) if sys_enable_fdext(),
+ reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx()
+}
+
val init_fdext_regs : unit -> unit effect {wreg}
function init_fdext_regs () = {
f0 = zero_freg;
@@ -339,30 +433,30 @@ bitfield Fcsr : bits(32) = {
register fcsr : Fcsr
-val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg}
+val ext_write_fcsr : (bits(3), bits(5)) -> unit effect {rreg, wreg, escape}
function ext_write_fcsr (frm, fflags) = {
fcsr->FRM() = frm; /* Note: frm can be an illegal value, 101, 110, 111 */
fcsr->FFLAGS() = fflags;
update_softfloat_fflags(fflags);
- dirty_fd_context();
+ dirty_fd_context_if_present();
}
/* called for softfloat paths (softfloat flags are consistent) */
-val write_fflags : (bits(5)) -> unit effect {rreg, wreg}
+val write_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
function write_fflags(fflags) = {
if fcsr.FFLAGS() != fflags
- then dirty_fd_context();
+ then dirty_fd_context_if_present();
fcsr->FFLAGS() = fflags;
}
/* called for non-softfloat paths (softfloat flags need updating) */
-val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg}
+val accrue_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
function accrue_fflags(flags) = {
let f = fcsr.FFLAGS() | flags;
if fcsr.FFLAGS() != f
then {
fcsr->FFLAGS() = f;
update_softfloat_fflags(f);
- dirty_fd_context();
+ dirty_fd_context_if_present();
}
}
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index ea6f280..ebd6eae 100644
--- a/model/riscv_insts_dext.sail
+++ b/model/riscv_insts_dext.sail
@@ -98,10 +98,6 @@ function fsplit_D x64 = (x64[63..63], x64[62..52], x64[51..0])
val fmake_D : (bits(1), bits(11), bits(52)) -> bits(64)
function fmake_D (sign, exp, mant) = sign @ exp @ mant
-/* ---- Canonical NaNs */
-
-function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000
-
/* ---- Structure tests */
val f_is_neg_inf_D : bits(64) -> bool
@@ -284,6 +280,21 @@ function fle_D (v1, v2, is_quiet) = {
(result, fflags)
}
+/* **************************************************************** */
+/* Helper functions for 'encdec()' */
+
+function haveDoubleFPU() -> bool = haveDExt() | haveZdinx()
+
+/* RV32Zdinx requires even register pairs; can be omitted for code */
+/* not used for RV32Zdinx (i.e. RV64-only or D-only). */
+val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, dec, regidx)) -> bool
+function validDoubleRegs(n, regs) = {
+ if haveZdinx() & sizeof(xlen) == 32 then
+ foreach (i from 0 to (n - 1))
+ if (regs[i][0] == bitone) then return false;
+ true
+}
+
/* ****************************************************************** */
/* Floating-point loads */
/* These are defined in: riscv_insts_fext.sail */
@@ -302,27 +313,28 @@ union clause ast = F_MADD_TYPE_D : (regidx, regidx, regidx, rounding_mode, regid
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMADD_D) if is_RV32D_or_RV64D()
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if is_RV32D_or_RV64D()
+ F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMADD_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
mapping clause encdec =
- F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMSUB_D) if is_RV32D_or_RV64D()
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if is_RV32D_or_RV64D()
+ F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FMSUB_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
mapping clause encdec =
- F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMSUB_D) if is_RV32D_or_RV64D()
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if is_RV32D_or_RV64D()
+ F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMSUB_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
mapping clause encdec =
- F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMADD_D) if is_RV32D_or_RV64D()
-<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if is_RV32D_or_RV64D()
+ F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, FNMADD_D) if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
+<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if haveDoubleFPU() & validDoubleRegs([rs3, rs2, rs1, rd])
/* Execution semantics ================================ */
function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = {
- let rs1_val_64b = F(rs1);
- let rs2_val_64b = F(rs2);
- let rs3_val_64b = F(rs3);
+ let rs1_val_64b = F_or_X_D(rs1);
+ let rs2_val_64b = F_or_X_D(rs2);
+ let rs3_val_64b = F_or_X_D(rs3);
+
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -335,7 +347,7 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = {
FNMADD_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, negate_D (rs3_val_64b))
};
write_fflags(fflags);
- F(rd) = rd_val_64b;
+ F_or_X_D(rd) = rd_val_64b;
RETIRE_SUCCESS
}
}
@@ -352,10 +364,10 @@ mapping f_madd_type_mnemonic_D : f_madd_op_D <-> string = {
mapping clause assembly = F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)
<-> f_madd_type_mnemonic_D(op)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
- ^ sep() ^ freg_name(rs3)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs3)
^ sep() ^ frm_mnemonic(rm)
/* ****************************************************************** */
@@ -368,26 +380,26 @@ union clause ast = F_BIN_RM_TYPE_D : (regidx, regidx, rounding_mode, regidx, f_b
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FADD_D) if is_RV32D_or_RV64D()
-<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FADD_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
mapping clause encdec =
- F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FSUB_D) if is_RV32D_or_RV64D()
-<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FSUB_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
mapping clause encdec =
- F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FMUL_D) if is_RV32D_or_RV64D()
-<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FMUL_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
mapping clause encdec =
- F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FDIV_D) if is_RV32D_or_RV64D()
-<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, FDIV_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
/* Execution semantics ================================ */
function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = {
- let rs1_val_64b = F(rs1);
- let rs2_val_64b = F(rs2);
+ let rs1_val_64b = F_or_X_D(rs1);
+ let rs2_val_64b = F_or_X_D(rs2);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -399,7 +411,7 @@ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = {
FDIV_D => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b)
};
write_fflags(fflags);
- F(rd) = rd_val_64b;
+ F_or_X_D(rd) = rd_val_64b;
RETIRE_SUCCESS
}
}
@@ -416,9 +428,9 @@ mapping f_bin_rm_type_mnemonic_D : f_bin_rm_op_D <-> string = {
mapping clause assembly = F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)
<-> f_bin_rm_type_mnemonic_D(op)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
^ sep() ^ frm_mnemonic(rm)
/* ****************************************************************** */
@@ -431,55 +443,55 @@ union clause ast = F_UN_RM_TYPE_D : (regidx, rounding_mode, regidx, f_un_rm_op_D
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D) if is_RV32D_or_RV64D()
-<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D) if haveDoubleFPU() & validDoubleRegs([rs1, rd])
+<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1, rd])
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D) if is_RV32D_or_RV64D()
-<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D) if haveDoubleFPU() & validDoubleRegs([rs1])
+<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1])
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D) if is_RV32D_or_RV64D()
-<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D) if haveDoubleFPU() & validDoubleRegs([rs1])
+<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1])
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W) if is_RV32D_or_RV64D()
-<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W) if haveDoubleFPU() & validDoubleRegs([rd])
+<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rd])
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU) if is_RV32D_or_RV64D()
-<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU) if haveDoubleFPU() & validDoubleRegs([rd])
+<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rd])
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D) if is_RV32D_or_RV64D()
-<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D) if haveDoubleFPU() & validDoubleRegs([rs1])
+<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1])
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S) if is_RV32D_or_RV64D()
-<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S) if haveDoubleFPU() & validDoubleRegs([rd])
+<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rd])
/* D instructions, RV64 only */
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) if is_RV64D()
-<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) if haveDoubleFPU() & sizeof(xlen) >= 64
+<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) if is_RV64D()
-<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) if haveDoubleFPU() & sizeof(xlen) >= 64
+<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) if is_RV64D()
-<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) if haveDoubleFPU() & sizeof(xlen) >= 64
+<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64
mapping clause encdec =
- F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) if is_RV64D()
-<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64D()
+ F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) if haveDoubleFPU() & sizeof(xlen) >= 64
+<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64
/* Execution semantics ================================ */
function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = {
- let rs1_val_D = F(rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -487,14 +499,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = {
let (fflags, rd_val_D) = riscv_f64Sqrt (rm_3b, rs1_val_D);
write_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
}
function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = {
- let rs1_val_D = F(rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -509,7 +521,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = {
}
function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = {
- let rs1_val_D = F(rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -532,7 +544,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = {
let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W);
write_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -547,14 +559,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = {
let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU);
write_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
}
function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = {
- let rs1_val_D = F(rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -562,14 +574,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = {
let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D);
write_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
}
function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -577,7 +589,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S);
write_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -585,7 +597,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {
assert(sizeof(xlen) >= 64);
- let rs1_val_D = F(rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -601,7 +613,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {
function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = {
assert(sizeof(xlen) >= 64);
- let rs1_val_D = F(rs1);
+ let rs1_val_D = F_or_X_D(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -625,7 +637,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = {
let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L);
write_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -641,7 +653,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = {
let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU);
write_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
}
@@ -667,68 +679,68 @@ mapping f_un_rm_type_mnemonic_D : f_un_rm_op_D <-> string = {
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)
<-> f_un_rm_type_mnemonic_D(FSQRT_D)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)
<-> f_un_rm_type_mnemonic_D(FCVT_W_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)
<-> f_un_rm_type_mnemonic_D(FCVT_WU_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)
<-> f_un_rm_type_mnemonic_D(FCVT_D_W)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)
<-> f_un_rm_type_mnemonic_D(FCVT_D_WU)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)
<-> f_un_rm_type_mnemonic_D(FCVT_L_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)
<-> f_un_rm_type_mnemonic_D(FCVT_LU_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)
<-> f_un_rm_type_mnemonic_D(FCVT_D_L)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)
<-> f_un_rm_type_mnemonic_D(FCVT_D_LU)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)
<-> f_un_rm_type_mnemonic_D(FCVT_S_D)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)
<-> f_un_rm_type_mnemonic_D(FCVT_D_S)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
/* ****************************************************************** */
@@ -740,68 +752,69 @@ union clause ast = F_BIN_TYPE_D : (regidx, regidx, regidx, f_bin_op_D)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D) if is_RV32D_or_RV64D()
- <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+ <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D) if is_RV32D_or_RV64D()
- <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+ <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D) if is_RV32D_or_RV64D()
- <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+ <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D) if is_RV32D_or_RV64D()
- <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+ <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D) if is_RV32D_or_RV64D()
- <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
+ <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1, rd])
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) if is_RV32D_or_RV64D()
- <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1])
+ <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1])
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) if is_RV32D_or_RV64D()
- <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1])
+ <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1])
-mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if is_RV32D_or_RV64D()
- <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32D_or_RV64D()
+mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if haveDoubleFPU() & validDoubleRegs([rs2, rs1])
+ <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs2, rs1])
/* Execution semantics ================================ */
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
+
let (s1, e1, m1) = fsplit_D (rs1_val_D);
let (s2, e2, m2) = fsplit_D (rs2_val_D);
let rd_val_D = fmake_D (s2, e1, m1);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
let (s1, e1, m1) = fsplit_D (rs1_val_D);
let (s2, e2, m2) = fsplit_D (rs2_val_D);
let rd_val_D = fmake_D (0b1 ^ s2, e1, m1);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
let (s1, e1, m1) = fsplit_D (rs1_val_D);
let (s2, e2, m2) = fsplit_D (rs2_val_D);
let rd_val_D = fmake_D (s1 ^ s2, e1, m1);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
let is_quiet = true;
let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet);
@@ -815,13 +828,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = {
else /* (not rs1_lt_rs2) */ rs2_val_D;
accrue_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
let is_quiet = true;
let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet);
@@ -835,13 +848,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = {
else /* (not rs2_lt_rs1) */ rs2_val_D;
accrue_fflags(fflags);
- F(rd) = rd_val_D;
+ F_or_X_D(rd) = rd_val_D;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f64Eq (rs1_val_D, rs2_val_D);
@@ -852,8 +865,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
}
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f64Lt (rs1_val_D, rs2_val_D);
@@ -864,8 +877,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
}
function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
- let rs1_val_D = F(rs1);
- let rs2_val_D = F(rs2);
+ let rs1_val_D = F_or_X_D(rs1);
+ let rs2_val_D = F_or_X_D(rs2);
let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f64Le (rs1_val_D, rs2_val_D);
@@ -890,51 +903,51 @@ mapping f_bin_type_mnemonic_D : f_bin_op_D <-> string = {
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)
<-> f_bin_type_mnemonic_D(FSGNJ_D)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)
<-> f_bin_type_mnemonic_D(FSGNJN_D)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)
<-> f_bin_type_mnemonic_D(FSGNJX_D)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)
<-> f_bin_type_mnemonic_D(FMIN_D)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)
<-> f_bin_type_mnemonic_D(FMAX_D)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)
<-> f_bin_type_mnemonic_D(FEQ_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)
<-> f_bin_type_mnemonic_D(FLT_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)
<-> f_bin_type_mnemonic_D(FLE_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
/* ****************************************************************** */
/* Unary, no rounding mode */
@@ -943,21 +956,21 @@ union clause ast = F_UN_TYPE_D : (regidx, regidx, f_un_op_D)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if haveDExt()
- <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDExt()
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if haveDoubleFPU() & validDoubleRegs([rs1])
+ <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDoubleFPU() & validDoubleRegs([rs1])
/* D instructions, RV64 only */
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if is_RV64D()
- <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D()
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if haveDExt()
+ <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt()
-mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if is_RV64D()
- <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D()
+mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if haveDExt()
+ <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt()
/* Execution semantics ================================ */
function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = {
- let rs1_val_D = F(rs1);
+ let rs1_val_D = F_or_X_D(rs1);
let rd_val_10b : bits (10) =
if f_is_neg_inf_D (rs1_val_D) then 0b_00_0000_0001
@@ -1013,6 +1026,6 @@ mapping clause assembly = F_UN_TYPE_D(rs1, rd, FMV_D_X)
mapping clause assembly = F_UN_TYPE_D(rs1, rd, FCLASS_D)
<-> f_un_type_mnemonic_D(FCLASS_D)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
/* ****************************************************************** */
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index 69fc528..2995f19 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -134,10 +134,6 @@ function fsplit_S x32 = (x32[31..31], x32[30..23], x32[22..0])
val fmake_S : (bits(1), bits(8), bits(23)) -> bits(32)
function fmake_S (sign, exp, mant) = sign @ exp @ mant
-/* ---- Canonical NaNs */
-
-function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000
-
/* ---- Structure tests */
val f_is_neg_inf_S : bits(32) -> bool
@@ -320,35 +316,9 @@ function fle_S (v1, v2, is_quiet) = {
}
/* **************************************************************** */
-/* NaN boxing/unboxing. */
-/* When 32-bit floats (single-precision) are stored in 64-bit regs */
-/* they must be 'NaN boxed' (upper 32b all ones). */
-/* When 32-bit floats (single-precision) are read from 64-bit regs */
-/* they must be 'NaN unboxed'. */
-
-val nan_box : bits(32) -> flenbits
-function nan_box val_32b =
- if (sizeof(flen) == 32)
- then val_32b
- else 0x_FFFF_FFFF @ val_32b
-
-val nan_unbox : flenbits -> bits(32)
-function nan_unbox regval =
- if (sizeof(flen) == 32)
- then regval
- else if regval [63..32] == 0x_FFFF_FFFF
- then regval [31..0]
- else canonical_NaN_S()
-
-/* **************************************************************** */
-/* Help-functions for 'encdec()' to restrict to certain */
-/* combinations of {F,D} x {RV32,RV64} */
-
-function is_RV32F_or_RV64F () -> bool = (haveFExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64))
-function is_RV64F () -> bool = (haveFExt() & sizeof(xlen) == 64)
+/* Helper functions for 'encdec()' */
-function is_RV32D_or_RV64D () -> bool = (haveDExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64))
-function is_RV64D () -> bool = (haveDExt() & sizeof(xlen) == 64)
+function haveSingleFPU() -> bool = haveFExt() | haveZfinx()
/* ****************************************************************** */
/* Floating-point loads */
@@ -360,11 +330,11 @@ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if is_RV32F_or_RV64F()
- <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if is_RV32F_or_RV64F()
+mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if haveFExt()
+ <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if haveFExt()
-mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if is_RV32D_or_RV64D()
- <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if is_RV32D_or_RV64D()
+mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if haveDExt()
+ <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if haveDExt()
/* Execution semantics ================================ */
@@ -420,7 +390,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
mapping clause assembly = LOAD_FP(imm, rs1, rd, width)
<-> "fl" ^ size_mnemonic(width)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ hex_bits_12(imm)
^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
@@ -434,11 +404,11 @@ union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) if is_RV32F_or_RV64F()
- <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if is_RV32F_or_RV64F()
+mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) if haveFExt()
+ <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if haveFExt()
-mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if is_RV32D_or_RV64D()
- <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if is_RV32D_or_RV64D()
+mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if haveDExt()
+ <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if haveDExt()
/* Execution semantics ================================ */
@@ -504,27 +474,27 @@ union clause ast = F_MADD_TYPE_S : (regidx, regidx, regidx, rounding_mode, regid
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMADD_S) if is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if is_RV32F_or_RV64F()
+ F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMADD_S) if haveSingleFPU()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if haveSingleFPU()
mapping clause encdec =
- F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMSUB_S) if is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if is_RV32F_or_RV64F()
+ F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FMSUB_S) if haveSingleFPU()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if haveSingleFPU()
mapping clause encdec =
- F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMSUB_S) if is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if is_RV32F_or_RV64F()
+ F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMSUB_S) if haveSingleFPU()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if haveSingleFPU()
mapping clause encdec =
- F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMADD_S) if is_RV32F_or_RV64F()
-<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if is_RV32F_or_RV64F()
+ F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, FNMADD_S) if haveSingleFPU()
+<-> rs3 @ 0b00 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if haveSingleFPU()
/* Execution semantics ================================ */
function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = {
- let rs1_val_32b = nan_unbox (F(rs1));
- let rs2_val_32b = nan_unbox (F(rs2));
- let rs3_val_32b = nan_unbox (F(rs3));
+ let rs1_val_32b = F_or_X_S(rs1);
+ let rs2_val_32b = F_or_X_S(rs2);
+ let rs3_val_32b = F_or_X_S(rs3);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -537,7 +507,7 @@ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = {
FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b))
};
write_fflags(fflags);
- F(rd) = nan_box (rd_val_32b);
+ F_or_X_S(rd) = rd_val_32b;
RETIRE_SUCCESS
}
}
@@ -554,10 +524,10 @@ mapping f_madd_type_mnemonic_S : f_madd_op_S <-> string = {
mapping clause assembly = F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)
<-> f_madd_type_mnemonic_S(op)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
- ^ sep() ^ freg_name(rs3)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs3)
^ sep() ^ frm_mnemonic(rm)
/* ****************************************************************** */
@@ -570,26 +540,26 @@ union clause ast = F_BIN_RM_TYPE_S : (regidx, regidx, rounding_mode, regidx, f_b
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FADD_S) if is_RV32F_or_RV64F()
-<-> 0b000_0000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FADD_S) if haveSingleFPU()
+<-> 0b000_0000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec =
- F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FSUB_S) if is_RV32F_or_RV64F()
-<-> 0b000_0100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FSUB_S) if haveSingleFPU()
+<-> 0b000_0100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec =
- F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FMUL_S) if is_RV32F_or_RV64F()
-<-> 0b000_1000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FMUL_S) if haveSingleFPU()
+<-> 0b000_1000 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec =
- F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FDIV_S) if is_RV32F_or_RV64F()
-<-> 0b000_1100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, FDIV_S) if haveSingleFPU()
+<-> 0b000_1100 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
/* Execution semantics ================================ */
function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = {
- let rs1_val_32b = nan_unbox (F(rs1));
- let rs2_val_32b = nan_unbox (F(rs2));
+ let rs1_val_32b = F_or_X_S(rs1);
+ let rs2_val_32b = F_or_X_S(rs2);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -601,7 +571,7 @@ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = {
FDIV_S => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b)
};
write_fflags(fflags);
- F(rd) = nan_box (rd_val_32b);
+ F_or_X_S(rd) = rd_val_32b;
RETIRE_SUCCESS
}
}
@@ -618,9 +588,9 @@ mapping f_bin_rm_type_mnemonic_S : f_bin_rm_op_S <-> string = {
mapping clause assembly = F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)
<-> f_bin_rm_type_mnemonic_S(op)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
^ sep() ^ frm_mnemonic(rm)
/* ****************************************************************** */
@@ -633,47 +603,47 @@ union clause ast = F_UN_RM_TYPE_S : (regidx, rounding_mode, regidx, f_un_rm_op_S
/* AST <-> Binary encoding ================================ */
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S) if is_RV32F_or_RV64F()
-<-> 0b010_1100 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S) if haveSingleFPU()
+<-> 0b010_1100 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S) if is_RV32F_or_RV64F()
-<-> 0b110_0000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S) if haveSingleFPU()
+<-> 0b110_0000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S) if is_RV32F_or_RV64F()
-<-> 0b110_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S) if haveSingleFPU()
+<-> 0b110_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W) if is_RV32F_or_RV64F()
-<-> 0b110_1000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W) if haveSingleFPU()
+<-> 0b110_1000 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU) if is_RV32F_or_RV64F()
-<-> 0b110_1000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU) if haveSingleFPU()
+<-> 0b110_1000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU()
/* F instructions, RV64 only */
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) if is_RV64F()
-<-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) if haveSingleFPU() & sizeof(xlen) >= 64
+<-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) if is_RV64F()
-<-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) if haveSingleFPU() & sizeof(xlen) >= 64
+<-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) if is_RV64F()
-<-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) if haveSingleFPU() & sizeof(xlen) >= 64
+<-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64
mapping clause encdec =
- F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) if is_RV64F()
-<-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if is_RV64F()
+ F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) if haveSingleFPU() & sizeof(xlen) >= 64
+<-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64
/* Execution semantics ================================ */
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -681,14 +651,14 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = {
let (fflags, rd_val_S) = riscv_f32Sqrt (rm_3b, rs1_val_S);
write_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
}
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -703,7 +673,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = {
}
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -726,7 +696,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = {
let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W);
write_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -741,7 +711,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU);
write_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -749,7 +719,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
assert(sizeof(xlen) >= 64);
- let rs1_val_S = nan_unbox (F(rs1));
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -765,7 +735,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = {
assert(sizeof(xlen) >= 64);
- let rs1_val_S = nan_unbox (F(rs1));
+ let rs1_val_S = F_or_X_S(rs1);
match (select_instr_or_fcsr_rm (rm)) {
None() => { handle_illegal(); RETIRE_FAIL },
Some(rm') => {
@@ -789,7 +759,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = {
let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L);
write_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -805,7 +775,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = {
let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU);
write_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
}
@@ -828,55 +798,55 @@ mapping f_un_rm_type_mnemonic_S : f_un_rm_op_S <-> string = {
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)
<-> f_un_rm_type_mnemonic_S(FSQRT_S)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)
<-> f_un_rm_type_mnemonic_S(FCVT_W_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)
<-> f_un_rm_type_mnemonic_S(FCVT_WU_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)
<-> f_un_rm_type_mnemonic_S(FCVT_S_W)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)
<-> f_un_rm_type_mnemonic_S(FCVT_S_WU)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)
<-> f_un_rm_type_mnemonic_S(FCVT_L_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)
<-> f_un_rm_type_mnemonic_S(FCVT_LU_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)
<-> f_un_rm_type_mnemonic_S(FCVT_S_L)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
mapping clause assembly = F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)
<-> f_un_rm_type_mnemonic_S(FCVT_S_LU)
- ^ spc() ^ freg_name(rd)
+ ^ spc() ^ freg_or_reg_name(rd)
^ sep() ^ reg_name(rs1)
^ sep() ^ frm_mnemonic(rm)
@@ -890,68 +860,68 @@ union clause ast = F_BIN_TYPE_S : (regidx, regidx, regidx, f_bin_op_S)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S) if is_RV32F_or_RV64F()
- <-> 0b001_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S) if haveSingleFPU()
+ <-> 0b001_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveSingleFPU()
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S) if is_RV32F_or_RV64F()
- <-> 0b001_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S) if haveSingleFPU()
+ <-> 0b001_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU()
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S) if is_RV32F_or_RV64F()
- <-> 0b001_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S) if haveSingleFPU()
+ <-> 0b001_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveSingleFPU()
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S) if is_RV32F_or_RV64F()
- <-> 0b001_0100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S) if haveSingleFPU()
+ <-> 0b001_0100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveSingleFPU()
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S) if is_RV32F_or_RV64F()
- <-> 0b001_0100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S) if haveSingleFPU()
+ <-> 0b001_0100 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU()
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S) if is_RV32F_or_RV64F()
- <-> 0b101_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S) if haveSingleFPU()
+ <-> 0b101_0000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveSingleFPU()
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S) if is_RV32F_or_RV64F()
- <-> 0b101_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S) if haveSingleFPU()
+ <-> 0b101_0000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU()
-mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if is_RV32F_or_RV64F()
- <-> 0b101_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV32F_or_RV64F()
+mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if haveSingleFPU()
+ <-> 0b101_0000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveSingleFPU()
/* Execution semantics ================================ */
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let (s1, e1, m1) = fsplit_S (rs1_val_S);
let (s2, e2, m2) = fsplit_S (rs2_val_S);
let rd_val_S = fmake_S (s2, e1, m1);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let (s1, e1, m1) = fsplit_S (rs1_val_S);
let (s2, e2, m2) = fsplit_S (rs2_val_S);
let rd_val_S = fmake_S (0b1 ^ s2, e1, m1);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let (s1, e1, m1) = fsplit_S (rs1_val_S);
let (s2, e2, m2) = fsplit_S (rs2_val_S);
let rd_val_S = fmake_S (s1 ^ s2, e1, m1);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let is_quiet = true;
let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet);
@@ -965,13 +935,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = {
else /* (not rs1_lt_rs2) */ rs2_val_S;
accrue_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let is_quiet = true;
let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet);
@@ -985,13 +955,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = {
else /* (not rs2_lt_rs1) */ rs2_val_S;
accrue_fflags(fflags);
- F(rd) = nan_box (rd_val_S);
+ F_or_X_S(rd) = rd_val_S;
RETIRE_SUCCESS
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f32Eq (rs1_val_S, rs2_val_S);
@@ -1002,8 +972,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f32Lt (rs1_val_S, rs2_val_S);
@@ -1014,8 +984,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
}
function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
- let rs2_val_S = nan_unbox (F(rs2));
+ let rs1_val_S = F_or_X_S(rs1);
+ let rs2_val_S = F_or_X_S(rs2);
let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f32Le (rs1_val_S, rs2_val_S);
@@ -1040,51 +1010,51 @@ mapping f_bin_type_mnemonic_S : f_bin_op_S <-> string = {
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)
<-> f_bin_type_mnemonic_S(FSGNJ_S)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)
<-> f_bin_type_mnemonic_S(FSGNJN_S)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)
<-> f_bin_type_mnemonic_S(FSGNJX_S)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)
<-> f_bin_type_mnemonic_S(FMIN_S)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)
<-> f_bin_type_mnemonic_S(FMAX_S)
- ^ spc() ^ freg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ spc() ^ freg_or_reg_name(rd)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)
<-> f_bin_type_mnemonic_S(FEQ_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)
<-> f_bin_type_mnemonic_S(FLT_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
mapping clause assembly = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)
<-> f_bin_type_mnemonic_S(FLE_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
- ^ sep() ^ freg_name(rs2)
+ ^ sep() ^ freg_or_reg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs2)
/* ****************************************************************** */
/* Unary, no rounding mode */
@@ -1093,8 +1063,8 @@ union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S)
/* AST <-> Binary encoding ================================ */
-mapping clause encdec = F_UN_TYPE_S(rs1, rd, FCLASS_S) if haveFExt()
- <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveFExt()
+mapping clause encdec = F_UN_TYPE_S(rs1, rd, FCLASS_S) if haveSingleFPU()
+ <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveSingleFPU()
mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W) if haveFExt()
<-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt()
@@ -1105,7 +1075,7 @@ mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if
/* Execution semantics ================================ */
function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = {
- let rs1_val_S = nan_unbox (F(rs1));
+ let rs1_val_S = F_or_X_S(rs1);
let rd_val_10b : bits (10) =
if f_is_neg_inf_S (rs1_val_S) then 0b_00_0000_0001
@@ -1159,6 +1129,6 @@ mapping clause assembly = F_UN_TYPE_S(rs1, rd, FMV_W_X)
mapping clause assembly = F_UN_TYPE_S(rs1, rd, FCLASS_S)
<-> f_un_type_mnemonic_S(FCLASS_S)
^ spc() ^ reg_name(rd)
- ^ sep() ^ freg_name(rs1)
+ ^ sep() ^ freg_or_reg_name(rs1)
/* ****************************************************************** */
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index f5ee261..6204ae5 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -559,6 +559,9 @@ function init_sys() -> unit = {
misa->U() = 0b1; /* user-mode */
misa->S() = 0b1; /* supervisor-mode */
+ if sys_enable_fdext() & sys_enable_zfinx()
+ then internal_error("F and Zfinx cannot both be enabled!");
+
/* We currently support both F and D */
misa->F() = bool_to_bits(sys_enable_fdext()); /* single-precision */
misa->D() = if sizeof(flen) >= 64
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 696d154..2e638cf 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -144,6 +144,8 @@ val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.
val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool
/* whether misa.{f,d} were enabled at boot */
val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool
+/* whether zfinx was enabled at boot */
+val sys_enable_zfinx = {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool
/* whether the N extension was enabled at boot */
val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool
@@ -178,7 +180,7 @@ function haveMulDiv() -> bool = misa.M() == 0b1
function haveSupMode() -> bool = misa.S() == 0b1
function haveUsrMode() -> bool = misa.U() == 0b1
function haveNExt() -> bool = misa.N() == 0b1
-/* see below for F and D extension tests */
+/* see below for F and D (and Z*inx counterparts) extension tests */
/* Cryptography extension support. Note these will need updating once */
/* Sail can be dynamically configured with different extension support */
@@ -278,11 +280,13 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
/* We don't have any extension context yet. */
let m = update_XS(m, extStatus_to_bits(Off));
+
/* FS is WARL, and making FS writable can support the M-mode emulation of an FPU
- * to support code running in S/U-modes. Spike does this, and for now, we match it.
+ * to support code running in S/U-modes. Spike does this, and for now, we match it,
+ * but only if Zfinx isn't enabled.
* FIXME: This should be made a platform parameter.
*/
-
+ let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m;
let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
let m = update_SD(m, bool_to_bits(dirty));
@@ -331,6 +335,10 @@ function in32BitMode() -> bool = {
function haveFExt() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00)
function haveDExt() -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00)
+/* Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */
+function haveZfinx() -> bool = sys_enable_zfinx()
+function haveZdinx() -> bool = sys_enable_zfinx() & sizeof(flen) >= 64
+
/* interrupt processing state */
bitfield Minterrupts : xlenbits = {
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index 81e33da..ccf4875 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -82,6 +82,7 @@ let enable_dirty_update () = !config_enable_dirty_update
let enable_misaligned_access () = !config_enable_misaligned_access
let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
let enable_pmp () = !config_enable_pmp
+let enable_zfinx () = false
let rom_base () = arch_bits_of_int64 P.rom_base
let rom_size () = arch_bits_of_int !rom_size_ref
generated by cgit v1.1 at 2024-08-04 15:23:14 +0000