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 Jan 22, 2024
1 parent d7a3d80 commit 19ca9db
Show file tree
Hide file tree
Showing 11 changed files with 145 additions and 43 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
8 changes: 4 additions & 4 deletions model/riscv_insts_zicsr.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,10 +198,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) },
(0x305, _) => { Some(set_mtvec(value)) },
(0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) },
(0x30A, 32) => { menvcfg = legalize_envcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) },
(0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) },
(0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits()[63 .. 32] @ value); Some(menvcfg.bits()[31 .. 0]) },
(0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits()) },
(0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now
(0x31A, 32) => { menvcfg = legalize_envcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) },
(0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits()[31 .. 0]); Some(menvcfg.bits()[63 .. 32]) },
(0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) },
(0x340, _) => { mscratch = value; Some(mscratch) },
(0x341, _) => { Some(set_xret_target(Machine, value)) },
Expand Down Expand Up @@ -248,7 +248,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) },
(0x105, _) => { Some(set_stvec(value)) },
(0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) },
(0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) },
(0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits()[sizeof(xlen) - 1 .. 0]) },
(0x140, _) => { sscratch = value; Some(sscratch) },
(0x141, _) => { Some(set_xret_target(Supervisor, value)) },
(0x142, _) => { scause->bits() = value; Some(scause.bits()) },
Expand Down
53 changes: 41 additions & 12 deletions model/riscv_pte.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,12 +70,27 @@

/* 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 PTE_StdExt_Bits : pteStdExtAttribs = {
N : 9,
PBMT : 8 .. 7,
RSVD : 6 .. 0
}

/*
* On SV32, there are no reserved bits available to extensions. Therefore, by
Expand All @@ -84,9 +99,9 @@ type extPte = bits(10)
* 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 @@ -99,14 +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);
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
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 @@ -117,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 @@ -137,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 @@ -149,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()
}
23 changes: 22 additions & 1 deletion 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 @@ -215,6 +221,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 @@ -865,7 +877,16 @@ bitfield Envcfg : bits(64) = {
register menvcfg : Envcfg
register senvcfg : Envcfg

function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
let v = Mk_Envcfg(v);
let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
// Svpbmt - PBMTE : PBMT enable
let o = update_PBMTE(o, if haveSvpbmt() then v.PBMTE() else 0b0);
// Other extensions are not implemented yet so all other fields are read only zero.
o
}

function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = {
let v = Mk_Envcfg(v);
let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0);
// Other extensions are not implemented yet so all other fields are read only zero.
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
34 changes: 23 additions & 11 deletions model/riscv_vmem_sv39.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,19 +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_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 @@ -110,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 @@ -119,7 +120,9 @@ 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 (pte.PPNi() & mask) != zero_extend(0b0) 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 */
/* print("walk39: misaligned superpage mapping"); */
PTW_Failure(PTW_Misaligned(), ext_ptw)
Expand All @@ -133,9 +136,18 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
}
} else {
/* normal leaf PTE */
/* let res = append(pte.PPNi(), va.PgOfs());
print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */
PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw)
if ( haveSvnapot() & eattr.N() == 0b1 & pte.PPNi()[3 .. 0] != 0b1000 ) then {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else {
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)); */
PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw)
}
}
}
}
Expand Down Expand Up @@ -185,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
Loading

0 comments on commit 19ca9db

Please sign in to comment.