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 Jul 6, 2024
1 parent 4ab15c0 commit 75d7b42
Show file tree
Hide file tree
Showing 16 changed files with 142 additions and 55 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 @@ -92,6 +92,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 @@ -11,6 +11,8 @@ bool sys_enable_writable_misa(unit);
bool sys_enable_writable_fiom(unit);
bool sys_enable_vext(unit);
bool sys_enable_bext(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 @@ -20,6 +20,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 @@ -24,6 +24,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 @@ -56,6 +56,8 @@ enum {
OPT_PMP_GRAIN,
OPT_ENABLE_SVINVAL,
OPT_ENABLE_ZCB,
OPT_ENABLE_SVNAPOT,
OPT_ENABLE_SVPBMT,
};

static bool do_dump_dts = false;
Expand Down Expand Up @@ -154,6 +156,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 @@ -415,6 +419,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 @@ -23,7 +23,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 @@ -41,7 +41,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
8 changes: 4 additions & 4 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,11 +72,11 @@ 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 mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
MemValue(result) => { load_reservation(vaddr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
},
}
}
}
}
Expand Down Expand Up @@ -123,7 +123,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 = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
Expand Down Expand Up @@ -184,7 +184,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else match translateAddr(vaddr, ReadWrite(Data, Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
TR_Address(addr, _, _) => {
let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
match (eares) {
Expand Down
9 changes: 4 additions & 5 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -331,14 +331,13 @@ 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 mem_read(Read(Data), paddr, width_bytes, aq, rl, false) {
MemValue(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
},
}
}
},
}
}
}

Expand Down Expand Up @@ -387,7 +386,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 = mem_write_ea(paddr, width_bytes, aq, rl, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
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
17 changes: 16 additions & 1 deletion model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,12 @@ val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "
/* whether misa.b was enabled at boot */
val sys_enable_bext = {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : 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 @@ -172,6 +178,12 @@ function haveZalrsc() -> bool = haveAtomics()
/* 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()

/*
* Illegal values legalized to least privileged mode supported.
* Note: the only valid combinations of supported modes are M, M+U, M+S+U.
Expand Down Expand Up @@ -840,7 +852,10 @@ 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
FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0,
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 75d7b42

Please sign in to comment.