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 | 6 | ||||
-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_fdext_regs.sail | 99 | ||||
-rw-r--r-- | model/riscv_insts_cdext.sail | 16 | ||||
-rw-r--r-- | model/riscv_insts_cfext.sail | 16 | ||||
-rw-r--r-- | model/riscv_insts_dext.sail | 286 | ||||
-rw-r--r-- | model/riscv_insts_fext.sail | 222 | ||||
-rw-r--r-- | model/riscv_sys_control.sail | 6 | ||||
-rw-r--r-- | model/riscv_sys_regs.sail | 9 | ||||
-rw-r--r-- | ocaml_emulator/platform.ml | 2 |
17 files changed, 397 insertions, 287 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..c4a13f4 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,10 @@ 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; + 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_fdext_regs.sail b/model/riscv_fdext_regs.sail index 13de44d..4180a72 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -74,6 +74,41 @@ /* 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_unbox_do : (bool, bits(64)) -> bits(32) +function nan_unbox_do (zfinx_en, regval) = + if zfinx_en + then regval [31..0] + else if regval [63..32] == 0x_FFFF_FFFF + then regval [31..0] + else canonical_NaN_S() + +val nan_unbox_pass : (bool, bits(32)) -> bits(32) +function nan_unbox_pass (zfinx_en, regval) = + regval + +val nan_box_do : (bool, bits(32)) -> bits(64) +function nan_box_do (zfinx_en, regval) = + 0x_FFFF_FFFF @ regval + + +val nan_box_pass : (bool, bits(32)) -> bits(32) +function nan_box_pass (zfinx_en, regval) = + regval + +overload nan_unbox = { nan_unbox_do, nan_unbox_pass } +overload nan_box = { nan_box_do, nan_box_pass } + + +/* **************************************************************** */ /* Floating point register file */ register f0 : fregtype @@ -210,6 +245,58 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = { overload F = {rF_bits, wF_bits, rF, wF} +/* ---- Register Read/ Writes */ + +val rX_or_F_32 : (bool, bits(5)) -> bits(32) effect {escape, rreg} +function rX_or_F_32(zfinx_en, i) = { + if zfinx_en then + nan_unbox(zfinx_en, rX(unsigned(i))) + else + nan_unbox(zfinx_en, rF(unsigned(i))) +} + +val rX_or_F_64 : (bool, bits(5)) -> bits(64) effect {escape, rreg} +function rX_or_F_64(zfinx_en, i) = { + assert (zfinx_en | sizeof(flen) == 64); + if zfinx_en & sizeof (xlen) == 32 then { + assert (i[0] == bitzero); + if i == 0b00000 then + sail_zeros(64) + else rX(unsigned(i+1)) @ rX(unsigned(i)) + } + else if zfinx_en & sizeof(xlen) == 64 then + rX(unsigned(i)) + else + rF(unsigned(i)) +} + +val wX_or_F_64 : (bool, bits(5), bits(64)) -> unit effect {escape, wreg} +function wX_or_F_64(zfinx_en: bool, i: bits(5), data: bits(64)) = { + assert (zfinx_en | sizeof(flen) == 64); + if zfinx_en & sizeof(xlen) == 32 then { + assert (i[0] == bitzero); + if i != 0b00000 then { + wX(unsigned(i)) = data[31..0]; + wX(unsigned(i+1)) = data[63..32]; + } + } + else if zfinx_en & sizeof (xlen) == 64 then + wX(unsigned(i)) = data + else if ~ (zfinx_en) & sizeof (flen) == 64 then + wF(unsigned(i)) = data +} + +val wX_or_F_32 : (bool, bits(5), bits(32)) -> unit effect {escape, wreg} +function wX_or_F_32(zfinx_en: bool, i: bits(5), data : bits(32)) = { + if zfinx_en then + wX(unsigned(i)) = nan_box(zfinx_en, data) + else + wF(unsigned(i)) = nan_box(zfinx_en, data) +} + +overload X_or_F_S = { rX_or_F_32, wX_or_F_32 } +overload X_or_F_D = { rX_or_F_64, wX_or_F_64 } + /* register names */ val freg_name_abi : regidx <-> string @@ -289,6 +376,12 @@ mapping freg_name = { 0b11111 <-> "ft11" } +val reg_or_freg_name : bits(5) <-> string +mapping reg_or_freg_name = { + reg if sys_enable_zfinx() <-> reg_name(reg) if sys_enable_zfinx(), + reg if ~ (sys_enable_zfinx()) <-> freg_name(reg) if ~ (sys_enable_zfinx()) +} + val init_fdext_regs : unit -> unit effect {wreg} function init_fdext_regs () = { f0 = zero_freg; @@ -344,13 +437,13 @@ 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(); + if ~ (sys_enable_zfinx()) then dirty_fd_context(); } /* called for softfloat paths (softfloat flags are consistent) */ val write_fflags : (bits(5)) -> unit effect {rreg, wreg} function write_fflags(fflags) = { - if fcsr.FFLAGS() != fflags + if fcsr.FFLAGS() != fflags & ~ (sys_enable_zfinx()) then dirty_fd_context(); fcsr->FFLAGS() = fflags; } @@ -363,6 +456,6 @@ function accrue_fflags(flags) = { then { fcsr->FFLAGS() = f; update_softfloat_fflags(f); - dirty_fd_context(); + if ~ (sys_enable_zfinx()) then dirty_fd_context(); } } diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail index 77a6302..0c6bbd1 100644 --- a/model/riscv_insts_cdext.sail +++ b/model/riscv_insts_cdext.sail @@ -77,9 +77,9 @@ union clause ast = C_FLDSP : (bits(6), regidx) mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) <-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) function clause execute (C_FLDSP(uimm, rd)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -95,9 +95,9 @@ mapping clause assembly = C_FLDSP(uimm, rd) union clause ast = C_FSDSP : (bits(6), regidx) mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) <-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) function clause execute (C_FSDSP(uimm, rs2)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -113,9 +113,9 @@ mapping clause assembly = C_FSDSP(uimm, rs2) union clause ast = C_FLD : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) <-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) function clause execute (C_FLD(uimm, rsc, rdc)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -133,9 +133,9 @@ mapping clause assembly = C_FLD(uimm, rsc, rdc) union clause ast = C_FSD : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) <-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() + if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx()) function clause execute (C_FSD(uimm, rsc1, rsc2)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail index 9aa94ef..98eea24 100644 --- a/model/riscv_insts_cfext.sail +++ b/model/riscv_insts_cfext.sail @@ -77,9 +77,9 @@ union clause ast = C_FLWSP : (bits(6), regidx) mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd) - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) function clause execute (C_FLWSP(imm, rd)) = { let imm : bits(12) = EXTZ(imm @ 0b00); @@ -95,9 +95,9 @@ mapping clause assembly = C_FLWSP(imm, rd) union clause ast = C_FSWSP : (bits(6), regidx) mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2) - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) <-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) function clause execute (C_FSWSP(uimm, rs2)) = { let imm : bits(12) = EXTZ(uimm @ 0b00); @@ -113,9 +113,9 @@ mapping clause assembly = C_FSWSP(uimm, rd) union clause ast = C_FLW : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd) - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) function clause execute (C_FLW(uimm, rsc, rdc)) = { let imm : bits(12) = EXTZ(uimm @ 0b00); @@ -133,9 +133,9 @@ mapping clause assembly = C_FLW(uimm, rsc, rdc) union clause ast = C_FSW : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2) - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) <-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 - if sizeof(xlen) == 32 & haveRVC() & haveFExt() + if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx()) function clause execute (C_FSW(uimm, rsc1, rsc2)) = { let imm : bits(12) = EXTZ(uimm @ 0b00); diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index ea6f280..068bba6 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 @@ -302,27 +298,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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs3, rs2, rs1, rd]) +<-> rs3 @ 0b01 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if supports_RV32D_or_RV64D([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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_64b = X_or_F_D(sys_enable_zfinx(), rs2); + let rs3_val_64b = X_or_F_D(sys_enable_zfinx(), rs3); + match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -335,7 +332,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; + X_or_F_D(sys_enable_zfinx(), rd, rd_val_64b); RETIRE_SUCCESS } } @@ -352,10 +349,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_name(rs2) + ^ sep() ^ reg_or_freg_name(rs3) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ @@ -368,26 +365,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 supports_RV32D_or_RV64D([rs2, rs1, rd]) +<-> 0b000_0001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1, rd]) +<-> 0b000_0101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1, rd]) +<-> 0b000_1001 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1, rd]) +<-> 0b000_1101 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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); + rs1_val_64b = X_or_F_D(sys_enable_zfinx(), rs1); + rs2_val_64b = X_or_F_D(sys_enable_zfinx(), rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -399,7 +396,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; + X_or_F_D(sys_enable_zfinx(), rd, rd_val_64b); RETIRE_SUCCESS } } @@ -416,9 +413,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_name(rs2) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ @@ -431,32 +428,32 @@ 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 supports_RV32D_or_RV64D([rs1, rd]) +<-> 0b010_1101 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs1]) +<-> 0b110_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs1]) +<-> 0b110_0001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rd]) +<-> 0b110_1001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rd]) +<-> 0b110_1001 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs1]) +<-> 0b010_0000 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rd]) +<-> 0b010_0001 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([rd]) /* D instructions, RV64 only */ @@ -479,7 +476,7 @@ mapping clause encdec = /* 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 = X_or_F_D(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -487,14 +484,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; + X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -509,7 +506,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 = X_or_F_D(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -532,7 +529,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; + X_or_F_D(sys_enable_zfinx(), rd, rd_val_D); RETIRE_SUCCESS } } @@ -547,14 +544,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; + X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -562,14 +559,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); + X_or_F_S(sys_enable_zfinx(), 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)); + rs1_val_S = X_or_F_S(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -577,7 +574,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; + X_or_F_D(sys_enable_zfinx(), rd, rd_val_D); RETIRE_SUCCESS } } @@ -585,7 +582,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); + rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -601,7 +598,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 = X_or_F_D(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -609,7 +606,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = { let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D); write_fflags(fflags); - X(rd) = EXTS(rd_val_LU); + X(rd) = rd_val_LU; RETIRE_SUCCESS } } @@ -625,7 +622,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; + X_or_F_D(sys_enable_zfinx(), rd, rd_val_D); RETIRE_SUCCESS } } @@ -641,7 +638,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; + X_or_F_D(sys_enable_zfinx(), rd, rd_val_D); RETIRE_SUCCESS } } @@ -667,68 +664,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ @@ -740,68 +737,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 supports_RV32D_or_RV64D([rs2, rs1, rd]) + <-> 0b001_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1, rd]) + <-> 0b001_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1, rd]) + <-> 0b001_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1, rd]) + <-> 0b001_0101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1, rd]) + <-> 0b001_0101 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1]) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1]) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 supports_RV32D_or_RV64D([rs2, rs1]) + <-> 0b101_0001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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; + X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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; + X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), 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; + X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); @@ -815,13 +813,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; + X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); @@ -835,13 +833,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; + X_or_F_D(sys_enable_zfinx(), 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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Eq (rs1_val_D, rs2_val_D); @@ -852,11 +850,11 @@ 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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2); let (fflags, rd_val) : (bits_fflags, bool) = - riscv_f64Lt (rs1_val_D, rs2_val_D); + riscv_f64Lt (rs1_val_D, rs2_val_D); write_fflags(fflags); X(rd) = EXTZ(bool_to_bits(rd_val)); @@ -864,8 +862,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 = X_or_F_D(sys_enable_zfinx(), rs1); + let rs2_val_D = X_or_F_D(sys_enable_zfinx(), rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Le (rs1_val_D, rs2_val_D); @@ -890,51 +888,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_name(rs2) /* ****************************************************************** */ /* Unary, no rounding mode */ @@ -943,21 +941,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 supports_RV32D_or_RV64D([rs1]) + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if supports_RV32D_or_RV64D([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 is_RV64D() & ~ (sys_enable_zfinx()) + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() & ~ (sys_enable_zfinx()) -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 is_RV64D() & ~ (sys_enable_zfinx()) + <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() & ~ (sys_enable_zfinx()) /* Execution semantics ================================ */ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = { - let rs1_val_D = F(rs1); + let rs1_val_D = X_or_F_D(sys_enable_zfinx(), rs1); let rd_val_10b : bits (10) = if f_is_neg_inf_D (rs1_val_D) then 0b_00_0000_0001 @@ -1013,6 +1011,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() ^ reg_or_freg_name(rs1) /* ****************************************************************** */ diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 69fc528..8e42b01 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,27 +316,6 @@ 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} */ @@ -350,6 +325,17 @@ function is_RV64F () -> bool = (haveFExt() & sizeof(xlen) == 64) function is_RV32D_or_RV64D () -> bool = (haveDExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64)) function is_RV64D () -> bool = (haveDExt() & sizeof(xlen) == 64) +val supports_RV32D_or_RV64D : forall 'n, 'n > 0. (implicit('n), vector('n, dec, bits(5))) -> bool effect {rreg} +function supports_RV32D_or_RV64D (reg_vec_len, registers) = { + if ~ (sys_enable_zfinx()) then is_RV32D_or_RV64D() + else if sys_enable_zfinx() & is_RV64D() then true + else { + foreach (x from 0 to (reg_vec_len - 1) ) { + if (registers[x][0] == bitone) then return false + }; + true + } +} /* ****************************************************************** */ /* Floating-point loads */ @@ -360,11 +346,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 is_RV32F_or_RV64F() & ~ (sys_enable_zfinx()) + <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx()) -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 is_RV32D_or_RV64D() & ~ (sys_enable_zfinx()) + <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx()) /* Execution semantics ================================ */ @@ -385,7 +371,7 @@ val process_fload32 : (regidx, xlenbits, MemoryOpResult(bits(32))) -> Retired effect {escape, rreg, wreg} function process_fload32(rd, addr, value) = match value { - MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, + MemValue(result) => { F(rd) = nan_box(false, result); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } @@ -420,7 +406,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() ^ reg_or_freg_name(rd) ^ sep() ^ hex_bits_12(imm) ^ opt_spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" @@ -434,11 +420,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 is_RV32F_or_RV64F() & ~ (sys_enable_zfinx()) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if is_RV32F_or_RV64F() & ~ (sys_enable_zfinx()) -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 is_RV32D_or_RV64D() & ~ (sys_enable_zfinx()) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if is_RV32D_or_RV64D() & ~ (sys_enable_zfinx()) /* Execution semantics ================================ */ @@ -522,9 +508,9 @@ mapping clause encdec = /* 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_32b = X_or_F_S(sys_enable_zfinx(), rs2); + let rs3_val_32b = X_or_F_S(sys_enable_zfinx(), rs3); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -537,7 +523,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); + X_or_F_S(sys_enable_zfinx(), rd, rd_val_32b); RETIRE_SUCCESS } } @@ -554,10 +540,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_name(rs2) + ^ sep() ^ reg_or_freg_name(rs3) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ @@ -588,8 +574,8 @@ mapping clause encdec = /* 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_32b = X_or_F_S(sys_enable_zfinx(), rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -601,7 +587,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); + X_or_F_S(sys_enable_zfinx(), rd, rd_val_32b); RETIRE_SUCCESS } } @@ -618,9 +604,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_name(rs2) ^ sep() ^ frm_mnemonic(rm) /* ****************************************************************** */ @@ -673,7 +659,7 @@ mapping clause encdec = /* 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 = X_or_F_S(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -681,14 +667,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); + X_or_F_S(sys_enable_zfinx(), 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 = X_or_F_S(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -703,7 +689,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 = X_or_F_S(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -726,7 +712,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); + X_or_F_S(sys_enable_zfinx(), rd, rd_val_S); RETIRE_SUCCESS } } @@ -741,7 +727,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); + X_or_F_S(sys_enable_zfinx(), rd, rd_val_S); RETIRE_SUCCESS } } @@ -749,7 +735,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 = X_or_F_S(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -765,7 +751,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 = X_or_F_S(sys_enable_zfinx(), rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -789,7 +775,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); + X_or_F_S(sys_enable_zfinx(), rd, rd_val_S); RETIRE_SUCCESS } } @@ -805,7 +791,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); + X_or_F_S(sys_enable_zfinx(), rd, rd_val_S); RETIRE_SUCCESS } } @@ -828,55 +814,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) @@ -917,41 +903,41 @@ mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if is_ /* 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), 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); + X_or_F_S(sys_enable_zfinx(), 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), 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); + X_or_F_S(sys_enable_zfinx(), 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), 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); + X_or_F_S(sys_enable_zfinx(), 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); @@ -965,13 +951,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); + X_or_F_S(sys_enable_zfinx(), 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); @@ -985,13 +971,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); + X_or_F_S(sys_enable_zfinx(), 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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Eq (rs1_val_S, rs2_val_S); @@ -1002,8 +988,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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Lt (rs1_val_S, rs2_val_S); @@ -1014,8 +1000,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 = X_or_F_S(sys_enable_zfinx(), rs1); + let rs2_val_S = X_or_F_S(sys_enable_zfinx(), rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Le (rs1_val_S, rs2_val_S); @@ -1040,51 +1026,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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rd) + ^ sep() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_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() ^ reg_or_freg_name(rs1) + ^ sep() ^ reg_or_freg_name(rs2) /* ****************************************************************** */ /* Unary, no rounding mode */ @@ -1096,16 +1082,16 @@ union clause ast = F_UN_TYPE_S : (regidx, regidx, f_un_op_S) 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, FMV_X_W) if haveFExt() - <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() +mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_X_W) if haveFExt() & ~ (sys_enable_zfinx()) + <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & ~ (sys_enable_zfinx()) -mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if haveFExt() - <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() +mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if haveFExt() & ~ (sys_enable_zfinx()) + <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & ~ (sys_enable_zfinx()) /* 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 = X_or_F_S(sys_enable_zfinx(), rs1); let rd_val_10b : bits (10) = if f_is_neg_inf_S (rs1_val_S) then 0b_00_0000_0001 @@ -1134,7 +1120,7 @@ function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = { function clause execute (F_UN_TYPE_S(rs1, rd, FMV_W_X)) = { let rs1_val_X = X(rs1); let rd_val_S = rs1_val_X [31..0]; - F(rd) = nan_box (rd_val_S); + F(rd) = nan_box(false, rd_val_S); RETIRE_SUCCESS } @@ -1159,6 +1145,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() ^ reg_or_freg_name(rs1) /* ****************************************************************** */ diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index f5ee261..06be736 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -560,9 +560,9 @@ function init_sys() -> unit = { misa->S() = 0b1; /* supervisor-mode */ /* We currently support both F and D */ - misa->F() = bool_to_bits(sys_enable_fdext()); /* single-precision */ - misa->D() = if sizeof(flen) >= 64 - then bool_to_bits(sys_enable_fdext()) /* double-precision */ + misa->F() = bool_to_bits(sys_enable_fdext() & ~ (sys_enable_zfinx())); /* single-precision */ + misa->D() = if sizeof(flen) >= 64 & ~ (sys_enable_zfinx()) + then bool_to_bits(sys_enable_fdext()) /* double-precision */ else 0b0; mstatus = set_mstatus_SXL(mstatus, misa.MXL()); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 696d154..28505e3 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 @@ -163,7 +165,7 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { then m else update_C(m, v.C()); /* Handle updates for F/D. */ - if ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) + if ~(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) | sys_enable_zfinx() then m else update_D(update_F(m, v.F()), v.D()) } @@ -278,6 +280,7 @@ 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)); + let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m; /* 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. * FIXME: This should be made a platform parameter. @@ -328,8 +331,8 @@ function in32BitMode() -> bool = { } /* F and D extensions have to enabled both via misa.{FD} as well as mstatus.FS */ -function haveFExt() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00) -function haveDExt() -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00) +function haveFExt() -> bool = (misa.F() == 0b1 & mstatus.FS() != 0b00) | sys_enable_zfinx() +function haveDExt() -> bool = (misa.D() == 0b1 & mstatus.FS() != 0b00) | (sys_enable_zfinx() & sizeof(flen)==64) /* interrupt processing state */ diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 81e33da..a1d9c82 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -11,6 +11,7 @@ let config_enable_dirty_update = ref false let config_enable_misaligned_access = ref false let config_mtval_has_illegal_inst_bits = ref false let config_enable_pmp = ref false +let config_enable_zfinx = ref false let platform_arch = ref P.RV64 @@ -82,6 +83,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 () = !config_enable_zfinx let rom_base () = arch_bits_of_int64 P.rom_base let rom_size () = arch_bits_of_int !rom_size_ref |