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.

Sign up for GitHub

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

Add Debug Native Trigger Support #573

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
0b55df2
Add Debug Native Trigger Support
YazanHussnain-10x Oct 4, 2024
9f9b2e6
add remaining mcontrol6 match options
YazanHussnain-10x Oct 4, 2024
3421b03
replace sizeof(xlen) with xlen
YazanHussnain-10x Oct 4, 2024
dd87a8a
resolve error in NAPOT match option
YazanHussnain-10x Oct 4, 2024
b5c5a92
Add standard trigger for vector operations
YazanHussnain-10x Oct 9, 2024
38a1670
Update --reent-opt1 description
YazanHussnain-10x Oct 9, 2024
97e77f5
resolve reenterancy implementation issues
YazanHussnain-10x Oct 10, 2024
2a6aa63
resolve error in load data match
YazanHussnain-10x Oct 10, 2024
60e45de
Fix comment
YazanHussnain-10x Oct 29, 2024
0bd7e49
review changes and remove trailing whitespaces
YazanHussnain-10x Oct 29, 2024
232d922
remove trailing whitespaces
YazanHussnain-10x Oct 29, 2024
cab0f37
Apply suggestions from code review
YazanHussnain-10x Oct 31, 2024
cd5eb34
change mcontrol6.hit0/1 comment
YazanHussnain-10x Oct 31, 2024
b46a99a
resolve error in the interruptType encodings
YazanHussnain-10x Oct 31, 2024
b587644
review changes
YazanHussnain-10x Nov 2, 2024
40ad532
review changes cbo.*
YazanHussnain-10x Nov 8, 2024
fb13ad0
incorporate new type changes
YazanHussnain-10x Dec 21, 2024
5ea9eec
remove trailing whitespaces
YazanHussnain-10x Dec 22, 2024
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
View file
Open in desktop
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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This name doesn't mean much unless you know it relates to Sdtrig, which isn't clear. Also, is there a better name that captures what it actually does than "option 1"? Finally, without knowing the Sdtrig spec, the name doesn't make it clear what false, i.e. not "option 1", means.

{
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
Binary file not shown.
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras.lem
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passing 0b0 for every LOAD_MATCH_BEFORE is odd. Does that not mean a trigger on loading 0 will fire for every load? I imagine you instead want the data to be an optional type here and pass None() so it never matches. This is also what Spike implements. But I can't see this detail in the spec, not helped by the match algorithm being split across each field of the CSR.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It may also make sense to have two functions, one for the cases where the exception is raised now, and one for the cases where the exception is raised later. Currently the code here is implicitly assuming that LOAD_MATCH_BEFORE raises an exception, since it returns RETIRE_FAIL, and that LOAD_MATCH_AFTER doesn't, since it continues on to return RETIRE_SUCCESS. Maybe the former should also have the handle_mem_exception call in the caller here like all the other ways this can fault.

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);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why put the result in an unused variable?

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);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the actual store data, not just the debug value. But also it's weird to introduce a variable for the new code whilst not updating the existing code to use it. And you still have redundancy in slicing the right bytes out. Hoist the existing store code and use it for both.


// 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
View file
Open in desktop
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