Skip to content

Commit

Permalink
Implementing callbacks in sail-riscv for state-changing events
Browse files Browse the repository at this point in the history
  Pushed all the rv_enable_callbacks into the callback functions.
  • Loading branch information
kseniadobrovolskaya committed Jul 24, 2024
1 parent 5adc0bd commit 10348eb
Show file tree
Hide file tree
Showing 19 changed files with 133 additions and 127 deletions.
1 change: 1 addition & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_config.h
Original file line number Diff line number Diff line change
Expand Up @@ -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;
23 changes: 9 additions & 14 deletions c_emulator/riscv_default_callbacks.c
Original file line number Diff line number Diff line change
@@ -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) { }
48 changes: 29 additions & 19 deletions c_emulator/riscv_rvfi_callbacks.c
Original file line number Diff line number Diff line change
@@ -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) { }
2 changes: 2 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{
Expand All @@ -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) {
Expand Down
14 changes: 0 additions & 14 deletions model/riscv_csr_ext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
2 changes: 1 addition & 1 deletion model/riscv_fdext_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
12 changes: 8 additions & 4 deletions model/riscv_insts_vext_mem.sail
Original file line number Diff line number Diff line change
Expand Up @@ -153,22 +153,25 @@ 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
}
},
Ext_DataAddr_OK(vaddr) => {
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
}
},
Expand All @@ -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
}
}
Expand Down
45 changes: 27 additions & 18 deletions model/riscv_insts_vext_vset.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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();
Expand All @@ -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);
Expand All @@ -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
}
Expand All @@ -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();
Expand All @@ -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);
Expand All @@ -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
}
Expand All @@ -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();
Expand All @@ -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
}
Expand Down
9 changes: 7 additions & 2 deletions model/riscv_insts_zicsr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down Expand Up @@ -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) = {
Expand Down
18 changes: 8 additions & 10 deletions model/riscv_mem.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

Expand Down Expand Up @@ -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
}
}
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_pc_access.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
2 changes: 1 addition & 1 deletion model/riscv_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}

Expand Down
Loading

0 comments on commit 10348eb

Please sign in to comment.