riscv · billmcspadden-riscv · Jan 31, 2024 · Dec 12, 2023 · Dec 12, 2023
diff --git a/Makefile b/Makefile
@@ -255,9 +255,11 @@ gcovr:
 ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml
  ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@
 
+c_preserve_fns=-c_preserve _set_Misa_C
+
 generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
  mkdir -p generated_definitions/c
- $(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
+ $(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@)
 
 generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile
  mkdir -p generated_definitions/c2
@@ -296,7 +298,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
 # sed -i isn't posix compliant, unfortunately
 generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
  mkdir -p generated_definitions/c
- $(SAIL) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
+ $(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
  sed -e '/^[[:space:]]*$$/d' $@ > $@.new
  mv $@.new $@
 

diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
@@ -83,12 +83,12 @@ 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 (zero_extend (fcsr.FFLAGS()))
-function clause ext_read_CSR (0x002) = Some (zero_extend (fcsr.FRM()))
-function clause ext_read_CSR (0x003) = Some (zero_extend (fcsr.bits()))
+function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS]))
+function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM]))
+function clause ext_read_CSR (0x003) = Some(zero_extend(fcsr.bits))
 
-function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(zero_extend(fcsr.FFLAGS())) }
-function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(zero_extend(fcsr.FRM())) }
-function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(zero_extend(fcsr.bits())) }
+function clause ext_write_CSR (0x001, value) = { ext_write_fcsr(fcsr[FRM], value[4..0]); Some(zero_extend(fcsr[FFLAGS])) }
+function clause ext_write_CSR (0x002, value) = { ext_write_fcsr(value[2..0], fcsr[FFLAGS]); Some(zero_extend(fcsr[FRM])) }
+function clause ext_write_CSR (0x003, value) = { ext_write_fcsr(value[7..5], value[4..0]); Some(zero_extend(fcsr.bits)) }
 
 /* **************************************************************** */
diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
@@ -165,8 +165,8 @@ register f31 : fregtype
 
 function dirty_fd_context() -> unit = {
  assert(sys_enable_fdext());
- mstatus->FS() = extStatus_to_bits(Dirty);
- mstatus->SD() = 0b1
+ mstatus[FS] = extStatus_to_bits(Dirty);
+ mstatus[SD] = 0b1
 }
 
 function dirty_fd_context_if_present() -> unit = {
@@ -526,18 +526,18 @@ register fcsr : Fcsr
 
 val ext_write_fcsr : (bits(3), bits(5)) -> unit
 function ext_write_fcsr (frm, fflags) = {
- fcsr->FRM() = frm; /* Note: frm can be an illegal value, 101, 110, 111 */
- fcsr->FFLAGS() = fflags;
+ fcsr[FRM] = frm; /* Note: frm can be an illegal value, 101, 110, 111 */
+ fcsr[FFLAGS] = fflags;
  dirty_fd_context_if_present();
 }
 
 /* OR flags into the fflags register. */
 val accrue_fflags : (bits(5)) -> unit
 function accrue_fflags(flags) = {
- let f = fcsr.FFLAGS() | flags;
- if fcsr.FFLAGS() != f
+ let f = fcsr[FFLAGS] | flags;
+ if fcsr[FFLAGS] != f
  then {
- fcsr->FFLAGS() = f;
+ fcsr[FFLAGS] = f;
  dirty_fd_context_if_present();
  }
 }
diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail
@@ -69,10 +69,10 @@
 /*=======================================================================================*/
 
 function fetch() -> FetchResult = {
- rvfi_inst_data->rvfi_order()  = minstret;
- rvfi_pc_data->rvfi_pc_rdata() = zero_extend(get_arch_pc());
- rvfi_inst_data->rvfi_mode() = zero_extend(privLevel_to_bits(cur_privilege));
- rvfi_inst_data->rvfi_ixl() = zero_extend(misa.MXL());
+ rvfi_inst_data[rvfi_order] = minstret;
+ rvfi_pc_data[rvfi_pc_rdata] = zero_extend(get_arch_pc());
+ rvfi_inst_data[rvfi_mode] = zero_extend(privLevel_to_bits(cur_privilege));
+ rvfi_inst_data[rvfi_ixl] = zero_extend(misa[MXL]);
 
  /* First allow extensions to check pc */
  match ext_fetch_check_pc(PC, PC) {
@@ -84,7 +84,7 @@ function fetch() -> FetchResult = {
  else match translateAddr(use_pc, Execute()) {
  TR_Failure(e, _) => F_Error(e, PC),
  TR_Address(_, _) => {
- let i = rvfi_instruction.rvfi_insn();
+ let i = rvfi_instruction[rvfi_insn];
  rvfi_inst_data->rvfi_insn() = zero_extend(i);
  if (i[1 .. 0] != 0b11)
  then F_RVC(i[15 .. 0])

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
@@ -789,7 +789,7 @@ mapping clause encdec = SRET()
 function clause execute SRET() = {
  let sret_illegal : bool = match cur_privilege {
  User => true,
- Supervisor => not(haveSupMode ()) | mstatus.TSR() == 0b1,
+ Supervisor => not(haveSupMode ()) | mstatus[TSR] == 0b1,
  Machine => not(haveSupMode ())
  };
  if sret_illegal
@@ -826,7 +826,7 @@ mapping clause encdec = WFI()
 function clause execute WFI() =
  match cur_privilege {
  Machine => { platform_wfi(); RETIRE_SUCCESS },
- Supervisor => if mstatus.TW() == 0b1
+ Supervisor => if mstatus[TW] == 0b1
  then { handle_illegal(); RETIRE_FAIL }
  else { platform_wfi(); RETIRE_SUCCESS },
  User => { handle_illegal(); RETIRE_FAIL }
@@ -845,7 +845,7 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
  let asid : option(xlenbits) = if rs2 == 0b00000 then None() else Some(X(rs2));
  match cur_privilege {
  User => { handle_illegal(); RETIRE_FAIL },
- Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) {
+ Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus[TVM]) {
  (Some(_), 0b1) => { handle_illegal(); RETIRE_FAIL },
  (Some(_), 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
  (_, _) => internal_error(__FILE__, __LINE__, "unimplemented sfence architecture")

diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail
@@ -71,7 +71,7 @@
 /* ********************************************************************* */
 /* This file specifies the compressed floating-point instructions.
  *
- * These instructions are only legal if misa.C() and misa.D()
+ * These instructions are only legal if misa[C] and misa[D]
  * are set.
  */
 

diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
@@ -71,7 +71,7 @@
 /* ********************************************************************* */
 /* This file specifies the compressed instructions in the 'C' extension. */
 
-/* These instructions are only legal if misa.C() is true. Instead of
+/* These instructions are only legal if misa[C] is true. Instead of
  * checking this in every execute clause, we currently do the check in one place
  * in the fetch-execute logic.
  */

diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail
@@ -71,7 +71,7 @@
 /* ********************************************************************* */
 /* This file specifies the compressed floating-point instructions.
  *
- * These instructions are only legal if misa.C() and misa.F()
+ * These instructions are only legal if misa[C] and misa[F]
  * are set.
  */
 

diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
@@ -112,7 +112,7 @@ val select_instr_or_fcsr_rm : rounding_mode -> option(rounding_mode)
 function select_instr_or_fcsr_rm instr_rm =
  if (instr_rm == RM_DYN)
  then {
- let fcsr_rm = fcsr.FRM();
+ let fcsr_rm = fcsr[FRM];
  if (valid_rounding_mode(fcsr_rm) & fcsr_rm != encdec_rounding_mode(RM_DYN))
  then Some(encdec_rounding_mode(fcsr_rm)) else None()
  }

diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail
@@ -61,7 +61,7 @@ mapping clause encdec = FVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
  <-> encdec_fvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FVVTYPE(funct6, vm, vs2, vs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -136,7 +136,7 @@ mapping clause encdec = FVVMATYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
  <-> encdec_fvvmafunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FVVMATYPE(funct6, vm, vs2, vs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -203,7 +203,7 @@ mapping clause encdec = FWVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
  <-> encdec_fwvvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FWVVTYPE(funct6, vm, vs2, vs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -268,7 +268,7 @@ mapping clause encdec = FWVVMATYPE(funct6, vm, vs1, vs2, vd) if haveVExt()
  <-> encdec_fwvvmafunct6(funct6) @ vm @ vs1 @ vs2 @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FWVVMATYPE(funct6, vm, vs1, vs2, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -332,7 +332,7 @@ mapping clause encdec = FWVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
  <-> encdec_fwvfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FWVTYPE(funct6, vm, vs2, vs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -395,7 +395,7 @@ mapping clause encdec = VFUNARY0(vm, vs2, vfunary0, vd) if haveVExt()
  <-> 0b010010 @ vm @ vs2 @ encdec_vfunary0_vs1(vfunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -508,7 +508,7 @@ mapping clause encdec = VFWUNARY0(vm, vs2, vfwunary0, vd) if haveVExt()
  <-> 0b010010 @ vm @ vs2 @ encdec_vfwunary0_vs1(vfwunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(VFWUNARY0(vm, vs2, vfwunary0, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -638,7 +638,7 @@ mapping clause encdec = VFNUNARY0(vm, vs2, vfnunary0, vd) if haveVExt()
  <-> 0b010010 @ vm @ vs2 @ encdec_vfnunary0_vs1(vfnunary0) @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -773,7 +773,7 @@ mapping clause encdec = VFUNARY1(vm, vs2, vfunary1, vd) if haveVExt()
  <-> 0b010011 @ vm @ vs2 @ encdec_vfunary1_vs1(vfunary1) @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(VFUNARY1(vm, vs2, vfunary1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -849,7 +849,7 @@ mapping clause encdec = VFMVFS(vs2, rd) if haveVExt()
  <-> 0b010000 @ 0b1 @ vs2 @ 0b00000 @ 0b001 @ rd @ 0b1010111 if haveVExt()
 
 function clause execute(VFMVFS(vs2, rd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let num_elem = get_num_elem(0, SEW);
 
@@ -897,7 +897,7 @@ mapping clause encdec = FVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
  <-> encdec_fvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FVFTYPE(funct6, vm, vs2, rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -987,7 +987,7 @@ mapping clause encdec = FVFMATYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
  <-> encdec_fvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FVFMATYPE(funct6, vm, vs2, rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -1054,7 +1054,7 @@ mapping clause encdec = FWVFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
  <-> encdec_fwvffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FWVFTYPE(funct6, vm, vs2, rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -1118,7 +1118,7 @@ mapping clause encdec = FWVFMATYPE(funct6, vm, rs1, vs2, vd) if haveVExt()
  <-> encdec_fwvfmafunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FWVFMATYPE(funct6, vm, rs1, vs2, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -1181,7 +1181,7 @@ mapping clause encdec = FWFTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
  <-> encdec_fwffunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FWFTYPE(funct6, vm, vs2, rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -1235,7 +1235,7 @@ mapping clause encdec = VFMERGE(vs2, rs1, vd) if haveVExt()
  <-> 0b010111 @ 0b0 @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(VFMERGE(vs2, rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let start_element = get_start_element();
  let end_element = get_end_element();
  let SEW = get_sew();
@@ -1286,7 +1286,7 @@ mapping clause encdec = VFMV(rs1, vd) if haveVExt()
  <-> 0b010111 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(VFMV(rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -1324,7 +1324,7 @@ mapping clause encdec = VFMVSF(rs1, vd) if haveVExt()
  <-> 0b010000 @ 0b1 @ 0b00000 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(VFMVSF(rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let num_elem = get_num_elem(0, SEW);
 

diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail
@@ -190,7 +190,7 @@ mapping clause encdec = RFVVTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
 
 val process_rfvv_single: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired
 function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */
 
  if illegal_fp_reduction(SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL };
@@ -229,7 +229,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
 
 val process_rfvv_widen: forall 'n 'm 'p, 'n >= 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired
 function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW_widen = SEW * 2;
  let LMUL_pow_widen = LMUL_pow + 1;
  let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */

diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
@@ -63,7 +63,7 @@ function valid_eew_emul(EEW, EMUL_pow) = {
  */
 val valid_vtype : unit -> bool
 function valid_vtype() = {
- vtype.vill() == 0b0
+ vtype[vill] == 0b0
 }
 
 /* Check for vstart value */
@@ -643,7 +643,7 @@ function signed_saturation(len, elem) = {
 
 /* Get the floating point rounding mode from csr fcsr */
 val get_fp_rounding_mode : unit -> rounding_mode
-function get_fp_rounding_mode() = encdec_rounding_mode(fcsr.FRM())
+function get_fp_rounding_mode() = encdec_rounding_mode(fcsr[FRM])
 
 /* Negate a floating point number */
 val negate_fp : forall 'm, 'm in {16, 32, 64}. bits('m) -> bits('m)
@@ -863,7 +863,7 @@ function fp_class(xf) = {
 
 val fp_widen : forall 'm, 'm in {16, 32}. bits('m) -> bits('m * 2)
 function fp_widen(nval) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let (fflags, wval) : (bits_fflags, bits('m * 2)) = match 'm {
  16 => riscv_f16ToF32(rm_3b, nval),
  32 => riscv_f32ToF64(rm_3b, nval)

diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail
@@ -767,7 +767,7 @@ mapping clause encdec = FVVMTYPE(funct6, vm, vs2, vs1, vd) if haveVExt()
  <-> encdec_fvvmfunct6(funct6) @ vm @ vs2 @ vs1 @ 0b001 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);
@@ -831,7 +831,7 @@ mapping clause encdec = FVFMTYPE(funct6, vm, vs2, rs1, vd) if haveVExt()
  <-> encdec_fvfmfunct6(funct6) @ vm @ vs2 @ rs1 @ 0b101 @ vd @ 0b1010111 if haveVExt()
 
 function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
- let rm_3b = fcsr.FRM();
+ let rm_3b = fcsr[FRM];
  let SEW = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);