diff options
| author | Alasdair <alasdair.armstrong@cl.cam.ac.uk> | 2023-12-12 14:55:37 +0000 |
|---|---|---|
| committer | Bill McSpadden <bill@riscv.org> | 2024-01-31 12:38:33 -0600 |
| commit | 563446c477f5e905df905e0d30371a2c4d51d7a5 (patch) | |
| tree | d0f503b96366666ad97eea2a4ba4cbe748e82326 | |
| parent | d7a3d8012fd579f40e53a29569141d72dd5e0c32 (diff) | |
| download | sail-riscv-563446c477f5e905df905e0d30371a2c4d51d7a5.zip sail-riscv-563446c477f5e905df905e0d30371a2c4d51d7a5.tar.gz sail-riscv-563446c477f5e905df905e0d30371a2c4d51d7a5.tar.bz2 | |
Update bitfield syntax
Use newer bitfield syntax, which has been part of Sail for
a while now. Should in theory be more efficient as it removes
a level of indirection for bitfield accesses.
It's also much more friendly to `sail -fmt`, which has no idea
how to handle the old bitfield syntax.
36 files changed, 506 insertions, 504 deletions
@@ -247,9 +247,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 @@ -288,7 +290,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 index 563d600..4ea958f 100644 --- 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 index 7958016..d7786f3 100644 --- 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 index b036c1b..f4567ff 100644 --- 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 index eec5fbd..7d53d99 100644 --- 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 index 8851e34..af0366e 100644 --- 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 index 8b9fa8f..83d0d88 100644 --- 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 index 5380aa2..878bb65 100644 --- 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 index e0ea551..7bfef08 100644 --- 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 index 05f36fd..1c8fe1e 100755 --- 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 index be6afc3..80ee8f2 100755 --- 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 index 45935cb..7b29a0f 100755 --- 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 index b75b079..a144505 100755 --- 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); diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 9600362..263b40b 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -92,11 +92,11 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { /* set vtype */ match op { VSETVLI => { - vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul }, VSETVL => { let rs2 : regidx = sew[1 .. 0] @ lmul; - vtype->bits() = X(rs2) + vtype.bits = X(rs2) } }; @@ -107,9 +107,9 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { /* 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 */ + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); return RETIRE_SUCCESS }; @@ -137,11 +137,11 @@ function clause execute VSET_TYPE(op, ma, ta, sew, lmul, rs1, rd) = { /* 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 */ + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); } }; - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); /* reset vstart to 0 */ @@ -173,7 +173,7 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - vtype->bits() = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; /* check legal SEW and LMUL and calculate VLMAX */ let LMUL_pow_new = get_lmul_pow(); @@ -182,9 +182,9 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { /* 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 */ + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ vl = zeros(); - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); return RETIRE_SUCCESS }; @@ -199,7 +199,7 @@ function clause execute VSETI_TYPE(ma, ta, sew, lmul, uimm, rd) = { * TODO: configuration support for either using ceil(AVL / 2) or VLMAX */ X(rd) = vl; - print_reg("CSR vtype <- " ^ BitStr(vtype.bits())); + print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)); /* reset vstart to 0 */ diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 8953ad4..4be297a 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -91,23 +91,23 @@ function readCSR csr : csreg -> xlenbits = { (0xF12, _) => marchid, (0xF13, _) => mimpid, (0xF14, _) => mhartid, - (0x300, _) => mstatus.bits(), - (0x301, _) => misa.bits(), - (0x302, _) => medeleg.bits(), - (0x303, _) => mideleg.bits(), - (0x304, _) => mie.bits(), + (0x300, _) => mstatus.bits, + (0x301, _) => misa.bits, + (0x302, _) => medeleg.bits, + (0x303, _) => mideleg.bits, + (0x304, _) => mie.bits, (0x305, _) => get_mtvec(), - (0x306, _) => zero_extend(mcounteren.bits()), - (0x30A, _) => menvcfg.bits()[sizeof(xlen) - 1 .. 0], - (0x310, 32) => mstatush.bits(), - (0x31A, 32) => menvcfg.bits()[63 .. 32], - (0x320, _) => zero_extend(mcountinhibit.bits()), + (0x306, _) => zero_extend(mcounteren.bits), + (0x30A, _) => menvcfg.bits[sizeof(xlen) - 1 .. 0], + (0x310, 32) => mstatush.bits, + (0x31A, 32) => menvcfg.bits[63 .. 32], + (0x320, _) => zero_extend(mcountinhibit.bits), (0x340, _) => mscratch, (0x341, _) => get_xret_target(Machine) & pc_alignment_mask(), - (0x342, _) => mcause.bits(), + (0x342, _) => mcause.bits, (0x343, _) => mtval, - (0x344, _) => mip.bits(), + (0x344, _) => mip.bits, (0x3A0, _) => pmpReadCfgReg(0), // pmpcfg0 (0x3A1, 32) => pmpReadCfgReg(1), // pmpcfg1 @@ -141,27 +141,27 @@ function readCSR csr : csreg -> xlenbits = { (0x008, _) => zero_extend(vstart), (0x009, _) => zero_extend(vxsat), (0x00A, _) => zero_extend(vxrm), - (0x00F, _) => zero_extend(vcsr.bits()), + (0x00F, _) => zero_extend(vcsr.bits), (0xC20, _) => vl, - (0xC21, _) => vtype.bits(), + (0xC21, _) => vtype.bits, (0xC22, _) => vlenb, /* trigger/debug */ (0x7a0, _) => ~(tselect), /* this indicates we don't have any trigger support */ /* supervisor mode */ - (0x100, _) => lower_mstatus(mstatus).bits(), - (0x102, _) => sedeleg.bits(), - (0x103, _) => sideleg.bits(), - (0x104, _) => lower_mie(mie, mideleg).bits(), + (0x100, _) => lower_mstatus(mstatus).bits, + (0x102, _) => sedeleg.bits, + (0x103, _) => sideleg.bits, + (0x104, _) => lower_mie(mie, mideleg).bits, (0x105, _) => get_stvec(), - (0x106, _) => zero_extend(scounteren.bits()), - (0x10A, _) => senvcfg.bits()[sizeof(xlen) - 1 .. 0], + (0x106, _) => zero_extend(scounteren.bits), + (0x10A, _) => senvcfg.bits[sizeof(xlen) - 1 .. 0], (0x140, _) => sscratch, (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(), - (0x142, _) => scause.bits(), + (0x142, _) => scause.bits, (0x143, _) => stval, - (0x144, _) => lower_mip(mip, mideleg).bits(), + (0x144, _) => lower_mip(mip, mideleg).bits, (0x180, _) => satp, /* user mode counters */ @@ -191,23 +191,23 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { let res : option(xlenbits) = match (csr, sizeof(xlen)) { /* machine mode */ - (0x300, _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) }, - (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits()) }, - (0x302, _) => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits()) }, - (0x303, _) => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) }, - (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, + (0x300, _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits) }, + (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits) }, + (0x302, _) => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits) }, + (0x303, _) => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits) }, + (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits) }, (0x305, _) => { Some(set_mtvec(value)) }, - (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) }, - (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) }, - (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) }, - (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now - (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) }, - (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) }, + (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits)) }, + (0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) }, + (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits) }, + (0x310, 32) => { Some(mstatush.bits) }, // ignore writes for now + (0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) }, + (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits)) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, - (0x342, _) => { mcause->bits() = value; Some(mcause.bits()) }, + (0x342, _) => { mcause.bits = value; Some(mcause.bits) }, (0x343, _) => { mtval = value; Some(mtval) }, - (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits()) }, + (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits) }, // Note: Some(value) returned below is not the legalized value due to locked entries (0x3A0, _) => { pmpWriteCfgReg(0, value); Some(pmpReadCfgReg(0)) }, // pmpcfg0 @@ -242,18 +242,18 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x7a0, _) => { tselect = value; Some(tselect) }, /* supervisor mode */ - (0x100, _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits()) }, - (0x102, _) => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) }, - (0x103, _) => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */ - (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, + (0x100, _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits) }, + (0x102, _) => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits) }, + (0x103, _) => { sideleg.bits = value; Some(sideleg.bits) }, /* TODO: does this need legalization? */ + (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits) }, (0x105, _) => { Some(set_stvec(value)) }, - (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) }, - (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) }, + (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits)) }, + (0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, - (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, + (0x142, _) => { scause.bits = value; Some(scause.bits) }, (0x143, _) => { stval = value; Some(stval) }, - (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) }, + (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) }, (0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, /* user mode: seed (entropy source). writes are ignored */ @@ -263,9 +263,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x008, _) => { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); Some(zero_extend(vstart)) }, (0x009, _) => { vxsat = value[0 .. 0]; Some(zero_extend(vxsat)) }, (0x00A, _) => { vxrm = value[1 .. 0]; Some(zero_extend(vxrm)) }, - (0x00F, _) => { vcsr->bits() = value[2 ..0]; Some(zero_extend(vcsr.bits())) }, + (0x00F, _) => { vcsr.bits = value[2 ..0]; Some(zero_extend(vcsr.bits)) }, (0xC20, _) => { vl = value; Some(vl) }, - (0xC21, _) => { vtype->bits() = value; Some(vtype.bits()) }, + (0xC21, _) => { vtype.bits = value; Some(vtype.bits) }, (0xC22, _) => { vlenb = value; Some(vlenb) }, _ => ext_write_CSR(csr, value) diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 0f36dee..2df6192 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -158,13 +158,13 @@ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_ $ifdef RVFI_DII val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit function rvfi_read (addr, width, result) = { - rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { /* TODO: report tag bit for capability writes and extend mask by one bit. */ MemValue(v, _) => if width <= 16 - then { rvfi_mem_data->rvfi_mem_rdata() = sail_zero_extend(v, 256); - rvfi_mem_data->rvfi_mem_rmask() = rvfi_encode_width_mask(width) } + then { rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(v, 256); + rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width) } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") }, MemException(_) => () }; @@ -232,14 +232,14 @@ function mem_write_ea (addr, width, aq, rl, con) = { $ifdef RVFI_DII val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit function rvfi_write (addr, width, value, meta, result) = { - rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; match result { /* Log only the memory address (without the value) if the write fails. */ MemValue(_) => if width <= 16 then { /* TODO: report tag bit for capability writes and extend mask by one bit. */ - rvfi_mem_data->rvfi_mem_wdata() = sail_zero_extend(value,256); - rvfi_mem_data->rvfi_mem_wmask() = rvfi_encode_width_mask(width); + rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value,256); + rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width); } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); }, diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 432fd0d..796d9df 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -79,24 +79,24 @@ function clause ext_is_CSR_defined(0x042, _) = haveUsrMode() & haveNExt() // uca function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() & haveNExt() // utval function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() & haveNExt() // uip -function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits()) -function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits()) +function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits) +function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits) function clause ext_read_CSR(0x005) = Some(get_utvec()) function clause ext_read_CSR(0x040) = Some(uscratch) function clause ext_read_CSR(0x041) = Some(get_xret_target(User) & pc_alignment_mask()) -function clause ext_read_CSR(0x042) = Some(ucause.bits()) +function clause ext_read_CSR(0x042) = Some(ucause.bits) function clause ext_read_CSR(0x043) = Some(utval) -function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits()) +function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits) -function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits()) } +function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits) } function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value); mie = lift_sie(mie, mideleg, sie); - Some(mie.bits()) } + Some(mie.bits) } function clause ext_write_CSR(0x005, value) = { Some(set_utvec(value)) } function clause ext_write_CSR(0x040, value) = { uscratch = value; Some(uscratch) } function clause ext_write_CSR(0x041, value) = { Some(set_xret_target(User, value)) } -function clause ext_write_CSR(0x042, value) = { ucause->bits() = value; Some(ucause.bits()) } +function clause ext_write_CSR(0x042, value) = { ucause.bits = value; Some(ucause.bits) } function clause ext_write_CSR(0x043, value) = { utval = value; Some(utval) } function clause ext_write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value); mip = lift_sip(mip, mideleg, sip); - Some(mip.bits()) } + Some(mip.bits) } diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail index b078bf8..c0c584b 100644 --- a/model/riscv_next_regs.sail +++ b/model/riscv_next_regs.sail @@ -79,14 +79,14 @@ bitfield Ustatus : xlenbits = { /* This is a view, so there is no register defined. */ function lower_sstatus(s : Sstatus) -> Ustatus = { let u = Mk_Ustatus(zero_extend(0b0)); - let u = update_UPIE(u, s.UPIE()); - let u = update_UIE(u, s.UIE()); + let u = update_UPIE(u, s[UPIE]); + let u = update_UIE(u, s[UIE]); u } function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = { - let s = update_UPIE(s, u.UPIE()); - let s = update_UIE(s, u.UIE()); + let s = update_UPIE(s, u[UPIE]); + let s = update_UIE(s, u[UIE]); s } @@ -107,25 +107,25 @@ bitfield Uinterrupts : xlenbits = { /* Provides the uip read view of sip (s) as delegated by sideleg (d). */ function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); - let u = update_UEI(u, s.UEI() & d.UEI()); - let u = update_UTI(u, s.UTI() & d.UTI()); - let u = update_USI(u, s.USI() & d.USI()); + let u = update_UEI(u, s[UEI] & d[UEI]); + let u = update_UTI(u, s[UTI] & d[UTI]); + let u = update_USI(u, s[USI] & d[USI]); u } /* Provides the uie read view of sie as delegated by sideleg. */ function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); - let u = update_UEI(u, s.UEI() & d.UEI()); - let u = update_UTI(u, s.UTI() & d.UTI()); - let u = update_USI(u, s.USI() & d.USI()); + let u = update_UEI(u, s[UEI] & d[UEI]); + let u = update_UTI(u, s[UTI] & d[UTI]); + let u = update_USI(u, s[USI] & d[USI]); u } /* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */ function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { let s : Sinterrupts = o; - let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s; + let s = if d[USI] == 0b1 then update_USI(s, u[USI]) else s; s } @@ -136,9 +136,9 @@ function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterr /* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */ function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = { let s : Sinterrupts = o; - let s = if d.UEI() == 0b1 then update_UEI(s, u.UEI()) else s; - let s = if d.UTI() == 0b1 then update_UTI(s, u.UTI()) else s; - let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s; + let s = if d[UEI] == 0b1 then update_UEI(s, u[UEI]) else s; + let s = if d[UTI] == 0b1 then update_UTI(s, u[UTI]) else s; + let s = if d[USI] == 0b1 then update_USI(s, u[USI]) else s; s } diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 579a118..f9637fe 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -219,8 +219,8 @@ function clint_load(t, addr, width) = { if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { if get_config_print_platform() - then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI())); - MemValue(sail_zero_extend(mip.MSI(), sizeof(8 * 'n))) + then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip[MSI])); + MemValue(sail_zero_extend(mip[MSI], sizeof(8 * 'n))) } else if addr == MTIMECMP_BASE & ('n == 4) then { @@ -275,11 +275,11 @@ function clint_load(t, addr, width) = { function clint_dispatch() -> unit = { if get_config_print_platform() then print_platform("clint::tick mtime <- " ^ BitStr(mtime)); - mip->MTI() = 0b0; + mip[MTI] = 0b0; if mtimecmp <=_u mtime then { if get_config_print_platform() then print_platform(" clint timer pending at mtime " ^ BitStr(mtime)); - mip->MTI() = 0b1 + mip[MTI] = 0b1 } } @@ -290,7 +290,7 @@ function clint_store(addr, width, data) = { if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { if get_config_print_platform() then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")"); - mip->MSI() = [data[0]]; + mip[MSI] = [data[0]]; clint_dispatch(); MemValue(true) } else if addr == MTIMECMP_BASE & 'n == 8 then { @@ -320,7 +320,7 @@ function clint_store(addr, width, data) = { val tick_clock : unit -> unit function tick_clock() = { - if mcountinhibit.CY() == 0b0 + if mcountinhibit[CY] == 0b0 then mcycle = mcycle + 1; mtime = mtime + 1; @@ -416,23 +416,23 @@ function htif_store(paddr, width, data) = { | (unsigned(htif_payload_writes) > 2)) then { let cmd = Mk_htif_cmd(htif_tohost); - match cmd.device() { + match cmd[device] { 0x00 => { /* syscall-proxy */ if get_config_print_platform() - then print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload())); - if cmd.payload()[0] == bitone + then print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd[payload])); + if cmd[payload][0] == bitone then { htif_done = true; - htif_exit_code = (sail_zero_extend(cmd.payload(), 64) >> 1) + htif_exit_code = (sail_zero_extend(cmd[payload], 64) >> 1) } else () }, 0x01 => { /* terminal */ if get_config_print_platform() - then print_platform("htif-term cmd: " ^ BitStr(cmd.payload())); - match cmd.cmd() { + then print_platform("htif-term cmd: " ^ BitStr(cmd[payload])); + match cmd[cmd] { 0x00 => /* TODO: terminal input handling */ (), - 0x01 => plat_term_write(cmd.payload()[7..0]), + 0x01 => plat_term_write(cmd[payload][7..0]), c => print("Unknown term cmd: " ^ BitStr(c)) }; /* reset to ack */ diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 998fb92..e95dfa1 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -77,7 +77,7 @@ type pmp_addr_range = option((xlenbits, xlenbits)) function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range = { - match pmpAddrMatchType_of_bits(cfg.A()) { + match pmpAddrMatchType_of_bits(cfg[A]) { OFF => None(), TOR => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) }, NA4 => { // TODO: I find the spec unclear for entries marked NA4 and G = 1. @@ -99,10 +99,10 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits val pmpCheckRWX: (Pmpcfg_ent, AccessType(ext_access_type)) -> bool function pmpCheckRWX(ent, acc) = { match acc { - Read(_) => ent.R() == 0b1, - Write(_) => ent.W() == 0b1, - ReadWrite(_) => ent.R() == 0b1 & ent.W() == 0b1, - Execute() => ent.X() == 0b1 + Read(_) => ent[R] == 0b1, + Write(_) => ent[W] == 0b1, + ReadWrite(_) => ent[R] == 0b1 & ent[W] == 0b1, + Execute() => ent[X] == 0b1 } } diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 9b6355c..04ab309 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -144,25 +144,25 @@ val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits function pmpReadCfgReg(n) = { if sizeof(xlen) == 32 then match n { - 0 => append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))), - 1 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), pmp4cfg.bits()))), - 2 => append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))), - 3 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), pmp12cfg.bits()))), + 0 => append(pmp3cfg.bits, append(pmp2cfg.bits, append(pmp1cfg.bits, pmp0cfg.bits))), + 1 => append(pmp7cfg.bits, append(pmp6cfg.bits, append(pmp5cfg.bits, pmp4cfg.bits))), + 2 => append(pmp11cfg.bits, append(pmp10cfg.bits, append(pmp9cfg.bits, pmp8cfg.bits))), + 3 => append(pmp15cfg.bits, append(pmp14cfg.bits, append(pmp13cfg.bits, pmp12cfg.bits))), _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read") } else match n { // sizeof(xlen) >= 64 - 0 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), append(pmp4cfg.bits(), append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))))))), - 2 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), append(pmp12cfg.bits(), append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))))))), + 0 => append(pmp7cfg.bits, append(pmp6cfg.bits, append(pmp5cfg.bits, append(pmp4cfg.bits, append(pmp3cfg.bits, append(pmp2cfg.bits, append(pmp1cfg.bits, pmp0cfg.bits))))))), + 2 => append(pmp15cfg.bits, append(pmp14cfg.bits, append(pmp13cfg.bits, append(pmp12cfg.bits, append(pmp11cfg.bits, append(pmp10cfg.bits, append(pmp9cfg.bits, pmp8cfg.bits))))))), _ => internal_error(__FILE__, __LINE__, "Unexpected pmp config reg read") } } /* Helpers to handle locked entries */ function pmpLocked(cfg: Pmpcfg_ent) -> bool = - cfg.L() == 0b1 + cfg[L] == 0b1 function pmpTORLocked(cfg: Pmpcfg_ent) -> bool = - (cfg.L() == 0b1) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR) + (cfg[L] == 0b1) & (pmpAddrMatchType_of_bits(cfg[A]) == TOR) function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = if pmpLocked(cfg) then cfg diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index 90345cc..72de8ce 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -101,12 +101,12 @@ bitfield PTE_Bits : pteAttribs = { function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = { let a = Mk_PTE_Bits(p); - a.R() == 0b0 & a.W() == 0b0 & a.X() == 0b0 + a[R] == 0b0 & a[W] == 0b0 & a[X] == 0b0 } function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = { let a = Mk_PTE_Bits(p); - a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) + a[V] == 0b0 | (a[W] == 0b1 & a[R] == 0b0) } union PTE_Check = { @@ -123,29 +123,29 @@ function to_pte_check(b : bool) -> PTE_Check = */ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = { match (ac, priv) { - (Read(_), User) => to_pte_check(p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1), - (ReadWrite(_, _), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Execute(), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1), + (Read(_), User) => to_pte_check(p[U] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Write(_), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1), + (ReadWrite(_, _), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Execute(), User) => to_pte_check(p[U] == 0b1 & p[X] == 0b1), - (Read(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Write(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1), - (ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))), - (Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1), + (Read(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Write(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1), + (ReadWrite(_, _), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))), + (Execute(), Supervisor) => to_pte_check(p[U] == 0b0 & p[X] == 0b1), (_, Machine) => internal_error(__FILE__, __LINE__, "m-mode mem perm check") } } function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = { - let update_d = p.D() == 0b0 & (match a { // dirty-bit + let update_d = p[D] == 0b0 & (match a { // dirty-bit Execute() => false, Read() => false, Write(_) => true, ReadWrite(_,_) => true }); - let update_a = p.A() == 0b0; // accessed-bit + let update_a = p[A] == 0b0; // accessed-bit if update_d | update_a then { let np = update_A(p, 0b1); let np = if update_d then update_D(np, 0b1) else np; diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index 15e7613..7890a11 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -154,8 +154,8 @@ function rX r = { $ifdef RVFI_DII val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit function rvfi_wX (r,v) = { - rvfi_int_data->rvfi_rd_wdata() = zero_extend(v); - rvfi_int_data->rvfi_rd_addr() = to_bits(8,r); + rvfi_int_data[rvfi_rd_wdata] = zero_extend(v); + rvfi_int_data[rvfi_rd_addr] = to_bits(8,r); rvfi_int_data_present = true; } $else diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 550f11a..a71d855 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -83,7 +83,7 @@ function step(step_no : int) -> bool = { * written. See the note near the minstret declaration for more * information. */ - minstret_increment = mcountinhibit.IR() == 0b0; + minstret_increment = mcountinhibit[IR] == 0b0; let (retired, stepped) : (Retired, bool) = match dispatchInterrupt(cur_privilege) { diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 3830725..94e8a4c 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -175,17 +175,17 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) = & (privLevel_to_bits(p) >=_u csrpr) /* privilege */ function check_TVM_SATP(csr : csreg, p : Privilege) -> bool = - not(csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1) + not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1) function check_Counteren(csr : csreg, p : Privilege) -> bool = match(csr, p) { - (0xC00, Supervisor) => mcounteren.CY() == 0b1, - (0xC01, Supervisor) => mcounteren.TM() == 0b1, - (0xC02, Supervisor) => mcounteren.IR() == 0b1, + (0xC00, Supervisor) => mcounteren[CY] == 0b1, + (0xC01, Supervisor) => mcounteren[TM] == 0b1, + (0xC02, Supervisor) => mcounteren[IR] == 0b1, - (0xC00, User) => mcounteren.CY() == 0b1 & (not(haveSupMode()) | scounteren.CY() == 0b1), - (0xC01, User) => mcounteren.TM() == 0b1 & (not(haveSupMode()) | scounteren.TM() == 0b1), - (0xC02, User) => mcounteren.IR() == 0b1 & (not(haveSupMode()) | scounteren.IR() == 0b1), + (0xC00, User) => mcounteren[CY] == 0b1 & (not(haveSupMode()) | scounteren[CY] == 0b1), + (0xC01, User) => mcounteren[TM] == 0b1 & (not(haveSupMode()) | scounteren[TM] == 0b1), + (0xC02, User) => mcounteren[IR] == 0b1 & (not(haveSupMode()) | scounteren[IR] == 0b1), (_, _) => /* no HPM counters for now */ if 0xC03 <=_u csr & csr <=_u 0xC1F @@ -242,10 +242,10 @@ val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Pl */ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { let idx = num_of_ExceptionType(e); - let super = bit_to_bool(medeleg.bits()[idx]); + let super = bit_to_bool(medeleg.bits[idx]); /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */ let user = if haveSupMode() - then super & haveNExt() & bit_to_bool(sedeleg.bits()[idx]) + then super & haveNExt() & bit_to_bool(sedeleg.bits[idx]) else super & haveNExt(); let deleg = if haveUsrMode() & user then User else if haveSupMode() & super then Supervisor @@ -260,15 +260,15 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { */ function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = { let ip = Mk_Minterrupts(ip); - if ip.MEI() == 0b1 then Some(I_M_External) - else if ip.MSI() == 0b1 then Some(I_M_Software) - else if ip.MTI() == 0b1 then Some(I_M_Timer) - else if ip.SEI() == 0b1 then Some(I_S_External) - else if ip.SSI() == 0b1 then Some(I_S_Software) - else if ip.STI() == 0b1 then Some(I_S_Timer) - else if ip.UEI() == 0b1 then Some(I_U_External) - else if ip.USI() == 0b1 then Some(I_U_Software) - else if ip.UTI() == 0b1 then Some(I_U_Timer) + if ip[MEI] == 0b1 then Some(I_M_External) + else if ip[MSI] == 0b1 then Some(I_M_Software) + else if ip[MTI] == 0b1 then Some(I_M_Timer) + else if ip[SEI] == 0b1 then Some(I_S_External) + else if ip[SSI] == 0b1 then Some(I_S_Software) + else if ip[STI] == 0b1 then Some(I_S_Timer) + else if ip[UEI] == 0b1 then Some(I_U_External) + else if ip[USI] == 0b1 then Some(I_U_Software) + else if ip[UTI] == 0b1 then Some(I_U_Timer) else None() } @@ -285,9 +285,9 @@ union interrupt_set = { function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits, priv_enabled : bool) -> interrupt_set = { /* interrupts that are enabled but not delegated are pending */ - let effective_pend = xip.bits() & xie.bits() & (~ (xideleg)); + let effective_pend = xip.bits & xie.bits & (~ (xideleg)); /* the others are delegated */ - let effective_delg = xip.bits() & xideleg; + let effective_delg = xip.bits & xideleg; /* we have pending interrupts if this privilege is enabled */ if priv_enabled & (effective_pend != zero_extend(0b0)) then Ints_Pending(effective_pend) @@ -305,17 +305,17 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits */ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { assert(haveUsrMode(), "no user mode: M/U or M/S/U system required"); - let effective_pending = mip.bits() & mie.bits(); + let effective_pending = mip.bits & mie.bits; if effective_pending == zero_extend(0b0) then None() /* fast path */ else { /* Higher privileges than the current one are implicitly enabled, * while lower privileges are blocked. An unsupported privilege is * considered blocked. */ - let mIE = priv != Machine | (priv == Machine & mstatus.MIE() == 0b1); - let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus.SIE() == 0b1)); - let uIE = haveNExt() & (priv == User & mstatus.UIE() == 0b1); - match processPending(mip, mie, mideleg.bits(), mIE) { + let mIE = priv != Machine | (priv == Machine & mstatus[MIE] == 0b1); + let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus[SIE] == 0b1)); + let uIE = haveNExt() & (priv == User & mstatus[UIE] == 0b1); + match processPending(mip, mie, mideleg.bits, mIE) { Ints_Empty() => None(), Ints_Pending(p) => let r = (p, Machine) in Some(r), Ints_Delegated(d) => @@ -324,7 +324,7 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { else None() } else { /* the delegated bits are pending for S-mode */ - match processPending(Mk_Minterrupts(d), mie, sideleg.bits(), sIE) { + match processPending(Mk_Minterrupts(d), mie, sideleg.bits, sIE) { Ints_Empty() => None(), Ints_Pending(p) => let r = (p, Supervisor) in Some(r), Ints_Delegated(d) => if uIE @@ -345,7 +345,7 @@ function dispatchInterrupt(priv : Privilege) -> option((InterruptType, Privilege */ if not(haveUsrMode()) | (not(haveSupMode()) & not(haveNExt())) then { assert(priv == Machine, "invalid current privilege"); - let enabled_pending = mip.bits() & mie.bits(); + let enabled_pending = mip.bits & mie.bits; match findPendingInterrupt(enabled_pending) { Some(i) => let r = (i, Machine) in Some(r), None() => None() @@ -383,7 +383,7 @@ $ifdef RVFI_DII val rvfi_trap : unit -> unit // TODO: record rvfi_trap_data function rvfi_trap () = - rvfi_inst_data->rvfi_trap() = 0x01 + rvfi_inst_data[rvfi_trap] = 0x01 $else val rvfi_trap : unit -> unit function rvfi_trap () = () @@ -403,12 +403,12 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen match (del_priv) { Machine => { - mcause->IsInterrupt() = bool_to_bits(intr); - mcause->Cause() = zero_extend(c); + mcause[IsInterrupt] = bool_to_bits(intr); + mcause[Cause] = zero_extend(c); - mstatus->MPIE() = mstatus.MIE(); - mstatus->MIE() = 0b0; - mstatus->MPP() = privLevel_to_bits(cur_privilege); + mstatus[MPIE] = mstatus[MIE]; + mstatus[MIE] = 0b0; + mstatus[MPP] = privLevel_to_bits(cur_privilege); mtval = tval(info); mepc = pc; @@ -417,19 +417,19 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); prepare_trap_vector(del_priv, mcause) }, Supervisor => { assert (haveSupMode(), "no supervisor mode present for delegation"); - scause->IsInterrupt() = bool_to_bits(intr); - scause->Cause() = zero_extend(c); + scause[IsInterrupt] = bool_to_bits(intr); + scause[Cause] = zero_extend(c); - mstatus->SPIE() = mstatus.SIE(); - mstatus->SIE() = 0b0; - mstatus->SPP() = match cur_privilege { + mstatus[SPIE] = mstatus[SIE]; + mstatus[SIE] = 0b0; + mstatus[SPP] = match cur_privilege { User => 0b0, Supervisor => 0b1, Machine => internal_error(__FILE__, __LINE__, "invalid privilege for s-mode trap") @@ -442,18 +442,18 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); prepare_trap_vector(del_priv, scause) }, User => { assert(haveUsrMode(), "no user mode present for delegation"); - ucause->IsInterrupt() = bool_to_bits(intr); - ucause->Cause() = zero_extend(c); + ucause[IsInterrupt] = bool_to_bits(intr); + ucause[Cause] = zero_extend(c); - mstatus->UPIE() = mstatus.UIE(); - mstatus->UIE() = 0b0; + mstatus[UPIE] = mstatus[UIE]; + mstatus[UIE] = 0b0; utval = tval(info); uepc = pc; @@ -462,7 +462,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); prepare_trap_vector(del_priv, ucause) } @@ -481,15 +481,15 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, }, (_, CTL_MRET()) => { let prev_priv = cur_privilege; - mstatus->MIE() = mstatus.MPIE(); - mstatus->MPIE() = 0b1; - cur_privilege = privLevel_of_bits(mstatus.MPP()); - mstatus->MPP() = privLevel_to_bits(if haveUsrMode() then User else Machine); + mstatus[MIE] = mstatus[MPIE]; + mstatus[MPIE] = 0b1; + cur_privilege = privLevel_of_bits(mstatus[MPP]); + mstatus[MPP] = privLevel_to_bits(if haveUsrMode() then User else Machine); if cur_privilege != Machine - then mstatus->MPRV() = 0b0; + then mstatus[MPRV] = 0b0; if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -498,15 +498,15 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, }, (_, CTL_SRET()) => { let prev_priv = cur_privilege; - mstatus->SIE() = mstatus.SPIE(); - mstatus->SPIE() = 0b1; - cur_privilege = if mstatus.SPP() == 0b1 then Supervisor else User; - mstatus->SPP() = 0b0; + mstatus[SIE] = mstatus[SPIE]; + mstatus[SPIE] = 0b1; + cur_privilege = if mstatus[SPP] == 0b1 then Supervisor else User; + mstatus[SPP] = 0b0; if cur_privilege != Machine - then mstatus->MPRV() = 0b0; + then mstatus[MPRV] = 0b0; if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -516,12 +516,12 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, }, (_, CTL_URET()) => { let prev_priv = cur_privilege; - mstatus->UIE() = mstatus.UPIE(); - mstatus->UPIE() = 0b1; + mstatus[UIE] = mstatus[UPIE]; + mstatus[UPIE] = 0b1; cur_privilege = User; if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -555,40 +555,40 @@ function init_sys() -> unit = { mhartid = zero_extend(0b0); - misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); - misa->A() = 0b1; /* atomics */ - misa->C() = bool_to_bits(sys_enable_rvc()); /* RVC */ - misa->I() = 0b1; /* base integer ISA */ - misa->M() = 0b1; /* integer multiply/divide */ - misa->U() = 0b1; /* user-mode */ - misa->S() = 0b1; /* supervisor-mode */ - misa->V() = bool_to_bits(sys_enable_vext()); /* vector extension */ + misa[MXL] = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); + misa[A] = 0b1; /* atomics */ + misa[C] = bool_to_bits(sys_enable_rvc()); /* RVC */ + misa[I] = 0b1; /* base integer ISA */ + misa[M] = 0b1; /* integer multiply/divide */ + misa[U] = 0b1; /* user-mode */ + misa[S] = 0b1; /* supervisor-mode */ + misa[V] = bool_to_bits(sys_enable_vext()); /* vector extension */ if sys_enable_fdext() & sys_enable_zfinx() then internal_error(__FILE__, __LINE__, "F and Zfinx cannot both be enabled!"); /* We currently support both F and D */ - misa->F() = bool_to_bits(sys_enable_fdext()); /* single-precision */ - misa->D() = if sizeof(flen) >= 64 + 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 */ else 0b0; - mstatus = set_mstatus_SXL(mstatus, misa.MXL()); - mstatus = set_mstatus_UXL(mstatus, misa.MXL()); - mstatus->SD() = 0b0; + mstatus = set_mstatus_SXL(mstatus, misa[MXL]); + mstatus = set_mstatus_UXL(mstatus, misa[MXL]); + mstatus[SD] = 0b0; /* set to little-endian mode */ if sizeof(xlen) == 64 then { - mstatus = Mk_Mstatus([mstatus.bits() with 37 .. 36 = 0b00]) + mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00]) }; - mstatush->bits() = zero_extend(0b0); - - mip->bits() = zero_extend(0b0); - mie->bits() = zero_extend(0b0); - mideleg->bits() = zero_extend(0b0); - medeleg->bits() = zero_extend(0b0); - mtvec->bits() = zero_extend(0b0); - mcause->bits() = zero_extend(0b0); + mstatush.bits = zero_extend(0b0); + + mip.bits = zero_extend(0b0); + mie.bits = zero_extend(0b0); + mideleg.bits = zero_extend(0b0); + medeleg.bits = zero_extend(0b0); + mtvec.bits = zero_extend(0b0); + mcause.bits = zero_extend(0b0); mepc = zero_extend(0b0); mtval = zero_extend(0b0); mscratch = zero_extend(0b0); @@ -596,13 +596,13 @@ function init_sys() -> unit = { mcycle = zero_extend(0b0); mtime = zero_extend(0b0); - mcounteren->bits() = zero_extend(0b0); + mcounteren.bits = zero_extend(0b0); minstret = zero_extend(0b0); minstret_increment = true; - menvcfg->bits() = zero_extend(0b0); - senvcfg->bits() = zero_extend(0b0); + menvcfg.bits = zero_extend(0b0); + senvcfg.bits = zero_extend(0b0); /* initialize vector csrs */ elen = 0b1; /* ELEN=64 as the common case */ vlen = 0b0100; /* VLEN=512 as a default value */ @@ -613,21 +613,21 @@ function init_sys() -> unit = { vstart = zero_extend(0b0); vxsat = 0b0; vxrm = 0b00; - vcsr->vxrm() = vxrm; - vcsr->vxsat() = vxsat; + vcsr[vxrm] = vxrm; + vcsr[vxsat] = vxsat; vl = zero_extend(0b0); - vtype->vill() = 0b1; - vtype->reserved() = zero_extend(0b0); - vtype->vma() = 0b0; - vtype->vta() = 0b0; - vtype->vsew() = 0b000; - vtype->vlmul() = 0b000; + vtype[vill] = 0b1; + vtype[reserved] = zero_extend(0b0); + vtype[vma] = 0b0; + vtype[vta] = 0b0; + vtype[vsew] = 0b000; + vtype[vlmul] = 0b000; init_pmp(); // log compatibility with spike if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") } /* memory access exceptions, defined here for use by the platform model. */ diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 14cc05c..4dcdd9e 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -125,25 +125,25 @@ function prepare_xret_target(p) = /* other trap-related CSRs */ function get_mtvec() -> xlenbits = - mtvec.bits() + mtvec.bits function get_stvec() -> xlenbits = - stvec.bits() + stvec.bits function get_utvec() -> xlenbits = - utvec.bits() + utvec.bits function set_mtvec(value : xlenbits) -> xlenbits = { mtvec = legalize_tvec(mtvec, value); - mtvec.bits() + mtvec.bits } function set_stvec(value : xlenbits) -> xlenbits = { stvec = legalize_tvec(stvec, value); - stvec.bits() + stvec.bits } function set_utvec(value : xlenbits) -> xlenbits = { utvec = legalize_tvec(utvec, value); - utvec.bits() + utvec.bits } diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 84f708e..d11f611 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -164,26 +164,26 @@ val ext_veto_disable_C : unit -> bool function legalize_misa(m : Misa, v : xlenbits) -> Misa = { let v = Mk_Misa(v); /* Suppress updates to MISA if MISA is not writable or if by disabling C next PC would become misaligned or an extension vetoes */ - if not(sys_enable_writable_misa()) | (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) + if not(sys_enable_writable_misa()) | (v[C] == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) then m else { /* Suppress enabling C if C was disabled at boot (i.e. not supported) */ - let m = if not(sys_enable_rvc()) then m else update_C(m, v.C()); + let m = if not(sys_enable_rvc()) then m else update_C(m, v[C]); /* Suppress updates to misa.{f,d} if disabled at boot */ if not(sys_enable_fdext()) then m - else update_D(update_F(m, v.F()), v.D() & v.F()) + else update_D(update_F(m, v[F]), v[D] & v[F]) } } /* helpers to check support for various extensions. */ /* we currently don't model 'E', so always assume 'I'. */ -function haveAtomics() -> bool = misa.A() == 0b1 -function haveRVC() -> bool = misa.C() == 0b1 -function haveMulDiv() -> bool = misa.M() == 0b1 -function haveSupMode() -> bool = misa.S() == 0b1 -function haveUsrMode() -> bool = misa.U() == 0b1 -function haveNExt() -> bool = misa.N() == 0b1 +function haveAtomics() -> bool = misa[A] == 0b1 +function haveRVC() -> bool = misa[C] == 0b1 +function haveMulDiv() -> bool = misa[M] == 0b1 +function haveSupMode() -> bool = misa[S] == 0b1 +function haveUsrMode() -> bool = misa[U] == 0b1 +function haveNExt() -> bool = misa[N] == 0b1 /* see below for F and D (and Z*inx counterparts) extension tests */ /* BitManip extension support. */ @@ -260,21 +260,21 @@ bitfield Mstatus : xlenbits = { register mstatus : Mstatus function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : Privilege) -> Privilege = - if t != Execute() & m.MPRV() == 0b1 - then privLevel_of_bits(m.MPP()) + if t != Execute() & m[MPRV] == 0b1 + then privLevel_of_bits(m[MPP]) else priv function get_mstatus_SXL(m : Mstatus) -> arch_xlen = { if sizeof(xlen) == 32 then arch_to_bits(RV32) - else m.bits()[35 .. 34] + else m.bits[35 .. 34] } function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { if sizeof(xlen) == 32 then m else { - let m = vector_update_subrange(m.bits(), 35, 34, a); + let m = vector_update_subrange(m.bits, 35, 34, a); Mk_Mstatus(m) } } @@ -282,14 +282,14 @@ function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { function get_mstatus_UXL(m : Mstatus) -> arch_xlen = { if sizeof(xlen) == 32 then arch_to_bits(RV32) - else m.bits()[33 .. 32] + else m.bits[33 .. 32] } function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { if sizeof(xlen) == 32 then m else { - let m = vector_update_subrange(m.bits(), 33, 32, a); + let m = vector_update_subrange(m.bits, 33, 32, a); Mk_Mstatus(m) } } @@ -311,8 +311,8 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { * FIXME: This should be made a platform parameter. */ let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m; - let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty | - extStatus_of_bits(m.VS()) == Dirty; + let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | + extStatus_of_bits(m[VS]) == Dirty; let m = update_SD(m, bool_to_bits(dirty)); /* We don't support dynamic changes to SXL and UXL. */ @@ -321,7 +321,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { /* We don't currently support changing MBE and SBE. */ let m = if sizeof(xlen) == 64 then { - Mk_Mstatus([m.bits() with 37 .. 36 = 0b00]) + Mk_Mstatus([m.bits with 37 .. 36 = 0b00]) } else m; /* Hardwired to zero in the absence of 'U' or 'N'. */ @@ -342,7 +342,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { function cur_Architecture() -> Architecture = { let a : arch_xlen = match (cur_privilege) { - Machine => misa.MXL(), + Machine => misa[MXL], Supervisor => get_mstatus_SXL(mstatus), User => get_mstatus_UXL(mstatus) }; @@ -357,12 +357,12 @@ 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) +function haveDExt() -> bool = (misa[D] == 0b1) & (mstatus[FS] != 0b00) /* Zfh (half-precision) extension depends on misa.F and mstatus.FS */ -function haveZfh() -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00) +function haveZfh() -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00) /* V extension has to enable both via misa.V as well as mstatus.VS */ -function haveVExt() -> bool = (misa.V() == 0b1) & (mstatus.VS() != 0b00) +function haveVExt() -> bool = (misa[V] == 0b1) & (mstatus[VS] != 0b00) /* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */ function haveZhinx() -> bool = sys_enable_zfinx() @@ -392,30 +392,30 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* The only writable bits are the S-mode bits, and with the 'N' * extension, the U-mode bits. */ let v = Mk_Minterrupts(v); - let m = update_SEI(o, v.SEI()); - let m = update_STI(m, v.STI()); - let m = update_SSI(m, v.SSI()); + let m = update_SEI(o, v[SEI]); + let m = update_STI(m, v[STI]); + let m = update_SSI(m, v[SSI]); if haveUsrMode() & haveNExt() then { - let m = update_UEI(m, v.UEI()); - let m = update_UTI(m, v.UTI()); - let m = update_USI(m, v.USI()); + let m = update_UEI(m, v[UEI]); + let m = update_UTI(m, v[UTI]); + let m = update_USI(m, v[USI]); m } else m } function legalize_mie(o : Minterrupts, v : xlenbits) -> Minterrupts = { let v = Mk_Minterrupts(v); - let m = update_MEI(o, v.MEI()); - let m = update_MTI(m, v.MTI()); - let m = update_MSI(m, v.MSI()); - let m = update_SEI(m, v.SEI()); - let m = update_STI(m, v.STI()); - let m = update_SSI(m, v.SSI()); + let m = update_MEI(o, v[MEI]); + let m = update_MTI(m, v[MTI]); + let m = update_MSI(m, v[MSI]); + let m = update_SEI(m, v[SEI]); + let m = update_STI(m, v[STI]); + let m = update_SSI(m, v[SSI]); /* The U-mode bits will be modified if we have the 'N' extension. */ if haveUsrMode() & haveNExt() then { - let m = update_UEI(m, v.UEI()); - let m = update_UTI(m, v.UTI()); - let m = update_USI(m, v.USI()); + let m = update_UEI(m, v[UEI]); + let m = update_UTI(m, v[UTI]); + let m = update_USI(m, v[USI]); m } else m } @@ -467,10 +467,10 @@ register mtvec : Mtvec /* Trap Vector */ function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = { let v = Mk_Mtvec(v); - match (trapVectorMode_of_bits(v.Mode())) { + match (trapVectorMode_of_bits(v[Mode])) { TV_Direct => v, TV_Vector => v, - _ => update_Mode(v, o.Mode()) + _ => update_Mode(v, o[Mode]) } } @@ -482,11 +482,11 @@ register mcause : Mcause /* Interpreting the trap-vector address */ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = { - let base : xlenbits = m.Base() @ 0b00; - match (trapVectorMode_of_bits(m.Mode())) { + let base : xlenbits = m[Base] @ 0b00; + match (trapVectorMode_of_bits(m[Mode])) { TV_Direct => Some(base), - TV_Vector => if c.IsInterrupt() == 0b1 - then Some(base + (zero_extend(c.Cause()) << 2)) + TV_Vector => if c[IsInterrupt] == 0b1 + then Some(base + (zero_extend(c[Cause]) << 2)) else Some(base), TV_Reserved => None() } @@ -502,13 +502,13 @@ register mepc : xlenbits function legalize_xepc(v : xlenbits) -> xlenbits = /* allow writing xepc[1] only if misa.C is enabled or could be enabled XXX specification says this legalization should be done on read */ - if (sys_enable_writable_misa() & sys_enable_rvc()) | misa.C() == 0b1 + if (sys_enable_writable_misa() & sys_enable_rvc()) | misa[C] == 0b1 then [v with 0 = bitzero] else v & sign_extend(0b100) /* masking for reads to xepc */ function pc_alignment_mask() -> xlenbits = - ~(zero_extend(if misa.C() == 0b1 then 0b00 else 0b10)) + ~(zero_extend(if misa[C] == 0b1 then 0b00 else 0b10)) /* auxiliary exception registers */ @@ -608,55 +608,55 @@ bitfield Sstatus : xlenbits = { /* sstatus is a view of mstatus, so there is no register defined. */ function get_sstatus_UXL(s : Sstatus) -> arch_xlen = { - let m = Mk_Mstatus(s.bits()); + let m = Mk_Mstatus(s.bits); get_mstatus_UXL(m) } function set_sstatus_UXL(s : Sstatus, a : arch_xlen) -> Sstatus = { - let m = Mk_Mstatus(s.bits()); + let m = Mk_Mstatus(s.bits); let m = set_mstatus_UXL(m, a); - Mk_Sstatus(m.bits()) + Mk_Sstatus(m.bits) } function lower_mstatus(m : Mstatus) -> Sstatus = { let s = Mk_Sstatus(zero_extend(0b0)); - let s = update_SD(s, m.SD()); + let s = update_SD(s, m[SD]); let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); - let s = update_MXR(s, m.MXR()); - let s = update_SUM(s, m.SUM()); - let s = update_XS(s, m.XS()); - let s = update_FS(s, m.FS()); - let s = update_VS(s, m.VS()); - let s = update_SPP(s, m.SPP()); - let s = update_SPIE(s, m.SPIE()); - let s = update_UPIE(s, m.UPIE()); - let s = update_SIE(s, m.SIE()); - let s = update_UIE(s, m.UIE()); + let s = update_MXR(s, m[MXR]); + let s = update_SUM(s, m[SUM]); + let s = update_XS(s, m[XS]); + let s = update_FS(s, m[FS]); + let s = update_VS(s, m[VS]); + let s = update_SPP(s, m[SPP]); + let s = update_SPIE(s, m[SPIE]); + let s = update_UPIE(s, m[UPIE]); + let s = update_SIE(s, m[SIE]); + let s = update_UIE(s, m[UIE]); s } function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { - let m = update_MXR(m, s.MXR()); - let m = update_SUM(m, s.SUM()); + let m = update_MXR(m, s[MXR]); + let m = update_SUM(m, s[SUM]); - let m = update_XS(m, s.XS()); + let m = update_XS(m, s[XS]); // See comment for mstatus.FS. - let m = update_FS(m, s.FS()); - let m = update_VS(m, s.VS()); - let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty | - extStatus_of_bits(m.VS()) == Dirty; + let m = update_FS(m, s[FS]); + let m = update_VS(m, s[VS]); + let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | + extStatus_of_bits(m[VS]) == Dirty; let m = update_SD(m, bool_to_bits(dirty)); - let m = update_SPP(m, s.SPP()); - let m = update_SPIE(m, s.SPIE()); - let m = update_UPIE(m, s.UPIE()); - let m = update_SIE(m, s.SIE()); - let m = update_UIE(m, s.UIE()); + let m = update_SPP(m, s[SPP]); + let m = update_SPIE(m, s[SPIE]); + let m = update_UPIE(m, s[UPIE]); + let m = update_SIE(m, s[SIE]); + let m = update_UIE(m, s[UIE]); m } function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = { - legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits()) + legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits) } bitfield Sedeleg : xlenbits = { @@ -690,35 +690,35 @@ bitfield Sinterrupts : xlenbits = { /* Provides the sip read view of mip (m) as delegated by mideleg (d). */ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); - let s = update_SEI(s, m.SEI() & d.SEI()); - let s = update_STI(s, m.STI() & d.STI()); - let s = update_SSI(s, m.SSI() & d.SSI()); + let s = update_SEI(s, m[SEI] & d[SEI]); + let s = update_STI(s, m[STI] & d[STI]); + let s = update_SSI(s, m[SSI] & d[SSI]); - let s = update_UEI(s, m.UEI() & d.UEI()); - let s = update_UTI(s, m.UTI() & d.UTI()); - let s = update_USI(s, m.USI() & d.USI()); + let s = update_UEI(s, m[UEI] & d[UEI]); + let s = update_UTI(s, m[UTI] & d[UTI]); + let s = update_USI(s, m[USI] & d[USI]); s } /* Provides the sie read view of mie (m) as delegated by mideleg (d). */ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); - let s = update_SEI(s, m.SEI() & d.SEI()); - let s = update_STI(s, m.STI() & d.STI()); - let s = update_SSI(s, m.SSI() & d.SSI()); - let s = update_UEI(s, m.UEI() & d.UEI()); - let s = update_UTI(s, m.UTI() & d.UTI()); - let s = update_USI(s, m.USI() & d.USI()); + let s = update_SEI(s, m[SEI] & d[SEI]); + let s = update_STI(s, m[STI] & d[STI]); + let s = update_SSI(s, m[SSI] & d[SSI]); + let s = update_UEI(s, m[UEI] & d[UEI]); + let s = update_UTI(s, m[UTI] & d[UTI]); + let s = update_USI(s, m[USI] & d[USI]); s } /* Returns the new value of mip from the previous mip (o) and the written sip (s) as delegated by mideleg (d). */ function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; - let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m; + let m = if d[SSI] == 0b1 then update_SSI(m, s[SSI]) else m; if haveNExt() then { - let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m; - let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m; + let m = if d[UEI] == 0b1 then update_UEI(m, s[UEI]) else m; + let m = if d[USI] == 0b1 then update_USI(m, s[USI]) else m; m } else m } @@ -730,13 +730,13 @@ function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr /* Returns the new value of mie from the previous mie (o) and the written sie (s) as delegated by mideleg (d). */ function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; - let m = if d.SEI() == 0b1 then update_SEI(m, s.SEI()) else m; - let m = if d.STI() == 0b1 then update_STI(m, s.STI()) else m; - let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m; + let m = if d[SEI] == 0b1 then update_SEI(m, s[SEI]) else m; + let m = if d[STI] == 0b1 then update_STI(m, s[STI]) else m; + let m = if d[SSI] == 0b1 then update_SSI(m, s[SSI]) else m; if haveNExt() then { - let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m; - let m = if d.UTI() == 0b1 then update_UTI(m, s.UTI()) else m; - let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m; + let m = if d[UEI] == 0b1 then update_UEI(m, s[UEI]) else m; + let m = if d[UTI] == 0b1 then update_UTI(m, s[UTI]) else m; + let m = if d[USI] == 0b1 then update_USI(m, s[USI]) else m; m } else m } @@ -767,10 +767,10 @@ bitfield Satp64 : bits(64) = { function legalize_satp64(a : Architecture, o : bits(64), v : bits(64)) -> bits(64) = { let s = Mk_Satp64(v); - match satp64Mode_of_bits(a, s.Mode()) { + match satp64Mode_of_bits(a, s[Mode]) { None() => o, Some(Sv32) => o, /* Sv32 is unsupported for now */ - Some(_) => s.bits() + Some(_) => s.bits } } @@ -867,7 +867,7 @@ register senvcfg : Envcfg function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { let v = Mk_Envcfg(v); - let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); + let o = update_FIOM(o, if sys_enable_writable_fiom() then v[FIOM] else 0b0); // Other extensions are not implemented yet so all other fields are read only zero. o } @@ -878,8 +878,8 @@ function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { function is_fiom_active() -> bool = { match cur_privilege { Machine => false, - Supervisor => menvcfg.FIOM() == 0b1, - User => (menvcfg.FIOM() | senvcfg.FIOM()) == 0b1, + Supervisor => menvcfg[FIOM] == 0b1, + User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1, } } /* vector csrs */ @@ -903,7 +903,7 @@ register vtype : Vtype /* this returns the power of 2 for SEW */ val get_sew_pow : unit -> {|3, 4, 5, 6|} function get_sew_pow() = { - let SEW_pow : {|3, 4, 5, 6|} = match vtype.vsew() { + let SEW_pow : {|3, 4, 5, 6|} = match vtype[vsew] { 0b000 => 3, 0b001 => 4, 0b010 => 5, @@ -937,7 +937,7 @@ function get_sew_bytes() = { /* this returns the power of 2 for LMUL */ val get_lmul_pow : unit -> {|-3, -2, -1, 0, 1, 2, 3|} function get_lmul_pow() = { - match vtype.vlmul() { + match vtype[vlmul] { 0b101 => -3, 0b110 => -2, 0b111 => -1, @@ -960,7 +960,7 @@ function decode_agtype(ag) = { } val get_vtype_vma : unit -> agtype -function get_vtype_vma() = decode_agtype(vtype.vma()) +function get_vtype_vma() = decode_agtype(vtype[vma]) val get_vtype_vta : unit -> agtype -function get_vtype_vta() = decode_agtype(vtype.vta()) +function get_vtype_vta() = decode_agtype(vtype[vta]) diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index 0fc1660..931b5d7 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -45,14 +45,14 @@ function clause ext_is_CSR_defined (0x009, _) = true function clause ext_is_CSR_defined (0x00A, _) = true function clause ext_is_CSR_defined (0x00F, _) = true -function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat())) -function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm())) -function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits())) +function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat])) +function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm])) +function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits)) -function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr.vxsat())) -function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr.vxrm())) -function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits())) +function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat])) +function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm])) +function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits)) -function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr.vxrm(), value[0 .. 0]); Some(zero_extend(vcsr.vxsat())) } -function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr.vxsat()); Some(zero_extend(vcsr.vxrm())) } -function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits())) } +function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); Some(zero_extend(vcsr[vxsat])) } +function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); Some(zero_extend(vcsr[vxrm])) } +function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits)) } diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 7faa50b..b74e081 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -108,8 +108,8 @@ mapping vreg_name = { function dirty_v_context() -> unit = { assert(sys_enable_vext()); - mstatus->VS() = extStatus_to_bits(Dirty); - mstatus->SD() = 0b1 + mstatus[VS] = extStatus_to_bits(Dirty); + mstatus[SD] = 0b1 } function dirty_v_context_if_present() -> unit = { @@ -259,8 +259,8 @@ register vcsr : Vcsr val ext_write_vcsr : (bits(2), bits(1)) -> unit function ext_write_vcsr (vxrm_val, vxsat_val) = { - vcsr->vxrm() = vxrm_val; /* Note: frm can be an illegal value, 101, 110, 111 */ - vcsr->vxsat() = vxsat_val; + vcsr[vxrm] = vxrm_val; /* Note: frm can be an illegal value, 101, 110, 111 */ + vcsr[vxsat] = vxsat_val; dirty_v_context_if_present() } diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail index 46134d2..453de86 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -91,13 +91,13 @@ type asid32 = bits(9) function curAsid32(satp : bits(32)) -> asid32 = { let s = Mk_Satp32(satp); - s.Asid() + s[Asid] } /* page table base from satp */ function curPTB32(satp : bits(32)) -> paddr32 = { let s : Satp32 = Mk_Satp32(satp); - shiftl(zero_extend(s.PPN()), PAGESIZE_BITS) + shiftl(zero_extend(s[PPN]), PAGESIZE_BITS) } /* Sv32 parameters and bitfield layouts */ @@ -147,13 +147,13 @@ type asid64 = bits(16) function curAsid64(satp : bits(64)) -> asid64 = { let s = Mk_Satp64(satp); - s.Asid() + s[Asid] } /* page table base from satp */ function curPTB64(satp : bits(64)) -> paddr64 = { let s = Mk_Satp64(satp); - shiftl(zero_extend(s.PPN()), PAGESIZE_BITS) + shiftl(zero_extend(s[PPN]), PAGESIZE_BITS) } /* Sv39 parameters and bitfield layouts */ diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index 3478be4..c0e20f8 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -87,7 +87,7 @@ function translationMode(priv) = { match arch { Some(RV32) => { let s = Mk_Satp32(satp[31..0]); - if s.Mode() == 0b0 then Sbare else Sv32 + if s[Mode] == 0b0 then Sbare else Sv32 }, _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") } @@ -98,8 +98,8 @@ function translationMode(priv) = { val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { - let mxr : bool = mstatus.MXR() == 0b1; - let do_sum : bool = mstatus.SUM() == 0b1; + let mxr : bool = mstatus[MXR] == 0b1; + let do_sum : bool = mstatus[SUM] == 0b1; let mode : SATPMode = translationMode(effPriv); let asid = curAsid32(satp); diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index 18d0991..025a1cb 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -100,7 +100,7 @@ function translationMode(priv) = { let arch = architecture(get_mstatus_SXL(mstatus)); match arch { Some(RV64) => { - let mbits : satp_mode = Mk_Satp64(satp).Mode(); + let mbits : satp_mode = Mk_Satp64(satp)[Mode]; match satp64Mode_of_bits(RV64, mbits) { Some(m) => m, None() => internal_error(__FILE__, __LINE__, "invalid RV64 translation mode in satp") @@ -108,7 +108,7 @@ function translationMode(priv) = { }, Some(RV32) => { let s = Mk_Satp32(satp[31..0]); - if s.Mode() == 0b0 then Sbare else Sv32 + if s[Mode] == 0b0 then Sbare else Sv32 }, _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch") } @@ -119,8 +119,8 @@ function translationMode(priv) = { val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType) function translateAddr_priv(vAddr, ac, effPriv) = { - let mxr : bool = mstatus.MXR() == 0b1; - let do_sum : bool = mstatus.SUM() == 0b1; + let mxr : bool = mstatus[MXR] == 0b1; + let do_sum : bool = mstatus[SUM] == 0b1; let mode : SATPMode = translationMode(effPriv); let asid = curAsid64(satp); diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 72def15..3b3ce1c 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -79,7 +79,7 @@ function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV32_Vaddr(vaddr); - let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), PTE32_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (mem_read_priv(Read(Data), Supervisor, to_phys_addr(pte_addr), 4, false, false, false)) { @@ -93,10 +93,10 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { }, MemValue(v) => { let pte = Mk_SV32_PTE(v); - let pbits = pte.BITS(); + let pbits = pte[BITS]; let ext_pte : extPte = default_sv32_ext_pte; let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr.G() == 0b1); + let is_global = global | (pattr[G] == 0b1); /* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(to_phys_addr(ptb)) ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) @@ -109,7 +109,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, ext_pte) then { if level > 0 then { /* walk down the pointer to the next level */ - walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk32: last-level pte contains a ptr"); */ @@ -124,24 +124,24 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV32_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != zero_extend(0b0) then { + let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV32_LEVEL_BITS) - 1; + if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk32: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); -/* let res = append(ppn, va.PgOfs()); - print("walk32: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); +/* let res = append(ppn, va[PgOfs]); + print("walk32: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } else { /* normal leaf PTE */ -/* let res = append(pte.PPNi(), va.PgOfs()); - print("walk32: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) +/* let res = append(pte[PPNi], va[PgOfs]); + print("walk32: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } } @@ -167,7 +167,7 @@ function lookup_TLB32(asid, vaddr) = val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV32_LEVEL_BITS); + let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV32_LEVEL_BITS); tlb32 = Some(ent) } @@ -192,7 +192,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* print("translate32: TLB32 hit for " ^ BitStr(vAddr)); */ let pte = Mk_SV32_PTE(ent.pte); let ext_pte : extPte = zeros(); // no reserved bits for extensions - let pteBits = Mk_PTE_Bits(pte.BITS()); + let pteBits = Mk_PTE_Bits(pte[BITS]); match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, PTE_Check_Success(ext_ptw) => { @@ -205,13 +205,13 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Failure(PTW_PTE_Update(), ext_ptw) } else { /* update PTE entry and TLB */ - n_pte = update_BITS(pte, pbits.bits()); + n_pte = update_BITS(pte, pbits.bits); /* ext is unused since there are no reserved bits for extensions */ n_ent : TLB32_Entry = ent; - n_ent.pte = n_pte.bits(); + n_ent.pte = n_pte.bits; write_TLB32(idx, n_ent); /* update page table */ - match mem_write_value_priv(to_phys_addr(zero_extend(ent.pteAddr)), 4, n_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(to_phys_addr(zero_extend(ent.pteAddr)), 4, n_pte.bits, Supervisor, false, false, false) { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; @@ -226,7 +226,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match walk32(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac, zeros()) { + match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, zeros()) { None() => { add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) @@ -237,9 +237,9 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - var w_pte : SV32_PTE = update_BITS(pte, pbits.bits()); + var w_pte : SV32_PTE = update_BITS(pte, pbits.bits); /* ext is unused since there are no reserved bits for extensions */ - match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 25378a8..058d749 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -73,7 +73,7 @@ val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV39_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), PTE39_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { @@ -87,10 +87,10 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { }, MemValue(v) => { let pte = Mk_SV39_PTE(v); - let pbits = pte.BITS(); - let ext_pte = pte.Ext(); + let pbits = pte[BITS]; + let ext_pte = pte[Ext]; let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr.G() == 0b1); + let is_global = global | (pattr[G] == 0b1); /* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) @@ -103,7 +103,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, ext_pte) then { if level > 0 then { /* walk down the pointer to the next level */ - walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk39: last-level pte contains a ptr"); */ @@ -118,24 +118,24 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != zero_extend(0b0) then { + let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; + if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk39: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); -/* let res = append(ppn, va.PgOfs()); - print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); +/* let res = append(ppn, va[PgOfs]); + print("walk39: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } else { /* normal leaf PTE */ -/* let res = append(pte.PPNi(), va.PgOfs()); - print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) +/* let res = append(pte[PPNi], va[PgOfs]); + print("walk39: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } } @@ -161,7 +161,7 @@ function lookup_TLB39(asid, vaddr) = val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV39_LEVEL_BITS); + let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV39_LEVEL_BITS); tlb39 = Some(ent) } @@ -185,8 +185,8 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = Some(idx, ent) => { /* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */ let pte = Mk_SV39_PTE(ent.pte); - let ext_pte = pte.Ext(); - let pteBits = Mk_PTE_Bits(pte.BITS()); + let ext_pte = pte[Ext]; + let pteBits = Mk_PTE_Bits(pte[BITS]); match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) { PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, PTE_Check_Success(ext_ptw) => { @@ -199,13 +199,13 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = TR_Failure(PTW_PTE_Update(), ext_ptw) } else { /* update PTE entry and TLB */ - n_pte = update_BITS(pte, pbits.bits()); + n_pte = update_BITS(pte, pbits.bits); n_pte = update_Ext(n_pte, ext); n_ent : TLB39_Entry = ent; - n_ent.pte = n_pte.bits(); + n_ent.pte = n_pte.bits; write_TLB39(idx, n_ent); /* update page table */ - match mem_write_value_priv(zero_extend(ent.pteAddr), 8, n_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(ent.pteAddr), 8, n_pte.bits, Supervisor, false, false, false) { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; @@ -220,7 +220,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match walk39(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac, pte.Ext()) { + match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { None() => { add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) @@ -231,9 +231,9 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - var w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); + var w_pte : SV39_PTE = update_BITS(pte, pbits.bits); w_pte = update_Ext(w_pte, ext); - match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 64c7a54..51eab14 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -73,7 +73,7 @@ val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV48_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), PTE48_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { @@ -87,10 +87,10 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { }, MemValue(v) => { let pte = Mk_SV48_PTE(v); - let pbits = pte.BITS(); - let ext_pte = pte.Ext(); + let pbits = pte[BITS]; + let ext_pte = pte[Ext]; let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr.G() == 0b1); + let is_global = global | (pattr[G] == 0b1); /* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) ^ " pt_ofs=" ^ BitStr(pt_ofs) @@ -103,7 +103,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, ext_pte) then { if level > 0 then { /* walk down the pointer to the next level */ - walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk48: last-level pte contains a ptr"); */ @@ -118,24 +118,24 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != zero_extend(0b0) then { + let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; + if (pte[PPNi] & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk48: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); -/* let res = append(ppn, va.PgOfs()); - print("walk48: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask); +/* let res = append(ppn, va[PgOfs]); + print("walk48: using superpage: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) + PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } else { /* normal leaf PTE */ -/* let res = append(pte.PPNi(), va.PgOfs()); - print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw) +/* let res = append(pte[PPNi], va[PgOfs]); + print("walk48: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw) } } } @@ -161,7 +161,7 @@ function lookup_TLB48(asid, vaddr) = val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV48_LEVEL_BITS); + let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV48_LEVEL_BITS); tlb48 = Some(ent) } @@ -184,7 +184,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) { PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw), PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac, pte.Ext()) { + match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) { None() => { add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) @@ -195,9 +195,9 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = /* pte needs dirty/accessed update but that is not enabled */ TR_Failure(PTW_PTE_Update(), ext_ptw) } else { - var w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); + var w_pte : SV48_PTE = update_BITS(pte, pbits.bits); w_pte = update_Ext(w_pte, ext); - match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) { MemValue(_) => { add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index e1007bb..121bcf8 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -93,18 +93,18 @@ function rvfi_set_instr_packet(p) = val rvfi_get_cmd : unit -> bits(8) -function rvfi_get_cmd () = rvfi_instruction.rvfi_cmd() +function rvfi_get_cmd () = rvfi_instruction[rvfi_cmd] val rvfi_get_insn : unit -> bits(32) -function rvfi_get_insn () = rvfi_instruction.rvfi_insn() +function rvfi_get_insn () = rvfi_instruction[rvfi_insn] val print_instr_packet : bits(64) -> unit function print_instr_packet(bs) = { let p = Mk_RVFI_DII_Instruction_Packet(bs); - print_bits("command ", p.rvfi_cmd()); - print_bits("instruction ", p.rvfi_insn()) + print_bits("command ", p[rvfi_cmd]); + print_bits("instruction ", p[rvfi_insn]) } bitfield RVFI_DII_Execution_Packet_V1 : bits(704) = { @@ -291,36 +291,36 @@ function rvfi_get_v2_support_packet () = { // backwards compatibility with old implementations that do not support // the new trace format. let rvfi_exec = update_rvfi_halt(rvfi_exec, 0x03); - return rvfi_exec.bits(); + return rvfi_exec.bits; } val rvfi_get_exec_packet_v1 : unit -> bits(704) function rvfi_get_exec_packet_v1 () = { let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); // Convert the v2 packet to a v1 packet - let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data.rvfi_intr()); - let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data.rvfi_halt()); - let v1_packet = update_rvfi_trap(v1_packet, rvfi_inst_data.rvfi_trap()); - let v1_packet = update_rvfi_insn(v1_packet, rvfi_inst_data.rvfi_insn()); - let v1_packet = update_rvfi_order(v1_packet, rvfi_inst_data.rvfi_order()); + let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data[rvfi_intr]); + let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data[rvfi_halt]); + let v1_packet = update_rvfi_trap(v1_packet, rvfi_inst_data[rvfi_trap]); + let v1_packet = update_rvfi_insn(v1_packet, rvfi_inst_data[rvfi_insn]); + let v1_packet = update_rvfi_order(v1_packet, rvfi_inst_data[rvfi_order]); - let v1_packet = update_rvfi_pc_wdata(v1_packet, rvfi_pc_data.rvfi_pc_wdata()); - let v1_packet = update_rvfi_pc_rdata(v1_packet, rvfi_pc_data.rvfi_pc_rdata()); + let v1_packet = update_rvfi_pc_wdata(v1_packet, rvfi_pc_data[rvfi_pc_wdata]); + let v1_packet = update_rvfi_pc_rdata(v1_packet, rvfi_pc_data[rvfi_pc_rdata]); - let v1_packet = update_rvfi_rd_addr(v1_packet, rvfi_int_data.rvfi_rd_addr()); + let v1_packet = update_rvfi_rd_addr(v1_packet, rvfi_int_data[rvfi_rd_addr]); let v1_packet = update_rvfi_rs2_addr(v1_packet, rvfi_int_data.rvfi_rs2_addr()); let v1_packet = update_rvfi_rs1_addr(v1_packet, rvfi_int_data.rvfi_rs1_addr()); - let v1_packet = update_rvfi_rd_wdata(v1_packet, rvfi_int_data.rvfi_rd_wdata()); + let v1_packet = update_rvfi_rd_wdata(v1_packet, rvfi_int_data[rvfi_rd_wdata]); let v1_packet = update_rvfi_rs2_data(v1_packet, rvfi_int_data.rvfi_rs2_rdata()); let v1_packet = update_rvfi_rs1_data(v1_packet, rvfi_int_data.rvfi_rs1_rdata()); - let v1_packet = update_rvfi_mem_wmask(v1_packet, truncate(rvfi_mem_data.rvfi_mem_wmask(), 8)); - let v1_packet = update_rvfi_mem_rmask(v1_packet, truncate(rvfi_mem_data.rvfi_mem_rmask(), 8)); - let v1_packet = update_rvfi_mem_wdata(v1_packet, truncate(rvfi_mem_data.rvfi_mem_wdata(), 64)); - let v1_packet = update_rvfi_mem_rdata(v1_packet, truncate(rvfi_mem_data.rvfi_mem_rdata(), 64)); - let v1_packet = update_rvfi_mem_addr(v1_packet, rvfi_mem_data.rvfi_mem_addr()); + let v1_packet = update_rvfi_mem_wmask(v1_packet, truncate(rvfi_mem_data[rvfi_mem_wmask], 8)); + let v1_packet = update_rvfi_mem_rmask(v1_packet, truncate(rvfi_mem_data[rvfi_mem_rmask], 8)); + let v1_packet = update_rvfi_mem_wdata(v1_packet, truncate(rvfi_mem_data[rvfi_mem_wdata], 64)); + let v1_packet = update_rvfi_mem_rdata(v1_packet, truncate(rvfi_mem_data[rvfi_mem_rdata], 64)); + let v1_packet = update_rvfi_mem_addr(v1_packet, rvfi_mem_data[rvfi_mem_addr]); - return v1_packet.bits(); + return v1_packet.bits; } val rvfi_get_v2_trace_size : unit -> bits(64) @@ -337,27 +337,27 @@ function rvfi_get_exec_packet_v2 () = { // TODO: find a way to return a variable-length bitvector let packet = Mk_RVFI_DII_Execution_PacketV2(zero_extend(0b0)); let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE) - let packet = update_basic_data(packet, rvfi_inst_data.bits()); - let packet = update_pc_data(packet, rvfi_pc_data.bits()); + let packet = update_basic_data(packet, rvfi_inst_data.bits); + let packet = update_pc_data(packet, rvfi_pc_data.bits); let packet = update_integer_data_available(packet, bool_to_bits(rvfi_int_data_present)); let packet = update_memory_access_data_available(packet, bool_to_bits(rvfi_mem_data_present)); // To simplify the implementation (so that we can return a fixed-size vector) // we always return a max-size packet from this function, and the C emulator // ensures that only trace_size bits are sent over the socket. let packet = update_trace_size(packet, rvfi_get_v2_trace_size()); - return packet.bits(); + return packet.bits; } val rvfi_get_int_data : unit -> bits(320) function rvfi_get_int_data () = { assert(rvfi_int_data_present, "reading uninitialized data"); - return rvfi_int_data.bits(); + return rvfi_int_data.bits; } val rvfi_get_mem_data : unit -> bits(704) function rvfi_get_mem_data () = { assert(rvfi_mem_data_present, "reading uninitialized data"); - return rvfi_mem_data.bits(); + return rvfi_mem_data.bits; } val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. atom('n) -> bits(32) @@ -368,22 +368,22 @@ function rvfi_encode_width_mask(width) = val print_rvfi_exec : unit -> unit function print_rvfi_exec () = { - print_bits("rvfi_intr : ", rvfi_inst_data.rvfi_intr()); - print_bits("rvfi_halt : ", rvfi_inst_data.rvfi_halt()); - print_bits("rvfi_trap : ", rvfi_inst_data.rvfi_trap()); - print_bits("rvfi_rd_addr : ", rvfi_int_data.rvfi_rd_addr()); + print_bits("rvfi_intr : ", rvfi_inst_data[rvfi_intr]); + print_bits("rvfi_halt : ", rvfi_inst_data[rvfi_halt]); + print_bits("rvfi_trap : ", rvfi_inst_data[rvfi_trap]); + print_bits("rvfi_rd_addr : ", rvfi_int_data[rvfi_rd_addr]); print_bits("rvfi_rs2_addr : ", rvfi_int_data.rvfi_rs2_addr()); print_bits("rvfi_rs1_addr : ", rvfi_int_data.rvfi_rs1_addr()); - print_bits("rvfi_mem_wmask: ", rvfi_mem_data.rvfi_mem_wmask()); - print_bits("rvfi_mem_rmask: ", rvfi_mem_data.rvfi_mem_rmask()); - print_bits("rvfi_mem_wdata: ", rvfi_mem_data.rvfi_mem_wdata()); - print_bits("rvfi_mem_rdata: ", rvfi_mem_data.rvfi_mem_rdata()); - print_bits("rvfi_mem_addr : ", rvfi_mem_data.rvfi_mem_addr()); - print_bits("rvfi_rd_wdata : ", rvfi_int_data.rvfi_rd_wdata()); + print_bits("rvfi_mem_wmask: ", rvfi_mem_data[rvfi_mem_wmask]); + print_bits("rvfi_mem_rmask: ", rvfi_mem_data[rvfi_mem_rmask]); + print_bits("rvfi_mem_wdata: ", rvfi_mem_data[rvfi_mem_wdata]); + print_bits("rvfi_mem_rdata: ", rvfi_mem_data[rvfi_mem_rdata]); + print_bits("rvfi_mem_addr : ", rvfi_mem_data[rvfi_mem_addr]); + print_bits("rvfi_rd_wdata : ", rvfi_int_data[rvfi_rd_wdata]); print_bits("rvfi_rs2_data : ", rvfi_int_data.rvfi_rs2_rdata()); print_bits("rvfi_rs1_data : ", rvfi_int_data.rvfi_rs1_rdata()); - print_bits("rvfi_insn : ", rvfi_inst_data.rvfi_insn()); - print_bits("rvfi_pc_wdata : ", rvfi_pc_data.rvfi_pc_wdata()); - print_bits("rvfi_pc_rdata : ", rvfi_pc_data.rvfi_pc_rdata()); - print_bits("rvfi_order : ", rvfi_inst_data.rvfi_order()); + print_bits("rvfi_insn : ", rvfi_inst_data[rvfi_insn]); + print_bits("rvfi_pc_wdata : ", rvfi_pc_data[rvfi_pc_wdata]); + print_bits("rvfi_pc_rdata : ", rvfi_pc_data[rvfi_pc_rdata]); + print_bits("rvfi_order : ", rvfi_inst_data[rvfi_order]); } |