diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index ef4069aa2..ecc0490ef 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -19,7 +19,7 @@ enum clause extension = Ext_F function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b00) enum clause extension = Ext_D -function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64 +function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & flen >= 64 enum clause extension = Ext_Zfinx function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx() diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 51a59cd68..18616ff2d 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -30,13 +30,13 @@ function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000 val nan_box_H : bits(16) -> flenbits function nan_box_H val_16b = - if (sizeof(flen) == 32) + if (flen == 32) then 0x_FFFF @ val_16b else 0x_FFFF_FFFF_FFFF @ val_16b val nan_unbox_H : flenbits -> bits(16) function nan_unbox_H regval = - if (sizeof(flen) == 32) + if (flen == 32) then if regval [31..16] == 0x_FFFF then regval [15..0] else canonical_NaN_H() @@ -47,7 +47,7 @@ function nan_unbox_H regval = val nan_box_S : bits(32) -> flenbits function nan_box_S val_32b = { assert(sys_enable_fdext()); - if (sizeof(flen) == 32) + if (flen == 32) then val_32b else 0x_FFFF_FFFF @ val_32b } @@ -55,7 +55,7 @@ function nan_box_S val_32b = { val nan_unbox_S : flenbits -> bits(32) function nan_unbox_S regval = { assert(sys_enable_fdext()); - if (sizeof(flen) == 32) + if (flen == 32) then regval else if regval [63..32] == 0x_FFFF_FFFF then regval [31..0] @@ -210,42 +210,42 @@ overload F = {rF_bits, wF_bits, rF, wF} val rF_H : regidx -> bits(16) function rF_H(i) = { - assert(sizeof(flen) >= 16); + assert(flen >= 16); assert(sys_enable_fdext() & not(sys_enable_zfinx())); nan_unbox(F(i)) } val wF_H : (regidx, bits(16)) -> unit function wF_H(i, data) = { - assert(sizeof(flen) >= 16); + assert(flen >= 16); assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) = nan_box(data) } val rF_S : regidx -> bits(32) function rF_S(i) = { - assert(sizeof(flen) >= 32); + assert(flen >= 32); assert(sys_enable_fdext() & not(sys_enable_zfinx())); nan_unbox(F(i)) } val wF_S : (regidx, bits(32)) -> unit function wF_S(i, data) = { - assert(sizeof(flen) >= 32); + assert(flen >= 32); assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) = nan_box(data) } val rF_D : regidx -> bits(64) function rF_D(i) = { - assert(sizeof(flen) >= 64); + assert(flen >= 64); assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) } val wF_D : (regidx, bits(64)) -> unit function wF_D(i, data) = { - assert(sizeof(flen) >= 64); + assert(flen >= 64); assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) = data } @@ -256,7 +256,7 @@ overload F_D = { rF_D, wF_D } val rF_or_X_H : regidx -> bits(16) function rF_or_X_H(i) = { - assert(sizeof(flen) >= 16); + assert(flen >= 16); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_H(i) @@ -265,7 +265,7 @@ function rF_or_X_H(i) = { val rF_or_X_S : regidx -> bits(32) function rF_or_X_S(i) = { - assert(sizeof(flen) >= 32); + assert(flen >= 32); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_S(i) @@ -274,7 +274,7 @@ function rF_or_X_S(i) = { val rF_or_X_D : regidx -> bits(64) function rF_or_X_D(i) = { - assert(sizeof(flen) >= 64); + assert(flen >= 64); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_D(i) @@ -288,7 +288,7 @@ function rF_or_X_D(i) = { val wF_or_X_H : (regidx, bits(16)) -> unit function wF_or_X_H(i, data) = { - assert(sizeof(flen) >= 16); + assert(flen >= 16); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_H(i) = data @@ -297,7 +297,7 @@ function wF_or_X_H(i, data) = { val wF_or_X_S : (regidx, bits(32)) -> unit function wF_or_X_S(i, data) = { - assert(sizeof(flen) >= 32); + assert(flen >= 32); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_S(i) = data @@ -306,7 +306,7 @@ function wF_or_X_S(i, data) = { val wF_or_X_D : (regidx, bits(64)) -> unit function wF_or_X_D(i, data) = { - assert (sizeof(flen) >= 64); + assert (flen >= 64); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_D(i) = data diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 1d5318e26..c89e9f33b 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -225,7 +225,7 @@ function fle_D (v1, v2, is_quiet) = { /* Helper functions for 'encdec()' */ enum clause extension = Ext_Zdinx -function clause extensionEnabled(Ext_Zdinx) = sys_enable_zfinx() & sizeof(flen) >= 64 +function clause extensionEnabled(Ext_Zdinx) = sys_enable_zfinx() & flen >= 64 function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | extensionEnabled(Ext_Zdinx) diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index b47955d7f..d74e8217a 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -288,7 +288,7 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if extensionEnabled val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64))) -> Retired function process_fload64(rd, addr, value) = - if sizeof(flen) == 64 + if flen == 64 then match value { MemValue(result) => { F(rd) = result; RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } @@ -333,7 +333,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = { process_fload16(rd, vaddr, mem_read(Read(Data), addr, 2, aq, rl, res)), WORD => process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)), - DOUBLE if sizeof(flen) >= 64 => + DOUBLE if flen >= 64 => process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"), } @@ -406,7 +406,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { BYTE => { handle_illegal(); RETIRE_FAIL }, HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), - DOUBLE if sizeof(flen) >= 64 => + DOUBLE if flen >= 64 => process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"), }; diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 89c82803f..bdfdc10a9 100755 --- a/model/riscv_insts_vext_fp.sail +++ b/model/riscv_insts_vext_fp.sail @@ -816,7 +816,7 @@ function clause execute(VFMVFS(vs2, rd)) = { let SEW = get_sew(); let num_elem = get_num_elem(0, SEW); - if illegal_fp_vd_unmasked(SEW, rm_3b) | SEW > sizeof(flen) + if illegal_fp_vd_unmasked(SEW, rm_3b) | SEW > flen then { handle_illegal(); return RETIRE_FAIL }; assert(num_elem > 0 & SEW != 8); diff --git a/model/riscv_insts_vext_fp_utils.sail b/model/riscv_insts_vext_fp_utils.sail index 19187c73a..d8e10d2e7 100755 --- a/model/riscv_insts_vext_fp_utils.sail +++ b/model/riscv_insts_vext_fp_utils.sail @@ -173,7 +173,7 @@ function f_is_NaN(xf) = { /* Scalar register shaping for floating point operations */ val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) function get_scalar_fp(rs1, SEW) = { - assert(sizeof(flen) >= SEW, "invalid vector floating-point type width: FLEN < SEW"); + assert(flen >= SEW, "invalid vector floating-point type width: FLEN < SEW"); match SEW { 16 => F_H(rs1), 32 => F_S(rs1), diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6a06caec3..e07704c00 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -514,7 +514,7 @@ function init_sys() -> unit = { /* We currently support both F and D */ misa[F] = bool_to_bits(sys_enable_fdext()); /* single-precision */ - misa[D] = if sizeof(flen) >= 64 + misa[D] = if flen >= 64 then bool_to_bits(sys_enable_fdext()) /* double-precision */ else 0b0;