From 10348eb636c2a5c67916b464191eda63701e6210 Mon Sep 17 00:00:00 2001 From: Ksenia Dobrovolskaya Date: Wed, 24 Jul 2024 18:09:33 +0300 Subject: [PATCH] Implementing callbacks in sail-riscv for state-changing events Pushed all the rv_enable_callbacks into the callback functions. --- Makefile | 1 + c_emulator/riscv_config.h | 1 + c_emulator/riscv_default_callbacks.c | 23 ++++++------- c_emulator/riscv_rvfi_callbacks.c | 48 +++++++++++++++++----------- c_emulator/riscv_sim.c | 2 ++ model/riscv_csr_ext.sail | 14 -------- model/riscv_fdext_regs.sail | 2 +- model/riscv_insts_vext_mem.sail | 12 ++++--- model/riscv_insts_vext_vset.sail | 45 +++++++++++++++----------- model/riscv_insts_zicsr.sail | 9 ++++-- model/riscv_mem.sail | 18 +++++------ model/riscv_pc_access.sail | 2 +- model/riscv_regs.sail | 2 +- model/riscv_sys_control.sail | 14 ++++---- model/riscv_types.sail | 25 ++++++--------- model/riscv_vext_regs.sail | 2 +- model/riscv_vreg_type.sail | 2 +- model/rvfi_dii.sail | 21 ++++++------ ocaml_emulator/platform.ml | 17 +++++----- 19 files changed, 133 insertions(+), 127 deletions(-) diff --git a/Makefile b/Makefile index 36c3ad7d1..ee2e2b3df 100644 --- a/Makefile +++ b/Makefile @@ -327,6 +327,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \ -c_preserve rvfi_halt_exec_packet \ -c_preserve rvfi_write \ -c_preserve rvfi_read \ + -c_preserve rvfi_mem_exception \ -c_preserve rvfi_wX \ -c_preserve print_rvfi_exec \ -c_preserve print_instr_packet \ diff --git a/c_emulator/riscv_config.h b/c_emulator/riscv_config.h index f8f3eb30d..285ff0421 100644 --- a/c_emulator/riscv_config.h +++ b/c_emulator/riscv_config.h @@ -5,3 +5,4 @@ extern bool config_print_instr; extern bool config_print_reg; extern bool config_print_mem_access; extern bool config_print_platform; +extern bool rv_enable_callbacks; diff --git a/c_emulator/riscv_default_callbacks.c b/c_emulator/riscv_default_callbacks.c index d4600321c..fd7fa3e84 100644 --- a/c_emulator/riscv_default_callbacks.c +++ b/c_emulator/riscv_default_callbacks.c @@ -1,16 +1,11 @@ /* The model assumes that these functions do not change the state of the model. */ -int mem_update_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) -{ -} -int mem_read_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) -{ -} -int xreg_update_callback(unsigned reg, uint64_t value) { } -int freg_update_callback(unsigned reg, uint64_t value) { } -int csr_update_callback(const char *reg_name, uint64_t value) { } -int csr_read_callback(const char *reg_name, uint64_t value) { } -int vreg_update_callback(unsigned reg, lbits value) { } -int pc_update_callback(uint64_t value) { } +int mem_write_callback(uint64_t addr, uint64_t width, lbits value) { } +int mem_read_callback(uint64_t addr, uint64_t width, lbits value) { } +int mem_exception_callback(uint64_t addr, uint64_t num_of_exception) { } +int xreg_write_callback(unsigned reg, uint64_t value) { } +int freg_write_callback(unsigned reg, uint64_t value) { } +int csr_write_callback(unsigned reg, uint64_t value) { } +int csr_read_callback(unsigned reg, uint64_t value) { } +int vreg_write_callback(unsigned reg, lbits value) { } +int pc_write_callback(uint64_t value) { } diff --git a/c_emulator/riscv_rvfi_callbacks.c b/c_emulator/riscv_rvfi_callbacks.c index 44048bf28..77cd37e8e 100644 --- a/c_emulator/riscv_rvfi_callbacks.c +++ b/c_emulator/riscv_rvfi_callbacks.c @@ -1,27 +1,37 @@ -int zrvfi_write(uint64_t addr, int64_t width, lbits value, bool is_exception); -int zrvfi_read(uint64_t addr, sail_int width, lbits value, bool is_exception); +#include "riscv_config.h" + +int zrvfi_write(uint64_t addr, int64_t width, lbits value); +int zrvfi_read(uint64_t addr, sail_int width, lbits value); +int zrvfi_mem_exception(uint64_t addr); int zrvfi_wX(int64_t reg, uint64_t value); -int mem_update_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) +int mem_write_callback(uint64_t addr, uint64_t width, lbits value) +{ + if (rv_enable_callbacks) + zrvfi_write(addr, width, value); +} +int mem_read_callback(uint64_t addr, uint64_t width, lbits value) { - zrvfi_write(addr, width, value, is_exception); + if (rv_enable_callbacks) { + sail_int len; + CREATE(sail_int)(&len); + CONVERT_OF(sail_int, mach_int)(&len, width); + zrvfi_read(addr, len, value); + KILL(sail_int)(&len); + } } -int mem_read_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) +int mem_exception_callback(uint64_t addr, uint64_t num_of_exception) { - sail_int len; - CREATE(sail_int)(&len); - CONVERT_OF(sail_int, mach_int)(&len, width); - zrvfi_read(addr, len, value, is_exception); - KILL(sail_int)(&len); + if (rv_enable_callbacks) + zrvfi_mem_exception(addr); } -int xreg_update_callback(unsigned reg, uint64_t value) +int xreg_write_callback(unsigned reg, uint64_t value) { - zrvfi_wX(reg, value); + if (rv_enable_callbacks) + zrvfi_wX(reg, value); } -int freg_update_callback(unsigned reg, uint64_t value) { } -int csr_update_callback(const char *reg_name, uint64_t value) { } -int csr_read_callback(const char *reg_name, uint64_t value) { } -int vreg_update_callback(unsigned reg, lbits value) { } -int pc_update_callback(uint64_t value) { } +int freg_write_callback(unsigned reg, uint64_t value) { } +int csr_write_callback(unsigned reg, uint64_t value) { } +int csr_read_callback(unsigned reg, uint64_t value) { } +int vreg_write_callback(unsigned reg, lbits value) { } +int pc_write_callback(uint64_t value) { } diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 913543144..dccb57775 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -89,6 +89,7 @@ bool config_print_reg = true; bool config_print_mem_access = true; bool config_print_platform = true; bool config_print_rvfi = false; +bool rv_enable_callbacks = true; void set_config_print(char *var, bool val) { @@ -98,6 +99,7 @@ void set_config_print(char *var, bool val) config_print_reg = val; config_print_platform = val; config_print_rvfi = val; + rv_enable_callbacks = val; } else if (strcmp("instr", var) == 0) { config_print_instr = val; } else if (strcmp("reg", var) == 0) { diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index 757c32a49..219874c38 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.sail @@ -23,17 +23,3 @@ end ext_read_CSR function clause ext_write_CSR (_, _) = None() end ext_write_CSR -function ext_notification_read_CSR (csr : csreg) -> option(xlenbits) = { - let res = ext_read_CSR(csr); - if rv_enable_callbacks then - match res { - Some(value) => csr_read_callback(csr_name_map(csr), value), - None() => (), - }; - res -} - -function ext_notification_write_CSR (csr : csreg, value : xlenbits) -> unit = { - let res = ext_write_CSR(csr, value); - if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value) -} diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 6c710b02e..93f4ea886 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -155,7 +155,7 @@ function rF (r : regno) -> flenbits = { function wF (r : regno, in_v : flenbits) -> unit = { assert(sys_enable_fdext()); - if rv_enable_callbacks then freg_update_callback(regno_to_regidx(r), in_v); + freg_write_callback(regno_to_regidx(r), in_v); let v = fregval_into_freg(in_v); match r { 0 => f0 = v, diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 1228cb307..bf8b63591 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -153,7 +153,8 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) Ext_DataAddr_Error(e) => { if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } }, @@ -161,14 +162,16 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) if check_misaligned(vaddr, width_type) then { if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } }, @@ -178,7 +181,8 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) MemException(e) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } } diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index f4861ee10..774f27522 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -49,10 +49,10 @@ function handle_illegal_vtype() = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions */ - let new_vtype = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); - ext_notification_write_CSR(csr_name_map("vl"), zeros()) + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vl = zeros(); + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); } val calculate_new_vl : (int, int) -> xlenbits @@ -77,8 +77,7 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -92,11 +91,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { if (rs1 != 0b00000) then { /* normal stripmining */ let rs1_val = X(rs1); let AVL = unsigned(rs1_val); - ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); + vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX)); + vl = to_bits(sizeof(xlen), VLMAX); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -105,7 +104,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { }; /* reset vstart to 0 */ - ext_notification_write_CSR(csr_name_map("vstart"), zeros()); + vstart = zeros(); + + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); + csr_write_callback(csr_name_map("vstart"), zero_extend(vstart)); RETIRE_SUCCESS } @@ -125,8 +128,7 @@ function clause execute VSETVL(rs2, rs1, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - let new_vtype = X(rs2); - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); + vtype.bits = X(rs2); /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -140,11 +142,11 @@ function clause execute VSETVL(rs2, rs1, rd) = { if (rs1 != 0b00000) then { /* normal stripmining */ let rs1_val = X(rs1); let AVL = unsigned(rs1_val); - ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); + vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX)); + vl = to_bits(sizeof(xlen), VLMAX); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -153,7 +155,11 @@ function clause execute VSETVL(rs2, rs1, rd) = { }; /* reset vstart to 0 */ - ext_notification_write_CSR(csr_name_map("vstart"), zeros()); + vstart = zeros(); + + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); + csr_write_callback(csr_name_map("vstart"), zero_extend(vstart)); RETIRE_SUCCESS } @@ -169,8 +175,7 @@ mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extensionEnable function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vtype */ - let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -182,11 +187,15 @@ function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vl according to VLMAX and AVL */ let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */ - ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); + vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; /* reset vstart to 0 */ - ext_notification_write_CSR(csr_name_map("vstart"), zeros()); + vstart = zeros(); + + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); + csr_write_callback(csr_name_map("vstart"), zero_extend(vstart)); RETIRE_SUCCESS } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index c69500a0e..3dec9b626 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -101,17 +101,18 @@ function readCSR csr : csreg -> xlenbits = { (0x015, _) => read_seed_csr(), _ => /* check extensions */ - match ext_notification_read_CSR(csr) { + match ext_read_CSR(csr) { Some(res) => res, None() => { print_bits("unhandled read to CSR ", csr); zero_extend(0x0) } } }; + csr_read_callback(csr, res); res } function writeCSR (csr : csreg, value : xlenbits) -> unit = { - if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value); + csr_write_callback(csr, value); let res : option(xlenbits) = match (csr, sizeof(xlen)) { /* machine mode */ @@ -183,6 +184,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { _ => ext_write_CSR(csr, value) }; + match res { + Some(v) => csr_write_callback(csr, v), + None() => print_bits("unhandled write to CSR ", csr) + } } function clause execute CSR(csr, rs1, rd, is_imm, op) = { diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 097669db7..3468ce702 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -132,11 +132,10 @@ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = { (false, true, true) => throw(Error_not_implemented("lr.rl")), (_, _, _) => checked_mem_read(typ, priv, paddr, width, aq, rl, res, meta) }; - if rv_enable_callbacks then - match result { - MemValue(value, _) => mem_read_callback(paddr, width, value, /* is_exception */ false), - MemException(_) => mem_read_callback(paddr, width, zeros(), /* is_exception */ true) - }; + match result { + MemValue(value, _) => mem_read_callback(paddr, width, value), + MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e)) + }; result } @@ -206,11 +205,10 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl then MemException(E_SAMO_Addr_Align()) else { let result = checked_mem_write(paddr, width, value, typ, priv, meta, aq, rl, con); - if rv_enable_callbacks then - match result { - MemValue(_) => mem_update_callback(paddr, width, value, /* is_exception */ false), - MemException(_) => mem_update_callback(paddr, width, value, /* is_exception */ true) - }; + match result { + MemValue(_) => mem_write_callback(paddr, width, value), + MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e)) + }; result } } diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index 4c8c43389..f69266328 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -28,6 +28,6 @@ function set_next_pc(pc) = { val tick_pc : unit -> unit function tick_pc() = { - if rv_enable_callbacks then pc_update_callback(PC); + pc_write_callback(PC); PC = nextPC } diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index 13dd2cc04..6d18e468e 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -126,7 +126,7 @@ function wX (r : regno, in_v : xlenbits) -> unit = { _ => assert(false, "invalid register number") }; if (r != 0) then { - if rv_enable_callbacks then xreg_update_callback(regno_to_regidx(r), in_v); + xreg_write_callback(regno_to_regidx(r), in_v); } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 40a763bad..ece9b1d3c 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -340,7 +340,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); prepare_trap_vector(del_priv, mcause) }, @@ -364,7 +364,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); prepare_trap_vector(del_priv, scause) }, @@ -383,7 +383,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); prepare_trap_vector(del_priv, ucause) } @@ -409,7 +409,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -424,7 +424,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -437,7 +437,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, mstatus[UPIE] = 0b1; cur_privilege = User; - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -544,7 +544,7 @@ function init_sys() -> unit = { // PMP's L and A fields are set to 0 on reset. init_pmp(); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); } /* memory access exceptions, defined here for use by the platform model. */ diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 03dc464ad..58178ae3a 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -43,8 +43,7 @@ type regno = range(0, 31) function regidx_to_regno (b : regidx) -> regno = unsigned(b) -val regno_to_regidx : {'n, 0 <= 'n < 32. regno('n)} -> bits(5) -function regno_to_regidx b = let 'r = to_bits(5, b) in r +function regno_to_regidx (b : regno) -> regidx = to_bits(5, b) /* mapping RVC register indices into normal indices */ val creg2reg_idx : cregidx -> regidx @@ -414,19 +413,13 @@ function report_invalid_width(f , l, w, k) -> 'a = { /* Callbacks for state-changing events */ -/* Whether need to call the callback functions */ -$ifdef RVFI_DII -register rv_enable_callbacks : bool = true -$else -register rv_enable_callbacks : bool = false -$endif - /* Defaults for these functions in riscv_default_callbacks.c and platform_impl.ml */ -val mem_update_callback = pure {ocaml: "Platform.mem_update_callback", c: "mem_update_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n), /* is exception */ bool) -> unit -val mem_read_callback = pure {ocaml: "Platform.mem_read_callback", c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n), /* is exception */ bool) -> unit -val pc_update_callback = pure {ocaml: "Platform.pc_update_callback", c: "pc_update_callback"} : xlenbits -> unit -val xreg_update_callback = pure {ocaml: "Platform.xreg_update_callback", c: "xreg_update_callback"} : (regidx, xlenbits) -> unit -val freg_update_callback = pure {ocaml: "Platform.freg_update_callback", c: "freg_update_callback"} : (regidx, flenbits) -> unit -val csr_update_callback = pure {ocaml: "Platform.csr_update_callback", c: "csr_update_callback"} : (/* name from the csr_name_map */ string, xlenbits) -> unit -val csr_read_callback = pure {ocaml: "Platform.csr_read_callback", c: "csr_read_callback"} : (/* name from the csr_name_map */ string, xlenbits) -> unit +val mem_write_callback = pure {ocaml: "Platform.mem_write_callback", c: "mem_write_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit +val mem_read_callback = pure {ocaml: "Platform.mem_read_callback", c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit +val mem_exception_callback = pure {ocaml: "Platform.mem_exception_callback", c: "mem_exception_callback"} : forall 'n, 0 <= 'n < xlen . (/* addr */ xlenbits, /* num_of_ExceptionType */ int('n)) -> unit +val pc_write_callback = pure {ocaml: "Platform.pc_write_callback", c: "pc_write_callback"} : xlenbits -> unit +val xreg_write_callback = pure {ocaml: "Platform.xreg_write_callback", c: "xreg_write_callback"} : (regidx, xlenbits) -> unit +val freg_write_callback = pure {ocaml: "Platform.freg_write_callback", c: "freg_write_callback"} : (regidx, flenbits) -> unit +val csr_write_callback = pure {ocaml: "Platform.csr_write_callback", c: "csr_write_callback"} : (csreg, xlenbits) -> unit +val csr_read_callback = pure {ocaml: "Platform.csr_read_callback", c: "csr_read_callback"} : (csreg, xlenbits) -> unit diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index a80e4eba4..60198d4ae 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -169,7 +169,7 @@ function wV (r : regno, in_v : vregtype) -> unit = { let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); - if rv_enable_callbacks then vreg_update_callback(regno_to_regidx(r), v); + vreg_write_callback(regno_to_regidx(r), v); } function rV_bits(i: regidx) -> vregtype = rV(unsigned(i)) diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail index 79190955c..5ab69305a 100755 --- a/model/riscv_vreg_type.sail +++ b/model/riscv_vreg_type.sail @@ -150,4 +150,4 @@ enum vmlsop = { VLM, VSM } /* Callbacks for vregs state-changing events */ /* Default for this function in riscv_default_callbacks.c and platform_impl.ml */ -val vreg_update_callback = pure {ocaml: "Platform.vreg_update_callback", c: "vreg_update_callback"} : (regidx, vregtype) -> unit +val vreg_write_callback = pure {ocaml: "Platform.vreg_write_callback", c: "vreg_write_callback"} : (regidx, vregtype) -> unit diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 5afb685fb..99b88a70e 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -330,12 +330,10 @@ function print_rvfi_exec () = { val internal_error : forall ('a : Type). (string, int, string) -> 'a -val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), bool) -> unit -function rvfi_write (addr, width, value, is_exception) = { +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n)) -> unit +function rvfi_write (addr, width, value) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; - /* Log only the memory address (without the value) if the write fails. */ - if is_exception == false then { 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); @@ -343,15 +341,12 @@ function rvfi_write (addr, width, value, is_exception) = { } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); }; - }; } -val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), bool) -> unit -function rvfi_read (addr, width, value, is_exception) = { +val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> unit +function rvfi_read (addr, width, value) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; - /* Log only the memory address (without the value) if the write fails. */ - if is_exception == false then { if width <= 16 then { /* TODO: report tag bit for capability writes and extend mask by one bit. */ rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(value, 256); @@ -359,7 +354,13 @@ function rvfi_read (addr, width, value, is_exception) = { } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") }; - }; +} + +val rvfi_mem_exception : xlenbits -> unit +function rvfi_mem_exception (addr) = { + /* Log only the memory address (without the value) if the write fails. */ + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); + rvfi_mem_data_present = true; } val rvfi_wX : forall 'n, 0 <= 'n < 32. (int('n), xlenbits) -> unit diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 8a6632c9b..0c8422641 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -25,14 +25,15 @@ let platform_arch = ref P.RV64 (* Defaults for callbacks functions. The model assumes that these functions do not change the state of the model. *) -let mem_update_callback (addr, width, value, is_exception) = () -let mem_read_callback (addr, width, value, is_exception) = () -let pc_update_callback value = () -let xreg_update_callback (reg, value) = () -let freg_update_callback (reg, value) = () -let csr_update_callback (reg_name, value) = () -let csr_read_callback (reg_name, value) = () -let vreg_update_callback (reg, value) = () +let mem_write_callback (addr, width, value) = () +let mem_read_callback (addr, width, value) = () +let mem_exception_callback (addr, num_of_exception) = () +let pc_write_callback value = () +let xreg_write_callback (reg, value) = () +let freg_write_callback (reg, value) = () +let csr_write_callback (reg, value) = () +let csr_read_callback (reg, value) = () +let vreg_write_callback (reg, value) = () (* logging *)