Skip to content

Commit

Permalink
Add Svnapot and Svpbmt extensions
Browse files Browse the repository at this point in the history
  • Loading branch information
@ved-rivos
ved-rivos committed Apr 21, 2024
1 parent 16077e1 commit 9919687
Show file tree
Hide file tree
Showing 16 changed files with 142 additions and 51 deletions.
10 changes: 10 additions & 0 deletions c_emulator/riscv_platform.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,16 @@ bool plat_mtval_has_illegal_inst_bits(unit u)
return rv_mtval_has_illegal_inst_bits;
}

bool sys_enable_svnapot(unit u)
{
return rv_enable_svnapot;
}

bool sys_enable_svpbmt(unit u)
{
return rv_enable_svpbmt;
}

mach_bits plat_ram_base(unit u)
{
return rv_ram_base;
Expand Down
2 changes: 2 additions & 0 deletions c_emulator/riscv_platform.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,8 @@ bool sys_enable_zfinx(unit);
bool sys_enable_writable_misa(unit);
bool sys_enable_writable_fiom(unit);
bool sys_enable_vext(unit);
bool sys_enable_svnapot(unit);
bool sys_enable_svpbmt(unit);

uint64_t sys_pmp_count(unit);
uint64_t sys_pmp_grain(unit);
Expand Down
2 changes: 2 additions & 0 deletions c_emulator/riscv_platform_impl.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ bool rv_enable_dirty_update = false;
bool rv_enable_misaligned = false;
bool rv_mtval_has_illegal_inst_bits = false;
bool rv_enable_writable_fiom = true;
bool rv_enable_svnapot = false;
bool rv_enable_svpbmt = false;

uint64_t rv_ram_base = UINT64_C(0x80000000);
uint64_t rv_ram_size = UINT64_C(0x4000000);
Expand Down
2 changes: 2 additions & 0 deletions c_emulator/riscv_platform_impl.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ extern bool rv_enable_dirty_update;
extern bool rv_enable_misaligned;
extern bool rv_mtval_has_illegal_inst_bits;
extern bool rv_enable_writable_fiom;
extern bool rv_enable_svnapot;
extern bool rv_enable_svpbmt;

extern uint64_t rv_ram_base;
extern uint64_t rv_ram_size;
Expand Down
12 changes: 12 additions & 0 deletions c_emulator/riscv_sim.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,8 @@ const char *RV32ISA = "RV32IMAC";
#define OPT_ENABLE_WRITABLE_FIOM 1001
#define OPT_PMP_COUNT 1002
#define OPT_PMP_GRAIN 1003
#define OPT_ENABLE_SVNAPOT 1004
#define OPT_ENABLE_SVPBMT 1005
#define OPT_ENABLE_ZCB 10014

static bool do_dump_dts = false;
Expand Down Expand Up @@ -150,6 +152,8 @@ static struct option options[] = {
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c' },
#endif
{"enable-svnapot", no_argument, 0, OPT_ENABLE_SVNAPOT },
{"enable-svpbmt", no_argument, 0, OPT_ENABLE_SVPBMT },
{0, 0, 0, 0 }
};

Expand Down Expand Up @@ -406,6 +410,14 @@ static int process_args(int argc, char **argv)
trace_log_path = optarg;
fprintf(stderr, "using %s for trace output.\n", trace_log_path);
break;
case OPT_ENABLE_SVNAPOT:
fprintf(stderr, "enabling Svnapot extension.\n");
rv_enable_svnapot = true;
break;
case OPT_ENABLE_SVPBMT:
fprintf(stderr, "enabling Svpbmt extension.\n");
rv_enable_svpbmt = true;
break;
case '?':
print_usage(argv[0], 1);
break;
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_fetch.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ function fetch() -> FetchResult =
then F_Error(E_Fetch_Addr_Align(), PC)
else match translateAddr(use_pc, Execute()) {
TR_Failure(e, _) => F_Error(e, PC),
TR_Address(ppclo, _) => {
TR_Address(ppclo, _, _) => {
/* split instruction fetch into 16-bit granules to handle RVC, as
* well as to generate precise fault addresses in any fetch
* exceptions.
Expand All @@ -42,7 +42,7 @@ function fetch() -> FetchResult =
Ext_FetchAddr_OK(use_pc_hi) => {
match translateAddr(use_pc_hi, Execute()) {
TR_Failure(e, _) => F_Error(e, PC_hi),
TR_Address(ppchi, _) => {
TR_Address(ppchi, _, _) => {
match mem_read(Execute(), ppchi, 2, false, false, false) {
MemException(e) => F_Error(e, PC_hi),
MemValue(ihi) => F_Base(append(ihi, ilo))
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_fetch_rvfi.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ function fetch() -> FetchResult = {
then F_Error(E_Fetch_Addr_Align(), PC)
else match translateAddr(use_pc, Execute()) {
TR_Failure(e, _) => F_Error(e, PC),
TR_Address(_, _) => {
TR_Address(_, _, _) => {
let i = rvfi_instruction[rvfi_insn];
rvfi_inst_data->rvfi_insn() = zero_extend(i);
if (i[1 .. 0] != 0b11)
Expand All @@ -34,7 +34,7 @@ function fetch() -> FetchResult = {
Ext_FetchAddr_OK(use_pc_hi) =>
match translateAddr(use_pc_hi, Execute()) {
TR_Failure(e, _) => F_Error(e, PC),
TR_Address(_, _) => F_Base(i)
TR_Address(_, _, _) => F_Base(i)
}
}
}
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
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, _) =>
TR_Address(addr, _, _) =>
match (width, sizeof(xlen)) {
(BYTE, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 1, aq, aq & rl, true), false),
(HALF, _) => process_loadres(rd, vaddr, mem_read(Read(Data), addr, 2, aq, aq & rl, true), false),
Expand Down Expand Up @@ -149,7 +149,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
* both result in a SAMO exception */
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
TR_Address(addr, _, _) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true),
(HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true),
Expand Down Expand Up @@ -221,7 +221,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
Ext_DataAddr_OK(vaddr) => {
match translateAddr(vaddr, ReadWrite(Data, Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
TR_Address(addr, _, _) => {
let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) {
(BYTE, _) => mem_write_ea(addr, 1, aq & rl, rl, true),
(HALF, _) => mem_write_ea(addr, 2, aq & rl, rl, true),
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -333,7 +333,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
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, _) =>
TR_Address(paddr, _, _) =>
match (width) {
BYTE =>
process_load(rd, vaddr, mem_read(Read(Data), paddr, 1, aq, rl, false), is_unsigned),
Expand Down Expand Up @@ -389,7 +389,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
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 },
TR_Address(paddr, _) => {
TR_Address(paddr, _, _) => {
let eares : MemoryOpResult(unit) = match width {
BYTE => mem_write_ea(paddr, 1, aq, rl, false),
HALF => mem_write_ea(paddr, 2, aq, rl, false),
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -322,7 +322,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, 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, _) => {
TR_Address(addr, _, _) => {
let (aq, rl, res) = (false, false, false);
match (width) {
BYTE => { handle_illegal(); RETIRE_FAIL },
Expand Down Expand Up @@ -388,7 +388,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, 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 },
TR_Address(addr, _) => {
TR_Address(addr, _, _) => {
let eares : MemoryOpResult(unit) = match width {
BYTE => MemValue () /* bogus placeholder for illegal size */,
HALF => mem_write_ea(addr, 2, aq, rl, false),
Expand Down
26 changes: 13 additions & 13 deletions model/riscv_insts_vext_mem.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) =
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, _) => {
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),
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
Expand Down Expand Up @@ -175,7 +175,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
trimmed = true
}
},
TR_Address(paddr, _) => {
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),
MemException(e) => {
Expand Down Expand Up @@ -258,7 +258,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem)
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 },
TR_Address(paddr, _) => {
TR_Address(paddr, _, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
Expand Down Expand Up @@ -329,7 +329,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e
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, _) => {
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),
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
Expand Down Expand Up @@ -395,7 +395,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_
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 },
TR_Address(paddr, _) => {
TR_Address(paddr, _, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
Expand Down Expand Up @@ -467,7 +467,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index
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, _) => {
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),
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
Expand Down Expand Up @@ -558,7 +558,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde
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 },
TR_Address(paddr, _) => {
TR_Address(paddr, _, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, EEW_data_bytes, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
Expand Down Expand Up @@ -651,7 +651,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
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, _) => {
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),
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
Expand All @@ -675,7 +675,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
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, _) => {
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), elem),
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
Expand Down Expand Up @@ -733,7 +733,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
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 },
TR_Address(paddr, _) => {
TR_Address(paddr, _, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
Expand Down Expand Up @@ -767,7 +767,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
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 },
TR_Address(paddr, _) => {
TR_Address(paddr, _, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, load_width_bytes, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
Expand Down Expand Up @@ -835,7 +835,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
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, _) => {
TR_Address(paddr, _, _) => {
match mem_read(Read(Data), paddr, 1, false, false, false) {
MemValue(elem) => write_single_element(8, i, vd_or_vs3, elem),
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
Expand All @@ -851,7 +851,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
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 },
TR_Address(paddr, _) => {
TR_Address(paddr, _, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL },
Expand Down
13 changes: 13 additions & 0 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,12 @@ val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pm
/* whether misa.v was enabled at boot */
val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool

/* whether svnapot was enabled at boot */
val sys_enable_svnapot = {c: "sys_enable_svnapot", ocaml: "Platform.enable_svnapot", _: "sys_enable_svnapot"} : unit -> bool
/* whether svpbmt was enabled at boot */
val sys_enable_svpbmt = {c: "sys_enable_svpbmt", ocaml: "Platform.enable_svpbmt", _: "sys_enable_svpbmt"} : 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. */
Expand Down Expand Up @@ -162,6 +168,12 @@ function haveZmmul() -> bool = true
/* Zicond extension support */
function haveZicond() -> bool = true

/* Svpbmt extension support */
function haveSvpbmt() -> bool = sys_enable_svpbmt()

/* Svnapot extension support */
function haveSvnapot() -> bool = sys_enable_svnapot()

bitfield Mstatush : bits(32) = {
MBE : 5,
SBE : 4
Expand Down Expand Up @@ -809,6 +821,7 @@ register senvcfg : SEnvcfg
function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = {
let v = Mk_MEnvcfg(v);
let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
let o = [o with PBMTE = if haveSvpbmt() then v[PBMTE] else 0b0];
// Other extensions are not implemented yet so all other fields are read only zero.
o
}
Expand Down
Loading

0 comments on commit 9919687

Please sign in to comment.