Skip to content

Commit

Permalink
add svnapot and svpbmt
Browse files Browse the repository at this point in the history
  • Loading branch information
@ved-rivos
ved-rivos committed Jan 22, 2024
1 parent 0b60e2d commit 8f90f78
Show file tree
Hide file tree
Showing 10 changed files with 104 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 @@ -72,6 +72,16 @@ bool plat_enable_pmp(unit u)
return rv_enable_pmp;
}

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 @@ -8,6 +8,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);

bool plat_enable_dirty_update(unit);
bool plat_enable_misaligned_access(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 @@ -15,6 +15,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 @@ -19,6 +19,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 @@ -51,6 +51,8 @@ const char *RV32ISA = "RV32IMAC";

#define OPT_TRACE_OUTPUT 1000
#define OPT_ENABLE_WRITABLE_FIOM 1001
#define OPT_ENABLE_SVNAPOT 1002
#define OPT_ENABLE_SVPBMT 1003

static bool do_dump_dts = false;
static bool do_show_times = false;
Expand Down Expand Up @@ -145,6 +147,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 @@ -381,6 +385,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
55 changes: 36 additions & 19 deletions model/riscv_pte.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,14 +70,23 @@

/* PTE attributes, permission checks and updates */


/* Extension hooks can request standard PTE validity checks by returning Ext_PTE_Std
*/
union Ext_isInvalPTE_Check = {
Ext_PTE_Invalid : unit,
Ext_PTE_Valid : unit,
Ext_PTE_Std : unit
}

type pteAttribs = bits(8)

/* Reserved PTE bits could be used by extensions on RV64. There are
/* Reserved PTE bits could be used by standard extensions on RV64. There are
* no such available bits on RV32, so these bits will be zeros on RV32.
*/
type extPte = bits(10)
type pteStdExtAttribs = bits(10)

bitfield EXT_PTE_Bits : extPte = {
bitfield PTE_StdExt_Bits : pteStdExtAttribs = {
N : 9,
PBMT : 8 .. 7,
RSVD : 6 .. 0
Expand All @@ -90,9 +99,9 @@ bitfield EXT_PTE_Bits : extPte = {
* those PTEs. To avoid the need for "inhibit" bits in extensions (i.e., so
* that extensions can use the more common and more RISC-V flavored "enable"
* disposition), we allow extensions to use any constant value by overriding
* this default_sv32_ext_pte value.
* this default_sv32_pte_std_ext_attribs value.
*/
let default_sv32_ext_pte : extPte = zeros()
let default_sv32_pte_std_ext_attribs : pteStdExtAttribs = zeros()

bitfield PTE_Bits : pteAttribs = {
D : 7,
Expand All @@ -105,20 +114,29 @@ bitfield PTE_Bits : pteAttribs = {
V : 0
}

function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
function ext_isInvalidPTE (p : pteAttribs, std_ext : pteStdExtAttribs) -> Ext_isInvalPTE_Check =
Ext_PTE_Std()

function isPTEPtr(p : pteAttribs, std_ext : pteStdExtAttribs) -> bool = {
let a = Mk_PTE_Bits(p);
a.R() == 0b0 & a.W() == 0b0 & a.X() == 0b0
}

function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
function isInvalidPTE(p : pteAttribs, std_ext : pteStdExtAttribs) -> bool = {
let a = Mk_PTE_Bits(p);
let e = Mk_EXT_PTE_Bits(ext);
a.V() == 0b0 |
(a.W() == 0b1 & a.R() == 0b0) |
(e.RSVD() != 0b0000000 | e.PBMT() == 0b11) |
(not(isPTEPtr(p, ext)) & (e.N() != 0b0 ) & (not(haveSvnapot()))) |
(not(isPTEPtr(p, ext)) & (e.PBMT() != 0b00) & (not(haveSvpbmt()) | menvcfg.PBMTE() == 0b0)) |
(isPTEPtr(p, ext) & (a.D() == 0b1 | a.A() == 0b1 | a.U() == 0b1 | e.N() != 0b0 | e.PBMT() != 0b00))
let e = Mk_PTE_StdExt_Bits(std_ext);
match ext_isInvalidPTE (p , std_ext) {
Ext_PTE_Invalid() => true,
Ext_PTE_Valid() => false,
Ext_PTE_Std() => {
a.V() == 0b0 |
(a.W() == 0b1 & a.R() == 0b0) |
(e.RSVD() != 0b0000000 | e.PBMT() == 0b11) |
(not(isPTEPtr(p, std_ext)) & (e.N() != 0b0 ) & (not(haveSvnapot()))) |
(not(isPTEPtr(p, std_ext)) & (e.PBMT() != 0b00) & (not(haveSvpbmt()) | menvcfg.PBMTE() == 0b0)) |
(isPTEPtr(p, std_ext) & (a.D() == 0b1 | a.A() == 0b1 | a.U() == 0b1 | e.N() != 0b0 | e.PBMT() != 0b00))
}
}
}

union PTE_Check = {
Expand All @@ -129,11 +147,11 @@ union PTE_Check = {
function to_pte_check(b : bool) -> PTE_Check =
if b then PTE_Check_Success(()) else PTE_Check_Failure((), ())

/* For extensions: this function gets the extension-available bits of the PTE in extPte,
/* For extensions: this function gets the extension-available bits of the PTE in std_ext,
* and the accumulated information of the page-table-walk in ext_ptw. It should return
* the updated ext_ptw in both the success and failure cases.
*/
function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = {
function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, std_ext : pteStdExtAttribs, ext_ptw : ext_ptw) -> PTE_Check = {
match (ac, priv) {
(Read(_), User) => to_pte_check(p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1),
Expand All @@ -149,8 +167,7 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
}
}

function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = {
let update_d = p.D() == 0b0 & (match a { // dirty-bit
function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), std_ext : pteStdExtAttribs) -> option((PTE_Bits, pteStdExtAttribs)) = { let update_d = p.D() == 0b0 & (match a { // dirty-bit
Execute() => false,
Read() => false,
Write(_) => true,
Expand All @@ -161,6 +178,6 @@ function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : ex
if update_d | update_a then {
let np = update_A(p, 0b1);
let np = if update_d then update_D(np, 0b1) else np;
Some(np, ext)
Some(np, std_ext)
} else None()
}
10 changes: 8 additions & 2 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,6 +156,12 @@ val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.
/* 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 @@ -216,10 +222,10 @@ function haveZmmul() -> bool = true
function haveZicond() -> bool = true

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

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

bitfield Mstatush : bits(32) = {
MBE : 5,
Expand Down
14 changes: 7 additions & 7 deletions model/riscv_vmem_sv32.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,19 +94,19 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
MemValue(v) => {
let pte = Mk_SV32_PTE(v);
let pbits = pte.BITS();
let ext_pte : extPte = default_sv32_ext_pte;
let std_ext : pteStdExtAttribs = default_sv32_pte_std_ext_attribs;
let pattr = Mk_PTE_Bits(pbits);
let is_global = global | (pattr.G() == 0b1);
/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr))
^ " pte=" ^ BitStr(v)); */
if isInvalidPTE(pbits, ext_pte) then {
if isInvalidPTE(pbits, std_ext) then {
/* print("walk32: invalid pte"); */
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
if isPTEPtr(pbits, ext_pte) then {
if isPTEPtr(pbits, std_ext) then {
if level > 0 then {
/* walk down the pointer to the next level */
walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
Expand All @@ -116,7 +116,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
}
} else { /* leaf PTE */
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, std_ext, ext_ptw) {
PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
/* print("walk32: pte permission check failure"); */
PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
Expand Down Expand Up @@ -191,12 +191,12 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
Some(idx, ent) => {
/* print("translate32: TLB32 hit for " ^ BitStr(vAddr)); */
let pte = Mk_SV32_PTE(ent.pte);
let ext_pte : extPte = zeros(); // no reserved bits for extensions
let std_ext : pteStdExtAttribs = default_sv32_pte_std_ext_attribs;
let pteBits = Mk_PTE_Bits(pte.BITS());
match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) {
match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, std_ext, ext_ptw) {
PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) },
PTE_Check_Success(ext_ptw) => {
match update_PTE_Bits(pteBits, ac, ext_pte) {
match update_PTE_Bits(pteBits, ac, std_ext) {
None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw),
Some(pbits, ext) => {
if not(plat_enable_dirty_update())
Expand Down
27 changes: 14 additions & 13 deletions model/riscv_vmem_sv39.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,20 +88,20 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
MemValue(v) => {
let pte = Mk_SV39_PTE(v);
let pbits = pte.BITS();
let ext_pte = pte.Ext();
let std_ext = pte.Ext();
let pattr = Mk_PTE_Bits(pbits);
let eattr = Mk_EXT_PTE_Bits(ext_pte);
let eattr = Mk_PTE_StdExt_Bits(std_ext);
let is_global = global | (pattr.G() == 0b1);
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
^ " pt_ofs=" ^ BitStr(pt_ofs)
^ " pte_addr=" ^ BitStr(pte_addr)
^ " pte=" ^ BitStr(v)); */
if isInvalidPTE(pbits, ext_pte) then {
if isInvalidPTE(pbits, std_ext) then {
/* print("walk39: invalid pte"); */
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
if isPTEPtr(pbits, ext_pte) then {
if isPTEPtr(pbits, std_ext) then {
if level > 0 then {
/* walk down the pointer to the next level */
walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
Expand All @@ -111,7 +111,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
}
} else { /* leaf PTE */
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, std_ext, ext_ptw) {
PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
/* print("walk39: pte permission check failure"); */
PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
Expand All @@ -120,7 +120,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
if level > 0 then { /* superpage */
/* fixme hack: to get a mask of appropriate size */
let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1;
if eattr.N() == 0b1 then {
if haveSvnapot() & eattr.N() == 0b1 then {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else if (pte.PPNi() & mask) != zero_extend(0b0) then {
/* misaligned superpage mapping */
Expand All @@ -136,12 +136,13 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
}
} else {
/* normal leaf PTE */
if ( eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then {
if ( haveSvnapot() & eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
let ppn : bits(44) = match eattr.N() {
0b0 => pte.PPNi(),
0b1 => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0])
let ppn : bits(44) = match (haveSvnapot(), eattr.N()) {
(false, _) => pte.PPNi(),
(true, 0b0) => pte.PPNi(),
(true, 0b1) => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0])
};
/* let res = append(ppn, va.PgOfs());
print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
Expand Down Expand Up @@ -196,12 +197,12 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) =
Some(idx, ent) => {
/* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */
let pte = Mk_SV39_PTE(ent.pte);
let ext_pte = pte.Ext();
let std_ext = pte.Ext();
let pteBits = Mk_PTE_Bits(pte.BITS());
match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) {
match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, std_ext, ext_ptw) {
PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) },
PTE_Check_Success(ext_ptw) => {
match update_PTE_Bits(pteBits, ac, ext_pte) {
match update_PTE_Bits(pteBits, ac, std_ext) {
None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw),
Some(pbits, ext) => {
if not(plat_enable_dirty_update())
Expand Down
21 changes: 11 additions & 10 deletions model/riscv_vmem_sv48.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,20 +88,20 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
MemValue(v) => {
let pte = Mk_SV48_PTE(v);
let pbits = pte.BITS();
let ext_pte = pte.Ext();
let std_ext = pte.Ext();
let pattr = Mk_PTE_Bits(pbits);
let eattr = Mk_EXT_PTE_Bits(ext_pte);
let eattr = Mk_PTE_StdExt_Bits(std_ext);
let is_global = global | (pattr.G() == 0b1);
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
^ " pt_ofs=" ^ BitStr(pt_ofs)
^ " pte_addr=" ^ BitStr(pte_addr)
^ " pte=" ^ BitStr(v)); */
if isInvalidPTE(pbits, ext_pte) then {
if isInvalidPTE(pbits, std_ext) then {
/* print("walk48: invalid pte"); */
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
if isPTEPtr(pbits, ext_pte) then {
if isPTEPtr(pbits, std_ext) then {
if level > 0 then {
/* walk down the pointer to the next level */
walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
Expand All @@ -111,7 +111,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
}
} else { /* leaf PTE */
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
match checkPTEPermission(ac, priv, mxr, do_sum, pattr, std_ext, ext_ptw) {
PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
/* print("walk48: pte permission check failure"); */
PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
Expand All @@ -120,7 +120,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
if level > 0 then { /* superpage */
/* fixme hack: to get a mask of appropriate size */
let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1;
if eattr.N() == 0b1 then {
if haveSvnapot() & eattr.N() == 0b1 then {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else if (pte.PPNi() & mask) != zero_extend(0b0) then {
/* misaligned superpage mapping */
Expand All @@ -136,12 +136,13 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
}
} else {
/* normal leaf PTE */
if ( eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then {
if ( haveSvnapot() & eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
let ppn : bits(44) = match eattr.N() {
0b0 => pte.PPNi(),
0b1 => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0])
let ppn : bits(44) = match (haveSvnapot(), eattr.N()) {
(false, _) => pte.PPNi(),
(true, 0b0) => pte.PPNi(),
(true, 0b1) => append(pte.PPNi()[43 .. 4], va.VPNi()[3 .. 0])
};
/* let res = append(ppn, va.PgOfs());
print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
Expand Down

0 comments on commit 8f90f78

Please sign in to comment.