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 09acccc
Show file tree
Hide file tree
Showing 20 changed files with 142 additions and 165 deletions.
27 changes: 1 addition & 26 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -287,32 +287,6 @@ rvfi: c_emulator/riscv_rvfi_$(ARCH)
c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@

# Note: We have to add -c_preserve since the functions might be optimized out otherwise
rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
-c_preserve rvfi_get_cmd \
-c_preserve rvfi_get_insn \
-c_preserve rvfi_get_v2_trace_size \
-c_preserve rvfi_get_v2_support_packet \
-c_preserve rvfi_get_exec_packet_v1 \
-c_preserve rvfi_get_exec_packet_v2 \
-c_preserve rvfi_get_mem_data \
-c_preserve rvfi_get_int_data \
-c_preserve rvfi_zero_exec_packet \
-c_preserve rvfi_halt_exec_packet \
-c_preserve print_rvfi_exec \
-c_preserve print_instr_packet \
-c_preserve print_rvfi_exec

# 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) $(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 $@

c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@

# Note: We have to add -c_preserve since the functions might be optimized out otherwise
rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
-c_preserve rvfi_get_cmd \
Expand All @@ -327,6 +301,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) { }
20 changes: 9 additions & 11 deletions c_emulator/riscv_sail.h
Original file line number Diff line number Diff line change
Expand Up @@ -52,19 +52,17 @@ extern bool have_exception;

/* Callbacks for state-changing events */

/* Whether need to call the callback functions */
extern bool zrv_enable_callbacks;
/* 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 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);

/* machine state */

Expand Down
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
15 changes: 0 additions & 15 deletions model/riscv_csr_ext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -22,18 +22,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
Loading

0 comments on commit 09acccc

Please sign in to comment.