Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Debug Native Trigger Support #573

Open
wants to merge 18 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,11 @@ bool sys_enable_zicbom(unit u)
return rv_enable_zicbom;
}

bool sys_reent_opt1(unit u)
{
return rv_reent_opt1;
}

bool sys_enable_zicboz(unit u)
{
return rv_enable_zicboz;
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ bool sys_enable_writable_fiom(unit);
bool sys_enable_vext(unit);
bool sys_enable_bext(unit);
bool sys_enable_zicbom(unit);
bool sys_reent_opt1(unit);
bool sys_enable_zicboz(unit);
bool sys_enable_sstc(unit);

Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ bool rv_enable_fdext = true;
bool rv_enable_vext = true;
bool rv_enable_bext = false;
bool rv_enable_zicbom = false;
bool rv_reent_opt1 = false;
bool rv_enable_zicboz = false;
bool rv_enable_sstc = false;

Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ extern bool rv_enable_fdext;
extern bool rv_enable_vext;
extern bool rv_enable_bext;
extern bool rv_enable_zicbom;
extern bool rv_reent_opt1;
extern bool rv_enable_zicboz;
extern bool rv_enable_sstc;
extern bool rv_enable_writable_misa;
Expand Down
6 changes: 6 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ enum {
OPT_ENABLE_ZICBOM,
OPT_ENABLE_ZICBOZ,
OPT_ENABLE_SSTC,
OPT_REENT_OPT1,
OPT_CACHE_BLOCK_SIZE,
};

Expand Down Expand Up @@ -159,6 +160,7 @@ static struct option options[] = {
{"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB },
{"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM },
{"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ },
{"reent-opt1", no_argument, 0, OPT_REENT_OPT1 },
{"cache-block-size", required_argument, 0, OPT_CACHE_BLOCK_SIZE },
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c' },
Expand Down Expand Up @@ -425,6 +427,10 @@ static int process_args(int argc, char **argv)
fprintf(stderr, "enabling Zicbom extension.\n");
rv_enable_zicbom = true;
break;
case OPT_REENT_OPT1:
fprintf(stderr, "Selecting Sdtrig reentrancy Option 1. \n");
rv_reent_opt1 = true;
break;
case OPT_ENABLE_ZICBOZ:
fprintf(stderr, "enabling Zicboz extension.\n");
rv_enable_zicboz = true;
Expand Down
Binary file added c_emulator/riscv_sim_RV64
Binary file not shown.
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,10 @@ val plat_rom_size : unit -> bitvector
let plat_rom_size () = []
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`

val sys_reent_opt1 : unit -> bool
let sys_reent_opt1 () = false
declare ocaml target_rep function sys_reent_opt1 = `Platform.reent_opt1`

val plat_cache_block_size_exp : unit -> bitvector
let plat_cache_block_size_exp () = []
declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras_sequential.lem
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_rom_size () = wordFromInteger 0
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`

val sys_reent_opt1 : unit -> bool
let sys_reent_opt1 () = false
declare ocaml target_rep function sys_reent_opt1 = `Platform.reent_opt1`

val plat_cache_block_size_exp : unit -> integer
let plat_cache_block_size_exp () = wordFromInteger 0
declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp`
Expand Down
16 changes: 13 additions & 3 deletions model/riscv_insts_aext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -86,13 +86,20 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
/* "LR faults like a normal load, even though it's in the AMO major opcode space."
* - Andrew Waterman, isa-dev, 10 Jul 2018.
*/
if not(is_aligned(virtaddr_bits(vaddr), width))
if (instrDataMatch(cur_privilege, virtaddr_bits(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width), LOAD_MATCH_BEFORE))
then { RETIRE_FAIL }
else if not(is_aligned(virtaddr_bits(vaddr), width))
then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) =>
match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
MemValue(result) => { load_reservation(physaddr_bits(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS },
MemValue(result) => {
load_reservation(physaddr_bits(addr));
X(rd) = sign_extend(result);
let load_after_match : bool = instrDataMatch(cur_privilege, virtaddr_bits(vaddr), zero_extend(X(rd)), matchSize_of_wordWidth(width), LOAD_MATCH_AFTER);
RETIRE_SUCCESS
},
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
},
}
Expand All @@ -112,6 +119,7 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)
/* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
let width_bytes = size_bytes(width);
let dbg_store_data = X(rs2);

// This is checked during decoding.
assert(width_bytes <= xlen_bytes);
Expand All @@ -131,7 +139,9 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
if not(is_aligned(virtaddr_bits(vaddr), width))
if (instrDataMatch(cur_privilege, virtaddr_bits(vaddr), zero_extend(dbg_store_data[width_bytes * 8 - 1 .. 0]), matchSize_of_wordWidth(width), STORE_MATCH))
then { RETIRE_FAIL }
else if not(is_aligned(virtaddr_bits(vaddr), width))
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else {
match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
Expand Down
15 changes: 12 additions & 3 deletions model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -334,14 +334,20 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
if check_misaligned(vaddr, width)
if (instrDataMatch(cur_privilege, virtaddr_bits(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width), LOAD_MATCH_BEFORE))
then { RETIRE_FAIL }
else if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(paddr, _) =>

match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) {
MemValue(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
MemValue(result) => {
X(rd) = extend_value(is_unsigned, result);
let load_after_match : bool = instrDataMatch(cur_privilege, virtaddr_bits(vaddr), zero_extend(X(rd)), matchSize_of_wordWidth(width), LOAD_MATCH_AFTER);
RETIRE_SUCCESS
},
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
},
}
Expand Down Expand Up @@ -381,6 +387,7 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
let width_bytes = size_bytes(width);
let dbg_store_data = X(rs2);

// This is checked during decoding.
assert(width_bytes <= xlen_bytes);
Expand All @@ -390,7 +397,9 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
if (instrDataMatch(cur_privilege, virtaddr_bits(vaddr), zero_extend(dbg_store_data[width_bytes * 8 - 1 .. 0]), matchSize_of_wordWidth(width), STORE_MATCH))
then { RETIRE_FAIL }
else if check_misaligned(vaddr, width)
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
Expand Down
Loading
Loading