diff options
| -rw-r--r-- | c_emulator/riscv_platform.c | 3 | ||||
| -rw-r--r-- | c_emulator/riscv_platform.h | 1 | ||||
| -rw-r--r-- | c_emulator/riscv_platform_impl.c | 1 | ||||
| -rw-r--r-- | c_emulator/riscv_platform_impl.h | 1 | ||||
| -rw-r--r-- | c_emulator/riscv_sim.c | 7 | ||||
| -rw-r--r-- | handwritten_support/0.11/riscv_extras.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/0.11/riscv_extras_sequential.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras.lem | 4 | ||||
| -rw-r--r-- | handwritten_support/riscv_extras_sequential.lem | 4 | ||||
| -rw-r--r-- | model/riscv_csr_map.sail | 2 | ||||
| -rw-r--r-- | model/riscv_fdext_control.sail | 6 | ||||
| -rw-r--r-- | model/riscv_fdext_regs.sail | 106 | ||||
| -rw-r--r-- | model/riscv_insts_dext.sail | 313 | ||||
| -rw-r--r-- | model/riscv_insts_fext.sail | 312 | ||||
| -rw-r--r-- | model/riscv_sys_control.sail | 3 | ||||
| -rw-r--r-- | model/riscv_sys_regs.sail | 14 | ||||
| -rw-r--r-- | ocaml_emulator/platform.ml | 1 |
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 |