diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index ae67bac42..dc3801f57 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -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; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index fe81c901b..2f4f1b6bb 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -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); uint64_t sys_pmp_count(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 2713715cc..5dca55720 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -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_dirty_update = false; diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index 8bda5e624..747cb7c73 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -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_writable_misa; extern bool rv_enable_dirty_update; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 78838462a..7acc8d82e 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -58,6 +58,7 @@ enum { OPT_ENABLE_ZCB, OPT_ENABLE_ZICBOM, OPT_ENABLE_ZICBOZ, + OPT_REENT_OPT1, OPT_CACHE_BLOCK_SIZE, }; @@ -158,6 +159,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' }, @@ -424,6 +426,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; diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 245a7fe80..695b4c930 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -193,6 +193,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` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index 5ffe482cd..e765e5454 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -173,6 +173,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` diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail index 053776435..b01b15ad3 100644 --- a/model/riscv_csr_begin.sail +++ b/model/riscv_csr_begin.sail @@ -306,6 +306,8 @@ mapping clause csr_name_map = 0x7a0 <-> "tselect" mapping clause csr_name_map = 0x7a1 <-> "tdata1" mapping clause csr_name_map = 0x7a2 <-> "tdata2" mapping clause csr_name_map = 0x7a3 <-> "tdata3" +mapping clause csr_name_map = 0x7a4 <-> "tinfo" +mapping clause csr_name_map = 0x7a5 <-> "tcontrol" /* vector csrs */ mapping clause csr_name_map = 0x008 <-> "vstart" mapping clause csr_name_map = 0x009 <-> "vxsat" diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 17863b820..7bebdc65e 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -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(vaddr, width)) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width), LOAD_MATCH_BEFORE)) + then { RETIRE_FAIL } + else if not(is_aligned(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(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS }, + MemValue(result) => { + load_reservation(addr); + X(rd) = sign_extend(result); + let load_after_match : bool = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(X(rd)), matchSize_of_wordWidth(width), LOAD_MATCH_AFTER); + RETIRE_SUCCESS + }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } }, } @@ -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); @@ -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(vaddr, width)) + if (instrDataMatch(cur_privilege, zero_extend(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(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: diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 1510dd425..f1a7bf028 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -332,14 +332,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, zero_extend(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, zero_extend(vaddr), zero_extend(X(rd)), matchSize_of_wordWidth(width), LOAD_MATCH_AFTER); + RETIRE_SUCCESS + }, MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, }, } @@ -379,6 +385,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); @@ -388,7 +395,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, zero_extend(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 }, diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index cc8161304..5bb00b60b 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -61,6 +61,13 @@ mapping vlewidth_pow : vlewidth <-> {3, 4, 5, 6} = { VLE64 <-> 6 } +mapping matchSize_of_vlewidth : vlewidth <-> matchSize = { + VLE8 <-> BITS_8, + VLE16 <-> BITS_16, + VLE32 <-> BITS_32, + VLE64 <-> BITS_64 +} + /* ******************** Vector Load Unit-Stride Normal & Segment (mop=0b00, lumop=0b00000) ********************* */ union clause ast = VLSEGTYPE : (bits(3), bits(1), regidx, vlewidth, regidx) @@ -84,13 +91,20 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width_type), LOAD_MATCH_BEFORE)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), + MemValue(elem) => { + if (xlen_bytes >= load_width_bytes) then { + let load_after_match : bool = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(elem), matchSize_of_wordWidth(width_type), LOAD_MATCH_AFTER); + }; + write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem) + }, MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } @@ -159,7 +173,9 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) } }, Ext_DataAddr_OK(vaddr) => { - if check_misaligned(vaddr, width_type) then { + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width_type), LOAD_MATCH_BEFORE)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else { vl = to_bits(xlen, i); @@ -177,7 +193,12 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), + MemValue(elem) => { + if (xlen_bytes >= load_width_bytes) then { + let load_after_match : bool = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(elem), matchSize_of_wordWidth(width_type), LOAD_MATCH_AFTER); + }; + write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem) + }, MemException(e) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { @@ -245,16 +266,23 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); + var trigMatched : bool = false; foreach (i from 0 to (num_elem - 1)) { if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; + let dbg_elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg)); match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + Ext_DataAddr_OK(vaddr) => { + if (xlen_bytes >= load_width_bytes) then { + trigMatched = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(dbg_elem_val), matchSize_of_wordWidth(width_type), STORE_MATCH); + }; + if (trigMatched) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -274,6 +302,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) } } } + } } } } @@ -325,13 +354,20 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width_type), LOAD_MATCH_BEFORE)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem), + MemValue(elem) => { + if (xlen_bytes >= load_width_bytes) then { + let load_after_match : bool = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(elem), matchSize_of_wordWidth(width_type), LOAD_MATCH_AFTER); + }; + write_single_element(load_width_bytes * 8, i, vd + to_bits(5, j * EMUL_reg), elem) + }, MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } @@ -382,16 +418,23 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); let rs2_val : int = unsigned(get_scalar(rs2, xlen)); let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); + var trigMatched : bool = false; foreach (i from 0 to (num_elem - 1)) { if mask[i] then { /* active segments */ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; + let dbg_elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, j * EMUL_reg)); match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + Ext_DataAddr_OK(vaddr) => { + if (xlen_bytes >= load_width_bytes) then { + trigMatched = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(dbg_elem_val), matchSize_of_wordWidth(width_type), STORE_MATCH); + }; + if (trigMatched) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -411,6 +454,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ } } } + } } } } @@ -463,13 +507,20 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width_type), LOAD_MATCH_BEFORE)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, EEW_data_bytes, false, false, false) { - MemValue(elem) => write_single_element(EEW_data_bytes * 8, i, vd + to_bits(5, j * EMUL_data_reg), elem), + MemValue(elem) => { + if (xlen_bytes >= EEW_data_bytes) then { + let load_after_match : bool = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(elem), matchSize_of_wordWidth(width_type), LOAD_MATCH_AFTER); + }; + write_single_element(EEW_data_bytes * 8, i, vd + to_bits(5, j * EMUL_data_reg), elem) + }, MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } @@ -544,6 +595,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde let vs3_seg : vector('n, bits('f * 'db * 8)) = read_vreg_seg(num_elem, EEW_data_bytes * 8, EMUL_data_pow, nf, vs3); let vs2_val : vector('n, bits('ib * 8)) = read_vreg(num_elem, EEW_index_bytes * 8, EMUL_index_pow, vs2); let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_data_pow, vm_val); + var trigMatched : bool = false; /* currently mop = 1 (unordered) or 3 (ordered) do the same operations */ foreach (i from 0 to (num_elem - 1)) { @@ -551,10 +603,16 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset : int = unsigned(vs2_val[i]) + j * EEW_data_bytes; + let dbg_elem_val : bits('db * 8) = read_single_element(EEW_data_bytes * 8, i, vs3 + to_bits(5, j * EMUL_data_reg)); match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + Ext_DataAddr_OK(vaddr) => { + if (xlen_bytes >= EEW_data_bytes) then { + trigMatched = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(dbg_elem_val), matchSize_of_wordWidth(width_type), STORE_MATCH); + }; + if (trigMatched) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -574,6 +632,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde } } } + } } } } @@ -647,13 +706,20 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width_type), LOAD_MATCH_BEFORE)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, load_width_bytes, false, false, false) { - MemValue(elem) => write_single_element(load_width_bytes * 8, i, vd + to_bits(5, cur_field), elem), + MemValue(elem) => { + if (xlen_bytes >= load_width_bytes) then { + let load_after_match : bool = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(elem), matchSize_of_wordWidth(width_type), LOAD_MATCH_AFTER); + }; + write_single_element(load_width_bytes * 8, i, vd + to_bits(5, cur_field), elem) + }, MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } @@ -671,7 +737,9 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width_type), LOAD_MATCH_BEFORE)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -721,15 +789,22 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { let elem_to_align : int = start_element % elem_per_reg; var cur_field : int = start_element / elem_per_reg; var cur_elem : int = start_element; + var trigMatched : bool = false; if elem_to_align > 0 then { foreach (i from elem_to_align to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset : int = cur_elem * load_width_bytes; + let dbg_elem_val : bits('b * 8) = read_single_element(load_width_bytes * 8, i, vs3 + to_bits(5, cur_field)); match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + Ext_DataAddr_OK(vaddr) => { + if (xlen_bytes >= load_width_bytes) then { + trigMatched = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(dbg_elem_val), matchSize_of_wordWidth(width_type), STORE_MATCH); + }; + if (trigMatched) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -749,12 +824,14 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { } } } + } }; cur_elem = cur_elem + 1 }; cur_field = cur_field + 1 }; + trigMatched = false; foreach (j from cur_field to (nf - 1)) { let vs3_val : vector('n, bits('b * 8)) = read_vreg(elem_per_reg, load_width_bytes * 8, 0, vs3 + to_bits(5, j)); foreach (i from 0 to (elem_per_reg - 1)) { @@ -762,8 +839,13 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { let elem_offset = cur_elem * load_width_bytes; match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, - Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + Ext_DataAddr_OK(vaddr) => { + if (xlen_bytes >= load_width_bytes) then { + trigMatched = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(vs3_val[i]), matchSize_of_wordWidth(width_type), STORE_MATCH); + }; + if (trigMatched) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, @@ -782,6 +864,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { } } } + } }; cur_elem = cur_elem + 1 } @@ -831,13 +914,18 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { match ext_data_get_addr(rs1, to_bits(xlen, i), Read(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), matchSize_of_wordWidth(width_type), LOAD_MATCH_BEFORE)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, TR_Address(paddr, _) => { match mem_read(Read(Data), paddr, 1, false, false, false) { - MemValue(elem) => write_single_element(8, i, vd_or_vs3, elem), + MemValue(elem) => { + let load_after_match : bool = instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(elem), matchSize_of_wordWidth(width_type), LOAD_MATCH_AFTER); + write_single_element(8, i, vd_or_vs3, elem) + }, MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL } } } @@ -847,7 +935,9 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { match ext_data_get_addr(rs1, to_bits(xlen, i), Write(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => - if check_misaligned(vaddr, width_type) + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(vd_or_vs3_val[i]), matchSize_of_wordWidth(width_type), STORE_MATCH)) + then { return RETIRE_FAIL } + else if check_misaligned(vaddr, width_type) then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); return RETIRE_FAIL } else match translateAddr(vaddr, Write(Data)) { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }, diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index a8fdd8bcb..c36478cd8 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -52,47 +52,51 @@ function process_clean_inval(rs1, cbop) = { match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { - TR_Address(paddr, _) => { - // "A cache-block management instruction is permitted to access the - // specified cache block whenever a load instruction or store instruction - // is permitted to access the corresponding physical addresses. If - // neither a load instruction nor store instruction is permitted to - // access the physical addresses, but an instruction fetch is permitted - // to access the physical addresses, whether a cache-block management - // instruction is permitted to access the cache block is UNSPECIFIED." - // - // In this implementation we currently don't allow access for fetches. - let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size); - let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size); - match (exc_read, exc_write) { - // Access is permitted if read OR write are allowed. If neither - // are allowed then we always report a store exception. - (Some(exc_read), Some(exc_write)) => Some(exc_write), - _ => None(), + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), cacheBlockSize_to_matchSize(cache_block_size_exp), STORE_MATCH)) + then { RETIRE_FAIL } + else { + let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { + TR_Address(paddr, _) => { + // "A cache-block management instruction is permitted to access the + // specified cache block whenever a load instruction or store instruction + // is permitted to access the corresponding physical addresses. If + // neither a load instruction nor store instruction is permitted to + // access the physical addresses, but an instruction fetch is permitted + // to access the physical addresses, whether a cache-block management + // instruction is permitted to access the cache block is UNSPECIFIED." + // + // In this implementation we currently don't allow access for fetches. + let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size); + let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size); + match (exc_read, exc_write) { + // Access is permitted if read OR write are allowed. If neither + // are allowed then we always report a store exception. + (Some(exc_read), Some(exc_write)) => Some(exc_write), + _ => None(), + } + }, + TR_Failure(e, _) => Some(e) + }; + // "If access to the cache block is not permitted, a cache-block management + // instruction raises a store page fault or store guest-page fault exception + // if address translation does not permit any access or raises a store access + // fault exception otherwise." + match res { + // The model has no caches so there's no action required. + None() => RETIRE_SUCCESS, + Some(e) => { + let e : ExceptionType = match e { + E_Load_Access_Fault() => E_SAMO_Access_Fault(), + E_SAMO_Access_Fault() => E_SAMO_Access_Fault(), + E_Load_Page_Fault() => E_SAMO_Page_Fault(), + E_SAMO_Page_Fault() => E_SAMO_Page_Fault(), + // No other exceptions should be generated since we're not checking + // for fetch access and it's can't be misaligned. + _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"), + }; + handle_mem_exception(vaddr, e); + RETIRE_FAIL } - }, - TR_Failure(e, _) => Some(e) - }; - // "If access to the cache block is not permitted, a cache-block management - // instruction raises a store page fault or store guest-page fault exception - // if address translation does not permit any access or raises a store access - // fault exception otherwise." - match res { - // The model has no caches so there's no action required. - None() => RETIRE_SUCCESS, - Some(e) => { - let e : ExceptionType = match e { - E_Load_Access_Fault() => E_SAMO_Access_Fault(), - E_SAMO_Access_Fault() => E_SAMO_Access_Fault(), - E_Load_Page_Fault() => E_SAMO_Page_Fault(), - E_SAMO_Page_Fault() => E_SAMO_Page_Fault(), - // No other exceptions should be generated since we're not checking - // for fetch access and it's can't be misaligned. - _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"), - }; - handle_mem_exception(vaddr, e); - RETIRE_FAIL } } } diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail index abf18dc82..9842c7c29 100644 --- a/model/riscv_insts_zicboz.sail +++ b/model/riscv_insts_zicboz.sail @@ -35,22 +35,26 @@ function clause execute(RISCV_ZICBOZ(rs1)) = { match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - // "An implementation may update the bytes in any order and with any granularity - // and atomicity, including individual bytes." - // - // This implementation does a single atomic write. - match translateAddr(vaddr, Write(Data)) { - TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(paddr, _) => { - let eares : MemoryOpResult(unit) = mem_write_ea(paddr, cache_block_size, false, false, false); - match (eares) { - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - MemValue(_) => { - let res : MemoryOpResult(bool) = mem_write_value(paddr, cache_block_size, zeros(), false, false, false); - match (res) { - MemValue(true) => RETIRE_SUCCESS, - MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + if (instrDataMatch(cur_privilege, zero_extend(vaddr), zero_extend(0b0), cacheBlockSize_to_matchSize(cache_block_size_exp), STORE_MATCH)) + then { RETIRE_FAIL } + else { + // "An implementation may update the bytes in any order and with any granularity + // and atomicity, including individual bytes." + // + // This implementation does a single atomic write. + match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, cache_block_size, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, cache_block_size, zeros(), false, false, false); + match (res) { + MemValue(true) => RETIRE_SUCCESS, + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } } } } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 5e4d47b9e..c40fa0ade 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -70,7 +70,12 @@ function clause read_CSR(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(ind function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index)) /* trigger/debug */ -function clause read_CSR(0x7a0) = ~(tselect) /* this indicates we don't have any trigger support */ +function clause read_CSR(0x7a0) = tselect +function clause read_CSR(0x7a1) = tdata1_read(tselect) +function clause read_CSR(0x7a2) = tdata2_read(tselect) +function clause read_CSR(0x7a3) = tdata3_read(tselect) +function clause read_CSR(0x7a4) = tinfo_read(tselect) +function clause read_CSR(0x7a5) = tcontrol.bits /* supervisor mode */ function clause read_CSR(0x100) = lower_mstatus(mstatus).bits @@ -156,7 +161,11 @@ function clause write_CSR((0b1011100 /* 0xB80 */ @ index : bits(5), value) if xl } /* trigger/debug */ -function clause write_CSR(0x7a0, value) = { tselect = value; tselect } +function clause write_CSR(0x7a0, value) = { tselect = legalize_tselect(tselect, value); tselect } +function clause write_CSR(0x7a1, value) = { tdata1 = tdata1_write(tselect, tdata1_read(tselect), value); tdata1 } +function clause write_CSR(0x7a2, value) = { tdata2 = tdata2_write(tselect, tdata2_read(tselect), value); tdata2 } +function clause write_CSR(0x7a3, value) = { tdata3 = tdata3_write(tselect, tdata3_read(tselect), value); tdata3 } +function clause write_CSR(0x7a5, value) = { tcontrol.bits = legalize_tcontrol(value); tcontrol.bits } /* supervisor mode */ function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 21bd82e47..c4def6eaf 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -32,46 +32,68 @@ function step(step_no : int) -> bool = { (RETIRE_FAIL, false) }, None() => { - /* the extension hook interposes on the fetch result */ - match ext_fetch_hook(fetch()) { - /* extension error */ - F_Ext_Error(e) => { - ext_handle_fetch_check_error(e); - (RETIRE_FAIL, false) - }, - /* standard error */ - F_Error(e, addr) => { - handle_mem_exception(addr, e); - (RETIRE_FAIL, false) - }, - /* non-error cases: */ - F_RVC(h) => { - sail_instr_announce(h); - instbits = zero_extend(h); - let ast = ext_decode_compressed(h); - if get_config_print_instr() - then { - print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); - }; - /* check for RVC once here instead of every RVC execute clause. */ - if extensionEnabled(Ext_Zca) then { - nextPC = PC + 2; - (execute(ast), true) - } else { - handle_illegal(); - (RETIRE_FAIL, true) + /* If Etrigger, Icount, Itrigger and mcontrol6 after, matches, fire + it before fetching the next instruction */ + if (check_trigger_firing(cur_privilege)) then { + (RETIRE_FAIL, false) + } + else { + /* the extension hook interposes on the fetch result */ + match ext_fetch_hook(fetch()) { + /* extension error */ + F_Ext_Error(e) => { + if not(instrDataMatch(cur_privilege, PC, zero_extend(0b0), ANY, INSTR_MATCH)) then { + ext_handle_fetch_check_error(e); + }; + (RETIRE_FAIL, false) + }, + /* standard error */ + F_Error(e, addr) => { + if not(instrDataMatch(cur_privilege, PC, zero_extend(0b0), ANY, INSTR_MATCH)) then { + handle_mem_exception(addr, e); + }; + (RETIRE_FAIL, false) + }, + /* non-error cases: */ + F_RVC(h) => { + sail_instr_announce(h); + instbits = zero_extend(h); + let ast = ext_decode_compressed(h); + if get_config_print_instr() + then { + print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast)); + }; + /* Check for mcontrol6 Instruction Match */ + if (instrDataMatch(cur_privilege, PC, zero_extend(h), BITS_16, INSTR_MATCH)) then { + (RETIRE_FAIL, true) + } + /* check for RVC once here instead of every RVC execute clause. */ + else if extensionEnabled(Ext_Zca) then { + nextPC = PC + 2; + icount_trigger_match(cur_privilege); /* Decrement instruction count */ + (execute(ast), true) + } else { + handle_illegal(); + (RETIRE_FAIL, true) + } + }, + F_Base(w) => { + sail_instr_announce(w); + instbits = zero_extend(w); + let ast = ext_decode(w); + if get_config_print_instr() + then { + print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); + }; + nextPC = PC + 4; + icount_trigger_match(cur_privilege); /* Decrement instruction count */ + /* Check for mcontrol6 Instruction Match */ + if not(instrDataMatch(cur_privilege, PC, zero_extend(w), BITS_32, INSTR_MATCH)) then { + (execute(ast), true) + } else { + (RETIRE_FAIL, true) + } } - }, - F_Base(w) => { - sail_instr_announce(w); - instbits = zero_extend(w); - let ast = ext_decode(w); - if get_config_print_instr() - then { - print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); - }; - nextPC = PC + 4; - (execute(ast), true) } } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 620240cb9..177e1ad03 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -68,8 +68,13 @@ function clause is_CSR_defined(0xB82) = xlen == 32 // minstreth function clause is_CSR_defined(0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & (xlen == 32) // mhpmcounterh3..31 -/* disabled trigger/debug module */ +/* trigger/debug module */ function clause is_CSR_defined(0x7a0) = true +function clause is_CSR_defined(0x7a1) = true +function clause is_CSR_defined(0x7a2) = true +function clause is_CSR_defined(0x7a3) = true +function clause is_CSR_defined(0x7a4) = true +function clause is_CSR_defined(0x7a5) = true /* supervisor mode: trap setup */ function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus @@ -289,6 +294,71 @@ val rvfi_trap : unit -> unit function rvfi_trap () = () $endif +/* Disable trigger firing in trap handler */ +function TriggerFireMatch(cur_priv : Privilege) -> bool = { + /* Second solution of reentrancy problem */ + if (sys_reent_opt1()) then { + match cur_priv { + Machine => bits_to_bool(tcontrol[mte]), + _ => true + } + } + /* First solution of reentrancy problem */ + else { + match cur_privilege { + Machine => bits_to_bool(mstatus[MIE]), + Supervisor => if (medeleg[Breakpoint] == 0b1) then { bits_to_bool(mstatus[SIE]) } else { true }, + _ => true + } + } +} + +/* Instruction Count Trigger Match */ +function icount_trigger_match(cur_priv : Privilege) -> unit = { + /* Traverse through all the triggers */ + foreach (i from 0 to (sizeof(N_TRIGGERS) - 1)) { + let trigger_type : bits(4) = tdata1_x.tdata1[i][(xlen - 1) .. (xlen - 4)]; + /* If Instruction Count trigger is found */ + if (trigger_type == triggerType_to_bits(TRIG_ICOUNT)) then { + var InstrCount : InstructionCount = Mk_InstructionCount(tdata1_x.tdata1[i][26 .. 0]); + /* Check that trigger matches */ + if ((((InstrCount[m] == 0b1) & (cur_priv == Machine)) | /* Trigger is enabled in M-mode */ + ((InstrCount[s] == 0b1) & (cur_priv == Supervisor)) | /* Trigger is enabled in S-mode */ + ((InstrCount[u] == 0b1) & (cur_priv == User)) ) & /* Trigger is enabled in U-mode */ + (InstrCount[count] != zero_extend(14, 0b0)) & + (TriggerFireMatch(cur_priv))) then { /* Trigger Match valid? check re-enterancy */ + /* Decrement the counter */ + if (InstrCount[count] == zero_extend(14, 0b1)) then { + InstrCount[pending] = 0b1; + }; + InstrCount[count] = InstrCount[count] - 1; + tdata1_x.tdata1[i][26 .. 0] = InstrCount.bits; + } + } + } +} + +/* Interrupt/Exception Trigger */ +function IEtrigger_match(cur_priv : Privilege, idx : {'n, (0 <= 'n < xlen). int('n)}, is_exce : bool) -> unit = { + /* Traverse through all the triggers */ + foreach (i from 0 to (sizeof(N_TRIGGERS) - 1)) { + let trigger_type : bits(4) = tdata1_x.tdata1[i][(xlen - 1) .. (xlen - 4)]; + /* If Interrupt / Exception trigger found */ + if (((trigger_type == triggerType_to_bits(TRIG_ETRIGGER)) & is_exce) | + ((trigger_type == triggerType_to_bits(TRIG_ITRIGGER)) & not(is_exce))) then { + var IEtrigger : InterruptTrigger = Mk_InterruptTrigger(tdata1_x.tdata1[i]); + if ((((IEtrigger[m] == 0b1) & (cur_priv == Machine)) | /* Trigger is enabled in M-mode */ + ((IEtrigger[s] == 0b1) & (cur_priv == Supervisor)) | /* Trigger is enabled in S-mode */ + ((IEtrigger[u] == 0b1) & (cur_priv == User)) ) & /* Trigger is enabled in U-mode */ + (bit_to_bool(tdata2_x.tdata2[i][idx])) & + (TriggerFireMatch(cur_priv))) then { /* Trigger match valid? check re-enterancy */ + IEtrigger[hit] = 0b1; + tdata1_x.tdata1[i] = IEtrigger.bits; + } + } + } +} + /* handle exceptional ctl flow by updating nextPC and operating privilege */ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception)) @@ -307,6 +377,8 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen mstatus[MPIE] = mstatus[MIE]; mstatus[MIE] = 0b0; mstatus[MPP] = privLevel_to_bits(cur_privilege); + tcontrol[mpte] = tcontrol[mte]; + tcontrol[mte] = 0b0; mtval = tval(info); mepc = pc; @@ -356,12 +428,14 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if get_config_print_platform() then print_platform("trapping from " ^ to_str(cur_priv) ^ " to " ^ to_str(del_priv) ^ " to handle " ^ to_str(e.trap)); + IEtrigger_match(cur_priv, num_of_ExceptionType(e.trap), true); trap_handler(del_priv, false, exceptionType_to_bits(e.trap), pc, e.excinfo, e.ext) }, (_, CTL_MRET()) => { let prev_priv = cur_privilege; mstatus[MIE] = mstatus[MPIE]; mstatus[MPIE] = 0b1; + tcontrol[mte] = tcontrol[mpte]; cur_privilege = privLevel_of_bits(mstatus[MPP]); mstatus[MPP] = privLevel_to_bits(if extensionEnabled(Ext_U) then User else Machine); if cur_privilege != Machine @@ -408,8 +482,194 @@ function handle_exception(e: ExceptionType) -> unit = { set_next_pc(exception_handler(cur_privilege, CTL_TRAP(t), PC)) } -function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = +function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = { + IEtrigger_match(cur_privilege, num_of_interruptType(i), false); set_next_pc(trap_handler(del_priv, true, interruptType_to_bits(i), PC, None(), None())) +} + +function find_first_zero(v: xlenbits) -> {'n, (0 <= 'n <= xlen). int('n)} = { + foreach (i from 0 to (xlen - 1)) { + if v[i .. i] == 0b0 then return i; + }; + return xlen; +} + +/* Match Control Type 6 Trigger Match */ +function instrDataMatch(cur_priv : Privilege, addr : xlenbits, data : xlenbits, match_size : matchSize, match_type : MatchType) -> bool = { + var raise_exception : bool = false; + let half_xlen = sizeof(half_xlen); + /* Traverse through all triggers */ + foreach (i from 0 to (sizeof(N_TRIGGERS) - 1)) { + let trigger_type : bits(4) = tdata1_x.tdata1[i][(xlen - 1) .. (xlen - 4)]; + var data_matched : bool = false; + var size_matched : bool = false; + /* Match Control Type 6 Trigger found */ + if (trigger_type == triggerType_to_bits(TRIG_MCONTROL6)) then { + var MCtrl6 : MatchControlType6 = Mk_MatchControlType6(tdata1_x.tdata1[i][26 .. 0]); + let matchOption : bits(4) = MCtrl6[match_opt]; + /* Decide content to match address/data based on select bit */ + let tdata2_content : xlenbits = match (MCtrl6[select]) { + 0b0 => { size_matched = true; addr }, + 0b1 => { + size_matched = match matchSize_of_bits(MCtrl6[size]) { + ANY => true, + _ => (match_size == matchSize_of_bits(MCtrl6[size])), + }; + data + } + }; + /* Data matched according to the select match options */ + data_matched = match (matchOpt_of_bits(matchOption)) { + MOPT_EQUAL => { (tdata2_x.tdata2[i] == tdata2_content) }, + MOPT_NAPOT => { + let idx : {'n, (0 <= 'n <= xlen). int('n)} = find_first_zero(tdata2_x.tdata2[i]); + if ((idx == xlen) | (idx == (xlen - 1))) then { true } + else { + tdata2_x.tdata2[i][(xlen - 1) .. (idx + 1)] == tdata2_content[(xlen - 1) .. (idx + 1)] + } + }, + MOPT_GE => { (tdata2_content >=_u tdata2_x.tdata2[i][(xlen - 1) .. 0]) }, + MOPT_LT => { (tdata2_content <_u tdata2_x.tdata2[i][(xlen - 1) .. 0]) }, + MOPT_MASK_LOW => { + let intemrd_cmpr_val : half_xlenbits = tdata2_content[(half_xlen - 1) .. 0] & tdata2_x.tdata2[i][(xlen - 1) .. half_xlen]; + intemrd_cmpr_val == tdata2_x.tdata2[i][(half_xlen - 1) .. 0] + }, + MOPT_MASK_HIGH => { + let intemrd_cmpr_val : half_xlenbits = tdata2_content[(xlen - 1) .. half_xlen] & tdata2_x.tdata2[i][(xlen - 1) .. half_xlen]; + intemrd_cmpr_val == tdata2_x.tdata2[i][(half_xlen - 1) .. 0] + }, + MOPT_NOT_EQUAL => { (tdata2_x.tdata2[i] != tdata2_content) }, + MOPT_NOT_NAPOT => { + let idx : {'n, (0 <= 'n <= xlen). int('n)} = find_first_zero(tdata2_x.tdata2[i]); + if ((idx == xlen) | (idx == (xlen - 1))) then { true } + else { + tdata2_x.tdata2[i][(xlen - 1) .. (idx + 1)] != tdata2_content[(xlen - 1) .. (idx + 1)] + } + }, + MOPT_NOT_MASK_LOW => { + let intemrd_cmpr_val : half_xlenbits = tdata2_content[(half_xlen - 1) .. 0] & tdata2_x.tdata2[i][(xlen - 1) .. half_xlen]; + intemrd_cmpr_val != tdata2_x.tdata2[i][(half_xlen - 1) .. 0] + }, + MOPT_NOT_MASK_HIGH => { + let intemrd_cmpr_val : half_xlenbits = tdata2_content[(xlen - 1) .. half_xlen] & tdata2_x.tdata2[i][(xlen - 1) .. half_xlen]; + intemrd_cmpr_val != tdata2_x.tdata2[i][(half_xlen - 1) .. 0] + }, + _ => false + }; + if ((((MCtrl6[m] == 0b1) & (cur_priv == Machine)) | /* Trigger is enabled in M-mode */ + ((MCtrl6[s] == 0b1) & (cur_priv == Supervisor)) | /* Trigger is enabled in S-mode */ + ((MCtrl6[u] == 0b1) & (cur_priv == User)) ) & /* Trigger is enabled in U-mode */ + (TriggerFireMatch(cur_priv))) then { /* Trigger match valid? check reentranacy */ + match match_type { + /* Check For PC or Instruction Match */ + INSTR_MATCH => { + if (data_matched & size_matched & (MCtrl6[execute] == 0b1)) then { + MCtrl6[hit0] = 0b1; + tdata1_x.tdata1[i][26 .. 0] = MCtrl6.bits; + raise_exception = true; + } + }, + /* Check for Load Address match */ + LOAD_MATCH_BEFORE => { + if (data_matched & size_matched & (MCtrl6[load] == 0b1)) then { + MCtrl6[hit0] = 0b1; + tdata1_x.tdata1[i][26 .. 0] = MCtrl6.bits; + raise_exception = true; + } + }, + /* Check for load data match */ + LOAD_MATCH_AFTER => { + if (data_matched & size_matched & (MCtrl6[load] == 0b1)) then { + MCtrl6[hit1] = 0b1; + MCtrl6[hit0] = 0b1; + tdata1_x.tdata1[i][26 .. 0] = MCtrl6.bits; + } + }, + /* Check for store address and data match */ + STORE_MATCH => { + if (data_matched & size_matched & (MCtrl6[store] == 0b1)) then { + MCtrl6[hit0] = 0b1; + tdata1_x.tdata1[i][26 .. 0] = MCtrl6.bits; + raise_exception = true; + } + }, + }; + + } + } + }; + if (raise_exception) then { + handle_mem_exception(zero_extend(addr), E_Breakpoint()); + }; + raise_exception +} + +/* Check for Etrigger, Icount, Itrigger and Mcontrol6 After, Trigger Firing */ +function check_trigger_firing(cur_priv : Privilege) -> bool = { + var trigger_fire_match : bool = false; + var icountTrigFired : bool = false; + var ITrigFired : bool = false; + var ETrigFired : bool = false; + var MCtrlTrigFired : bool = false; + var fired_trigger_idx : vector(2, dec, {'n, (0 <= 'n < N_TRIGGERS). int('n)}) = [0, 0]; + var InstrCount : InstructionCount = Mk_InstructionCount(zero_extend(0b0)); + var IEtrigger : InterruptTrigger = Mk_InterruptTrigger(zero_extend(0b0)); + var MCtrl6 : MatchControlType6 = Mk_MatchControlType6(zero_extend(0b0)); + /* Traverse through each trigger */ + foreach (i from 0 to (sizeof(N_TRIGGERS) - 1)) + { + InstrCount = Mk_InstructionCount(tdata1_x.tdata1[i][26 .. 0]); + IEtrigger = Mk_InterruptTrigger(tdata1_x.tdata1[i]); + MCtrl6 = Mk_MatchControlType6(tdata1_x.tdata1[i][26 .. 0]); + let trigger_type : bits(4) = tdata1_x.tdata1[i][(xlen - 1) .. (xlen - 4)]; + match triggerType_of_bits(trigger_type) { + /* Check Exception Trigger Firing */ + TRIG_ETRIGGER => { + if ((IEtrigger[hit] == 0b1) & (TriggerFireMatch(cur_priv)) & not(ETrigFired)) then { + ETrigFired = true; + } + }, + /* Check instruction count trigger firing */ + TRIG_ICOUNT => { + if ((InstrCount[pending] == 0b1) & TriggerFireMatch(cur_priv) & not(icountTrigFired)) then { + InstrCount[pending] = 0b0; + tdata1_x.tdata1[i][26 .. 0] = InstrCount.bits; + icountTrigFired = true; + fired_trigger_idx[0] = i; + } + }, + /* Check interrupt trigger firing */ + TRIG_ITRIGGER => { + if ((IEtrigger[hit] == 0b1) & (TriggerFireMatch(cur_priv)) & not(ITrigFired)) then { + ITrigFired = true; + } + }, + /* Check Match Control 6 After Trigger Firing */ + TRIG_MCONTROL6 => { + if ((MCtrl6[hit1] == 0b1) & TriggerFireMatch(cur_priv) & not(MCtrlTrigFired)) then { + MCtrlTrigFired = true; + fired_trigger_idx[1] = i; + } + }, + _ => () + } + }; + if (ETrigFired | icountTrigFired | ITrigFired | MCtrlTrigFired) then { + trigger_fire_match = true; + handle_mem_exception(zero_extend(0b0), E_Breakpoint()); + }; + if (icountTrigFired) then { + InstrCount = Mk_InstructionCount(tdata1_x.tdata1[fired_trigger_idx[0]][26 .. 0]); + InstrCount[hit] = 0b1; + tdata1_x.tdata1[fired_trigger_idx[0]][26 .. 0] = InstrCount.bits; + } else if (ETrigFired | ITrigFired) then { + MCtrl6 = Mk_MatchControlType6(tdata1_x.tdata1[fired_trigger_idx[1]][26 .. 0]); + MCtrl6[hit1] = 0b0; + MCtrl6[hit0] = 0b0; + tdata1_x.tdata1[fired_trigger_idx[1]][26 .. 0] = MCtrl6.bits; + }; + ETrigFired | icountTrigFired | ITrigFired | MCtrlTrigFired +} /* state state initialization */ @@ -485,6 +745,10 @@ function init_sys() -> unit = { vtype[vsew] = 0b000; vtype[vlmul] = 0b000; + foreach (i from 0 to (sizeof(N_TRIGGERS) - 1)) { + tdata1_x.tdata1[i][(xlen - 1) .. (xlen - 4)] = 0xf; + }; + // PMP's L and A fields are set to 0 on reset. init_pmp(); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 8bbf68e75..bf1e4e7cd 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -116,6 +116,8 @@ val sys_enable_bext = pure "sys_enable_bext" : unit -> bool val sys_enable_zicbom = pure "sys_enable_zicbom" : unit -> bool val sys_enable_zicboz = pure "sys_enable_zicboz" : unit -> bool +val sys_reent_opt1 = pure {c: "sys_reent_opt1", ocaml: "Platform.reent_opt1", _: "sys_reent_opt1"} : unit -> bool + /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on unsetting C. If it returns true the write will have no effect. */ @@ -360,7 +362,11 @@ register medeleg : Medeleg /* Delegation to S-mode */ function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = { /* M-EnvCalls delegation is not supported */ - [Mk_Medeleg(v) with MEnvCall = 0b0] + let m = Mk_Medeleg(v); + let m = [m with MEnvCall = 0b0]; + /* medeleg[3] <-> Breakpoint Exception is hard-wired to 0 for second solution + of reentrancy problem */ + if (sys_reent_opt1()) then { let m = [m with Breakpoint = bool_bits(not(sys_reent_opt1()))]; m } else { m } } /* registers for trap handling */ @@ -685,6 +691,268 @@ function legalize_satp32(a : Architecture, o : bits(32), v : bits(32)) -> bits(3 /* disabled trigger/debug module */ register tselect : xlenbits +/* Legalize TSELECT */ +function legalize_tselect(o : xlenbits, v : xlenbits) -> xlenbits = { + let t : xlenbits = o; + if (unsigned(v) <= (sizeof(N_TRIGGERS) - 1)) then { v } else { t } +} + +struct N_TDATA1 = { + tdata1 : vector(N_TRIGGERS, xlenbits) +} + +struct N_TDATA2 = { + tdata2 : vector(N_TRIGGERS, xlenbits) +} + +struct N_TDATA3 = { + tdata3 : vector(N_TRIGGERS, xlenbits) +} + +register tdata1_x : N_TDATA1 = undefined + +register tdata2_x : N_TDATA2 = undefined + +register tdata3_x : N_TDATA3 = undefined + +register tdata1 : xlenbits = undefined + +register tdata2 : xlenbits + +register tdata3 : xlenbits + +/* Match Control Type 6 Trigger Bit fields */ +bitfield MatchControlType6 : bits(27) = { + /* Trigger perfectly satisfied or not */ + uncertain : 26, + /* This field combine with hit0 */ + hit1 : 25, + /* Enable Mcontrol6 trigger in VS-mode */ + vs : 24, + /* Enable Mcontrol6 trigger in VU-mode */ + vu : 23, + /* 0: Trigger did not fire + * 1: Trigger fired before the instruction retires + * 2: Trigger fired after the instruction that + * triggered and at least one additional instruction were + * retired. + * 3: Trigger fired just after the instruction that + * triggered it was retired, but before any subsequent + * instructions were executed */ + hit0 : 22, + /* 0: address match, 1: data match */ + select : 21, + /* Reserved bits */ + rsvd1 : 20 .. 19, + /* Access Size */ + size : 18 .. 16, + /* Trigger Action */ + action : 15 .. 12, + /* trigger chaining */ + chain : 11, + /* Trigger match options */ + match_opt : 10 .. 7, + /* Enable Mcontrol6 trigger in M-mode */ + m : 6, + /* Enable uncertain matches */ + uncertainen : 5, + /* Enable Mcontrol6 trigger in S-mode */ + s : 4, + /* Enable Mcontrol6 trigger in U-mode */ + u : 3, + /* Trigger fires on the virtual address or opcode + of an instruction that is executed */ + execute : 2, + /* Trigger fires on the virtual address or data of + any store */ + store : 1, + /* Trigger fires on the virtual address or data of + any load */ + load : 0 +} + +/* Instruction Count Trigger Bit fields */ +bitfield InstructionCount : bits(27) = { + /* Enable Instruction Count trigger in VS-mode */ + vs : 26, + /* Enable Instruction Count trigger in VU-mode */ + vu : 25, + /* Sets it when trigger fires */ + hit : 24, + /* Number of instructions to count */ + count : 23 .. 10, + /* Enable Instruction Count trigger in M-mode */ + m : 9, + /* Sets when count decremented from 1 to 0 */ + pending : 8, + /* Enable Instruction Count trigger in S-mode */ + s : 7, + /* Enable Instruction Count trigger in U-mode */ + u : 6, + /* Trigger Action */ + action : 5 .. 0 +} + +/* Interrupt/Exception Trigger Bit fields */ +bitfield InterruptTrigger : xlenbits = { + /* Sets it when this trigger matches */ + hit : xlen - 6, + /* Reserved bits */ + rsvd2 : xlen - 19, + /* Enable Exception/Interrupt trigger from VS-mode */ + vs : 12, + /* Enable Exception/Interrupt trigger from VU-mode */ + vu : 11, + /* Non-maskable interrupts cause the trigger to fire - Only for Itrigger*/ + nmi : 10, + /* Enable Exception/Interrupr trigger from M-mode */ + m : 9, + /* Reserved bits */ + rsvd1 : 8, + /* Enable Exception/Interrupr trigger from S-mode */ + s : 7, + /* Enable Exception/Interrupr trigger from U-mode */ + u : 6, + /* Trigger Action */ + action : 5 .. 0 +} + +/* Legalize Tdata1 */ +function legalize_tdata1(o : xlenbits, v : xlenbits) -> xlenbits = { + let trigger_type : bits(4) = v[(xlen - 1) .. (xlen - 4)]; + let trigger_dmode : bits(1) = v[(xlen - 5) .. (xlen - 5)]; + /* TODO: Update trigger action when remaining trigger action option will add */ + let trigger_action : bits(6) = (0b00 @ 0x0); + let MCtrl6 : MatchControlType6 = Mk_MatchControlType6(v[26 .. 0]); + let InstrCount : InstructionCount = Mk_InstructionCount(v[26 .. 0]); + let IntrptTrigger : InterruptTrigger = Mk_InterruptTrigger(v); + let ExcepTrigger : InterruptTrigger = Mk_InterruptTrigger(v); + var new_value : xlenbits = o; + + new_value[(xlen - 1) .. (xlen - 4)] = trigger_type; + new_value[(xlen - 5) .. (xlen - 5)] = trigger_dmode; + match triggerType_of_bits(trigger_type){ + TRIG_ICOUNT => { + /* Trigger action */ + new_value[5 .. 0] = trigger_action; + /* vs | vu | hit | count | m | pending | s | u */ + new_value[24 .. 6] = InstrCount.bits[24 .. 6]; + new_value + }, + TRIG_ITRIGGER => { + /* Trigger action */ + new_value[5 .. 0] = trigger_action; + /* s | u */ + new_value[7 .. 6] = (IntrptTrigger[s] @ IntrptTrigger[u]); + /* nmi | m */ + new_value[10 .. 9] = (IntrptTrigger[nmi] @ IntrptTrigger[m]); + /* hit */ + new_value[(xlen - 6) .. (xlen - 6)] = IntrptTrigger[hit]; + new_value + }, + TRIG_ETRIGGER => { + /* trigger action */ + new_value[5 .. 0] = trigger_action; + /* s | u */ + new_value[7 .. 6] = (IntrptTrigger[s] @ IntrptTrigger[u]); + /* m */ + new_value[9 .. 9] = IntrptTrigger[m]; + /* hit */ + new_value[(xlen - 6) .. (xlen - 6)] = IntrptTrigger[hit]; + new_value + }, + TRIG_MCONTROL6 => { + let match_option : MATCH_OPTIONS = matchOpt_of_bits(v[10 .. 7]); + /* m | uncertainen | s | u | execute | store | load */ + new_value[6 .. 0] = MCtrl6.bits[6 .. 0]; + /* match */ + new_value[10 .. 7] = match matchOpt_of_bits(v[10 .. 7]) { RSVD => { o[10 .. 7]}, _ => { v[10 .. 7] } }; + /* size | action | chain */ + new_value[18 .. 11] = (MCtrl6[size] @ trigger_action[3 .. 0] @ MCtrl6[chain]); + /* hit0 | select */ + new_value[22 .. 21] = (MCtrl6[hit0] @ MCtrl6[select]); + /* uncertain | hit1 */ + new_value[26 .. 25] = (MCtrl6[uncertain] @ MCtrl6[hit1]); + new_value + }, + TRIG_DISABLED => {v}, + _ => { new_value = o; new_value } + } + +} + +/* Write tdata1 of current trigger */ +function tdata1_write(tselect_val : xlenbits, o : xlenbits, new_value : xlenbits) -> xlenbits = { + let index : int = unsigned(tselect[2 .. 0]); + let v : xlenbits = legalize_tdata1(o, new_value); + if ((index >= 0) & (index < vector_length(tdata1_x.tdata1))) then + { tdata1_x.tdata1[index] = v; v } else { o } +} + +/* Read tdata1 of current trigger */ +function tdata1_read(tselect_val : xlenbits) -> xlenbits = { + let index : int = unsigned(tselect[2 .. 0]); + if ((index >= 0) & (index < vector_length(tdata1_x.tdata1))) then + { tdata1_x.tdata1[index]; } else { zero_extend(0b0); } +} + +/* Write tdata2 of current trigger */ +function tdata2_write(tselect_val : xlenbits, o : xlenbits, v : xlenbits) -> xlenbits = { + let index : int = unsigned(tselect[2 .. 0]); + if ((index >= 0) & (index < vector_length(tdata2_x.tdata2))) then + { tdata2_x.tdata2[index] = v; v } else { o } +} + +/* Read TData2 of current trigger */ +function tdata2_read(tselect_val : xlenbits) -> xlenbits = { + let index : int = unsigned(tselect[2 .. 0]); + if ((index >= 0) & (index < vector_length(tdata2_x.tdata2))) then + { tdata2_x.tdata2[index]; } else { zero_extend(0b0); } +} + +/* Write tdata3 of current trigger */ +function tdata3_write(tselect_val : xlenbits, o : xlenbits, v : xlenbits) -> xlenbits = { + let index : int = unsigned(tselect[2 .. 0]); + if ((index >= 0) & (index < vector_length(tdata3_x.tdata3))) then + { tdata3_x.tdata3[index] = v; v } else { o } +} + +/* Read TData3 of current trigger */ +function tdata3_read(tselect_val : xlenbits) -> xlenbits = { + let index : int = unsigned(tselect[2 .. 0]); + if ((index >= 0) & (index < vector_length(tdata3_x.tdata3))) then + { tdata3_x.tdata3[index]; } else { zero_extend(0b0); } +} + +register tinfo : xlenbits + +function tinfo_read(tselect_val : xlenbits) -> xlenbits = { + let tinfo_info : bits(16) = zero_extend( + (0x0001 << triggerType_to_bits(TRIG_ICOUNT)) | + (0x0001 << triggerType_to_bits(TRIG_ITRIGGER)) | + (0x0001 << triggerType_to_bits(TRIG_ETRIGGER)) | + (0x0001 << triggerType_to_bits(TRIG_MCONTROL6)) | + (0x0001 << triggerType_to_bits(TRIG_DISABLED)) + ); + let tinfo_version : bits(8) = zero_extend(0b1); + + zero_extend(tinfo_version @ 0x00 @ tinfo_info) +} + + +bitfield Tcontrol : xlenbits = { + mpte : 7, + rsvd2 : 6 .. 4, + mte : 3, + rsvd1 : 2 .. 0 +} + +function legalize_tcontrol(v : xlenbits) -> xlenbits = { + zero_extend(v[7 .. 7] @ 0b000 @ v[3 .. 3] @ 0b000) +} + +register tcontrol : Tcontrol + /* * The seed CSR (entropy source) * ------------------------------------------------------------ diff --git a/model/riscv_types.sail b/model/riscv_types.sail index c333c4e17..8c5dd2f9f 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -145,6 +145,40 @@ union AccessType ('a : Type) = { } enum word_width = {BYTE, HALF, WORD, DOUBLE} +enum matchSize = {ANY, BITS_8, BITS_16, BITS_32, BITS_48, BITS_64, BITS_128} + +mapping matchSize_of_wordWidth : word_width <-> matchSize = { + BYTE <-> BITS_8, + HALF <-> BITS_16, + WORD <-> BITS_32, + DOUBLE <-> BITS_48 +} + +mapping matchSize_of_bits : bits(3) <-> matchSize = { + 0b000 <-> ANY, + 0b001 <-> BITS_8, + 0b010 <-> BITS_16, + 0b011 <-> BITS_32, + 0b100 <-> BITS_48, + 0b101 <-> BITS_64, + 0b110 <-> BITS_128 +} + +mapping cacheBlockSize_to_matchSize : int <-> matchSize = { + 1 <-> ANY, + 3 <-> BITS_8, + 4 <-> BITS_16, + 5 <-> BITS_32, + 6 <-> BITS_64, + 7 <-> BITS_128 +} + +mapping vlenByteNum_to_matchSize : {1, 2, 4, 8} <-> matchSize = { + 1 <-> BITS_8, + 2 <-> BITS_16, + 4 <-> BITS_32, + 8 <-> BITS_64 +} /* architectural interrupt definitions */ @@ -174,6 +208,20 @@ function interruptType_to_bits (i) = I_M_External => 0x0b } +val num_of_interruptType : InterruptType -> {'n, (0 <= 'n < xlen). int('n)} +function num_of_interruptType (i) = + match (i) { + I_U_Software => 0, + I_S_Software => 1, + I_M_Software => 3, + I_U_Timer => 4, + I_S_Timer => 5, + I_M_Timer => 7, + I_U_External => 8, + I_S_External => 9, + I_M_External => 11 + } + /* architectural exception definitions */ union ExceptionType = { @@ -273,6 +321,89 @@ function exceptionType_to_str(e) = overload to_str = {exceptionType_to_str} +/* debug spec trigger type definition */ + +type N_TRIGGERS = 7 +let VALID_TRIGGER_TYPES : vector(5, dec, bits(4)) = [0x3, 0x4, 0x5, 0x6, 0xF] + +type match_option = bits(4) +enum MATCH_OPTIONS = { + MOPT_EQUAL, + MOPT_NAPOT, + MOPT_GE, + MOPT_LT, + MOPT_MASK_LOW, + MOPT_MASK_HIGH, + MOPT_NOT_EQUAL, + MOPT_NOT_NAPOT, + MOPT_NOT_MASK_LOW, + MOPT_NOT_MASK_HIGH, + RSVD +} + +mapping matchOpt_of_bits : bits(4) <-> MATCH_OPTIONS = { + 0x0 <-> MOPT_EQUAL, + 0x1 <-> MOPT_NAPOT, + 0x2 <-> MOPT_GE, + 0x3 <-> MOPT_LT, + 0x4 <-> MOPT_MASK_LOW, + 0x5 <-> MOPT_MASK_HIGH, + 0x6 <-> RSVD, + 0x7 <-> RSVD, + 0x8 <-> MOPT_NOT_EQUAL, + 0x9 <-> MOPT_NOT_NAPOT, + 0xA <-> RSVD, + 0xB <-> RSVD, + 0xC <-> MOPT_NOT_MASK_LOW, + 0xD <-> MOPT_NOT_MASK_HIGH, + 0xE <-> RSVD, + 0xF <-> RSVD, +} + +enum MatchType = { + INSTR_MATCH, + LOAD_MATCH_BEFORE, + LOAD_MATCH_AFTER, + STORE_MATCH +} + +type trig_code = bits(4) +enum TriggerType = { + TRIG_NONE, + TRIG_LEGACY, + TRIG_MCONTROL, + TRIG_ICOUNT, + TRIG_ITRIGGER, + TRIG_ETRIGGER, + TRIG_MCONTROL6, + TRIG_TMEXTTRIGGER, + TRIG_DISABLED +} + +mapping triggerType_to_bits : TriggerType <-> bits(4) = { + TRIG_NONE <-> 0x0, + TRIG_LEGACY <-> 0x1, + TRIG_MCONTROL <-> 0x2, + TRIG_ICOUNT <-> 0x3, + TRIG_ITRIGGER <-> 0x4, + TRIG_ETRIGGER <-> 0x5, + TRIG_MCONTROL6 <-> 0x6, + TRIG_TMEXTTRIGGER <-> 0x7, + TRIG_DISABLED <-> 0xF +} + +mapping triggerType_of_bits : bits(4) <-> TriggerType = { + 0x0 <-> TRIG_NONE, + 0x1 <-> TRIG_LEGACY, + 0x2 <-> TRIG_MCONTROL, + 0x3 <-> TRIG_ICOUNT, + 0x4 <-> TRIG_ITRIGGER, + 0x5 <-> TRIG_ETRIGGER, + 0x6 <-> TRIG_MCONTROL6, + 0x7 <-> TRIG_TMEXTTRIGGER, + 0xF <-> TRIG_DISABLED +} + /* trap modes */ type tv_mode = bits(2) diff --git a/model/riscv_xlen.sail b/model/riscv_xlen.sail index 8b0544352..5ac734cf4 100644 --- a/model/riscv_xlen.sail +++ b/model/riscv_xlen.sail @@ -10,6 +10,9 @@ type xlen_bytes : Int = 2 ^ log2_xlen_bytes type xlen : Int = xlen_bytes * 8 type xlenbits = bits(xlen) +type half_xlen_bytes : Int = 2 ^ (log2_xlen_bytes - 1) +type half_xlen : Int = half_xlen_bytes * 8 +type half_xlenbits = bits(half_xlen) // Variable versions of the above types. Variables and types // are disjoint in Sail so they are allowed to have the same name. // This saves typing `sizeof()` everywhere. diff --git a/sail-riscv.install b/sail-riscv.install index 7a539dfb5..9001de619 100644 --- a/sail-riscv.install +++ b/sail-riscv.install @@ -1,2 +1,2 @@ bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"] -share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ] +share: [ "model/hex_bits.sail" {"model/hex_bits.sail"} "model/hex_bits_signed.sail" {"model/hex_bits_signed.sail"} "model/main.sail" {"model/main.sail"} "model/mapping.sail" {"model/mapping.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_svinval.sail" {"model/riscv_insts_svinval.sail"} "model/riscv_insts_vext_arith.sail" {"model/riscv_insts_vext_arith.sail"} "model/riscv_insts_vext_fp.sail" {"model/riscv_insts_vext_fp.sail"} "model/riscv_insts_vext_fp_red.sail" {"model/riscv_insts_vext_fp_red.sail"} "model/riscv_insts_vext_fp_utils.sail" {"model/riscv_insts_vext_fp_utils.sail"} "model/riscv_insts_vext_fp_vm.sail" {"model/riscv_insts_vext_fp_vm.sail"} "model/riscv_insts_vext_mask.sail" {"model/riscv_insts_vext_mask.sail"} "model/riscv_insts_vext_mem.sail" {"model/riscv_insts_vext_mem.sail"} "model/riscv_insts_vext_red.sail" {"model/riscv_insts_vext_red.sail"} "model/riscv_insts_vext_utils.sail" {"model/riscv_insts_vext_utils.sail"} "model/riscv_insts_vext_vm.sail" {"model/riscv_insts_vext_vm.sail"} "model/riscv_insts_vext_vset.sail" {"model/riscv_insts_vext_vset.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zca.sail" {"model/riscv_insts_zca.sail"} "model/riscv_insts_zcb.sail" {"model/riscv_insts_zcb.sail"} "model/riscv_insts_zcd.sail" {"model/riscv_insts_zcd.sail"} "model/riscv_insts_zcf.sail" {"model/riscv_insts_zcf.sail"} "model/riscv_insts_zfa.sail" {"model/riscv_insts_zfa.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicbom.sail" {"model/riscv_insts_zicbom.sail"} "model/riscv_insts_zicboz.sail" {"model/riscv_insts_zicboz.sail"} "model/riscv_insts_zicond.sail" {"model/riscv_insts_zicond.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vext_control.sail" {"model/riscv_vext_control.sail"} "model/riscv_vext_regs.sail" {"model/riscv_vext_regs.sail"} "model/riscv_vlen.sail" {"model/riscv_vlen.sail"} "model/riscv_vmem.sail" {"model/riscv_vmem.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_pte.sail" {"model/riscv_vmem_pte.sail"} "model/riscv_vmem_ptw.sail" {"model/riscv_vmem_ptw.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_vreg_type.sail" {"model/riscv_vreg_type.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]