Replace sizeof(flen) with flen

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()

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,15 +47,15 @@ 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
 }
 
 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

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)
 

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"),
               };

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);
 

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),

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;