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 21, 2024
1 parent d7a3d80 commit ef23f11
Show file tree
Hide file tree
Showing 5 changed files with 63 additions and 14 deletions.
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
14 changes: 13 additions & 1 deletion model/riscv_pte.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,12 @@ type pteAttribs = bits(8)
*/
type extPte = bits(10)

bitfield EXT_PTE_Bits : extPte = {
N : 9,
PBMT : 8 .. 7,
RSVD : 6 .. 0
}

/*
* On SV32, there are no reserved bits available to extensions. Therefore, by
* default, we initialize the PTE extension field with all zeros. However,
Expand Down Expand Up @@ -106,7 +112,13 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {

function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
let a = Mk_PTE_Bits(p);
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
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))
}

union PTE_Check = {
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 @@ -215,6 +215,12 @@ function haveZmmul() -> bool = true
/* Zicond extension support */
function haveZicond() -> bool = true

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

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

bitfield Mstatush : bits(32) = {
MBE : 5,
SBE : 4
Expand Down Expand Up @@ -865,7 +871,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
19 changes: 15 additions & 4 deletions model/riscv_vmem_sv39.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
let pbits = pte.BITS();
let ext_pte = pte.Ext();
let pattr = Mk_PTE_Bits(pbits);
let eattr = Mk_EXT_PTE_Bits(ext_pte);
let is_global = global | (pattr.G() == 0b1);
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
Expand Down Expand Up @@ -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 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,17 @@ 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 ( 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 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
19 changes: 15 additions & 4 deletions model/riscv_vmem_sv48.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
let pbits = pte.BITS();
let ext_pte = pte.Ext();
let pattr = Mk_PTE_Bits(pbits);
let eattr = Mk_EXT_PTE_Bits(ext_pte);
let is_global = global | (pattr.G() == 0b1);
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
Expand Down Expand Up @@ -119,7 +120,9 @@ 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 (pte.PPNi() & mask) != zero_extend(0b0) then {
if eattr.N() == 0b1 then {
PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
} else if (pte.PPNi() & mask) != zero_extend(0b0) then {
/* misaligned superpage mapping */
/* print("walk48: misaligned superpage mapping"); */
PTW_Failure(PTW_Misaligned(), ext_ptw)
Expand All @@ -133,9 +136,17 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
}
} else {
/* normal leaf PTE */
/* let res = append(pte.PPNi(), va.PgOfs());
print("walk48: 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 ( 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 res = append(ppn, va.PgOfs());
print("walk48: 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

0 comments on commit ef23f11

Please sign in to comment.