Fix NaN boxing issue and add notes for RVV configuration TODOs

.gitignore

@@ -6,6 +6,3 @@ _build/
 _sbuild/
 *.o
 *.a
-c_emulator/riscv_sim_*
-ocaml_emulator/riscv_ocaml_sim_*
-z3_problems

model/riscv_fdext_regs.sail

@@ -536,12 +536,8 @@ function ext_write_fcsr (frm, fflags) = {
 val write_fflags : (bits(5)) -> unit effect {rreg, wreg, escape}
 function write_fflags(fflags) = {
  if fcsr.FFLAGS() != fflags
- then {
- fcsr->FFLAGS() = fflags;
- dirty_fd_context_if_present();
- if get_config_print_reg()
- then print("fcsr.FFLAGS <- " ^ BitStr(fflags))
- }
+ then dirty_fd_context_if_present();
+ fcsr->FFLAGS() = fflags;
 }
 
 /* called for non-softfloat paths (softfloat flags need updating) */
@@ -553,7 +549,5 @@ function accrue_fflags(flags) = {
  fcsr->FFLAGS() = f;
  update_softfloat_fflags(f);
  dirty_fd_context_if_present();
- if get_config_print_reg()
- then print("fcsr.FFLAGS <- " ^ BitStr(flags))
  }
 }

model/riscv_insts_vext_fp.sail

@@ -861,7 +861,11 @@ function clause execute(VFMVFS(vs2, rd)) = {
  let 'm = SEW;
 
  let vs2_val : vector('n, dec, bits('m)) = read_vreg(num_elem, SEW, 0, vs2);
- F(rd) = nan_box_vector(vs2_val[0]);
+ match 'm {
+ 16 => F_H(rd) = vs2_val[0],
+ 32 => F_S(rd) = vs2_val[0],
+ 64 => F_D(rd) = vs2_val[0]
+ };
  vstart = zeros();
 
  RETIRE_SUCCESS

model/riscv_insts_vext_utils.sail

@@ -478,25 +478,6 @@ function canonical_NaN('m) = {
  }
 }
 
-/* Floating point NaN boxing / unboxing that support 16-bit to 64-bit types */
-val nan_box_vector : forall 'm, ('m in {16, 32, 64} & 'm <= flen). bits('m) -> flenbits
-function nan_box_vector(unboxed) = {
- match 'm {
- 16 => nan_box(unboxed),
- 32 => nan_box(unboxed),
- 64 => unboxed
- }
-}
-
-val nan_unbox_vector : forall 'm, ('m in {16, 32, 64} & 'm <= flen). (flenbits, int('m)) -> bits('m)
-function nan_unbox_vector(regval, 'm) = {
- match 'm {
- 16 => nan_unbox(regval),
- 32 => nan_unbox(regval),
- 64 => regval
- }
-}
-
 /* Floating point classification functions */
 val f_is_neg_inf : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool
 function f_is_neg_inf(xf) = {
@@ -600,12 +581,11 @@ 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) effect {escape, rreg}
 function get_scalar_fp(rs1, SEW) = {
- if sizeof(flen) >= SEW then {
- /* Least significant SEW bits */
- nan_unbox_vector(F(rs1), SEW)
- } else {
- assert(false, "invalid vector floating-point type width: FLEN < SEW");
- zeros()
+ assert(sizeof(flen) >= SEW, "invalid vector floating-point type width: FLEN < SEW");
+ match SEW {
+ 16 => F_H(rs1),
+ 32 => F_S(rs1),
+ 64 => F_D(rs1)
  }
 }
 

model/riscv_insts_vext_vset.sail

@@ -104,6 +104,9 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
  let LMUL_pow_new = get_lmul_pow();
  let SEW_pow_new = get_sew_pow();
  if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
+ /* Note: Implementations can set vill or trap if the vtype setting is not supported.
+ * TODO: configuration support for both solutions
+ */
  vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
  vl = zeros();
  print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
@@ -117,8 +120,11 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
  let rs1_val = X(rs1);
  let AVL = unsigned(rs1_val);
  vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
- else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) /* ceil(AVL / 2) ≤ vl ≤ VLMAX */
+ else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
  else to_bits(sizeof(xlen), VLMAX);
+ /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
+ * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
+ */
  X(rd) = vl;
  } else if (rd != 0b00000) then { /* set vl to VLMAX */
  let AVL = unsigned(ones(sizeof(xlen)));
@@ -128,6 +134,9 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = {
  let AVL = unsigned(vl);
  let ratio_pow_new = SEW_pow_new - LMUL_pow_new;
  if (ratio_pow_new != ratio_pow_ori) then {
+ /* Note: Implementations can set vill or trap if the vtype setting is not supported.
+ * TODO: configuration support for both solutions
+ */
  vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
  vl = zeros();
  }
@@ -170,6 +179,9 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = {
  let LMUL_pow_new = get_lmul_pow();
  let SEW_pow_new = get_sew_pow();
  if SEW_pow_new > LMUL_pow_new + ELEN_pow then {
+ /* Note: Implementations can set vill or trap if the vtype setting is not supported.
+ * TODO: configuration support for both solutions
+ */
  vtype->bits() = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
  vl = zeros();
  print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
@@ -181,8 +193,11 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = {
 
  /* set vl according to VLMAX and AVL */
  vl = if AVL <= VLMAX then to_bits(sizeof(xlen), AVL)
- else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) /* ceil(AVL / 2) ≤ vl ≤ VLMAX */
+ else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2)
  else to_bits(sizeof(xlen), VLMAX);
+ /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX)
+ * TODO: configuration support for either using ceil(AVL / 2) or VLMAX
+ */
  X(rd) = vl;
  print_reg("CSR vtype <- " ^ BitStr(vtype.bits()));
  print_reg("CSR vl <- " ^ BitStr(vl));

model/riscv_sys_control.sail

@@ -600,6 +600,15 @@ function init_sys() -> unit = {
  minstret_increment = true;
 
  /* initialize vector csrs */
+ elen = 0b1; /* ELEN=64 as default value */
+ /* vlen = ...;
+ * VLEN needs to be manually speficied currently.
+ * See riscv_vlen.sail for details.
+ */
+ vlenb = zero_extend(0b0);
+ /* The value of vlenb is not used currently.
+ * It should be assigned as 2 ^ (get_vlen_pow() - 3) after vlen is speficied.
+ */
  vstart = zero_extend(0b0);
  vxsat = 0b0;
  vxrm = 0b00;
@@ -612,7 +621,6 @@ function init_sys() -> unit = {
  vtype->vta() = 0b0;
  vtype->vsew() = 0b000;
  vtype->vlmul() = 0b000;
- vlenb = zero_extend(0b0);
 
  init_pmp();
 

model/riscv_sys_regs.sail

@@ -211,7 +211,6 @@ function haveZknd() -> bool = true
 
 function haveZmmul() -> bool = true
 function haveRVV() -> bool = misa.V() == 0b1
-/* see below for F and D extension tests */
 
 /* Zicond extension support */
 function haveZicond() -> bool = true

model/riscv_vlen.sail

@@ -44,6 +44,10 @@ function get_elen_pow() = match elen {
  0b0 => 5,
  0b1 => 6
 }
+/* Note: ELEN=32 requires a different encoding of the CSR vtype.
+ * The current version of vtype implementation corresponds to the ELEN=64 configuration.
+ * TODO: the configurarion of ELEN and its corresponding vtype implementations.
+ */
 
 register vlen : bits(4)