Skip to content

Commit

Permalink
Added support of Smepmp in sail Riscv
Browse files Browse the repository at this point in the history
  • Loading branch information
Hamza Khan committed Jan 26, 2023
1 parent 4d05aa1 commit b57289b
Show file tree
Hide file tree
Showing 6 changed files with 101 additions and 15 deletions.
2 changes: 2 additions & 0 deletions doc/Status.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ The Sail specification currently captures the following ISA features:

- Physical Memory Protection (PMP)

- PMP Enhancements for memory accesses and execution prevention on Machine mode (Smepmp)

For the RVWMO memory consistency model, this Sail ISA semantics is integrated with the RVWMO operational model in [the
RMEM tool](https://github.com/rems-project/rmem).

Expand Down
2 changes: 2 additions & 0 deletions model/riscv_csr_map.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,8 @@ mapping clause csr_name_map = 0x342 <-> "mcause"
mapping clause csr_name_map = 0x343 <-> "mtval"
mapping clause csr_name_map = 0x344 <-> "mip"
/* machine protection and translation */
mapping clause csr_name_map = 0x747 <-> "mseccfg"
mapping clause csr_name_map = 0x757 <-> "mseccfgh"
mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0"
mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1"
mapping clause csr_name_map = 0x3A2 <-> "pmpcfg2"
Expand Down
5 changes: 5 additions & 0 deletions model/riscv_insts_zicsr.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,9 @@ function readCSR csr : csreg -> xlenbits = {
(0x343, _) => mtval,
(0x344, _) => mip.bits(),

(0x747, _) => mseccfg.bits(), // mseccfg
(0x757, 32) => mseccfgh, // mseccfgh

(0x3A0, _) => pmpReadCfgReg(0), // pmpcfg0
(0x3A1, 32) => pmpReadCfgReg(1), // pmpcfg1
(0x3A2, _) => pmpReadCfgReg(2), // pmpcfg2
Expand Down Expand Up @@ -193,6 +196,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits()) },

// Note: Some(value) returned below is not the legalized value due to locked entries
(0x747, _) => { mseccfg = mseccfgWrite(mseccfg, value); Some(mseccfg.bits()) },
(0x757, 32) => { Some(mseccfgh) }, // ignore writes for now
(0x3A0, _) => { pmpWriteCfgReg(0, value); Some(pmpReadCfgReg(0)) }, // pmpcfg0
(0x3A1, 32) => { pmpWriteCfgReg(1, value); Some(pmpReadCfgReg(1)) }, // pmpcfg1
(0x3A2, _) => { pmpWriteCfgReg(2, value); Some(pmpReadCfgReg(2)) }, // pmpcfg2
Expand Down
50 changes: 44 additions & 6 deletions model/riscv_pmp_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,15 +104,41 @@ function pmpCheckRWX(ent, acc) = {
}
}

// this needs to be called with the effective current privilege.
val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool
/* this needs to be called with the effective current privilege */
val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool effect {rreg}
function pmpCheckPerms(ent, acc, priv) = {
if mseccfg.MML() == 0b1 then {
if ent.R() == 0b0 & ent.W() == 0b1 then {
if pmpLockBit(ent) then {
match acc {
Execute(_) => true,
Read(_) => priv == Machine & ent.X() == 0b1,
_ => false
}
} else {
match acc {
Read(_) => true,
Write(_) => priv == Machine | ent.X() == 0b1,
_ => false
}}
} else {
if ent.R() == 0b1 & ent.W() == 0b1 & ent.X() == 0b1 & pmpLockBit(ent) then {
match acc {
Read(_) => true,
_ => false
}
} else {
if (priv == Machine) == pmpLockBit(ent)
then pmpCheckRWX(ent, acc)
else false
}}
} else {
match priv {
Machine => if pmpLocked(ent)
Machine => if pmpLockBit(ent)
then pmpCheckRWX(ent, acc)
else true,
_ => pmpCheckRWX(ent, acc)
}
}}
}

/* matching logic */
Expand Down Expand Up @@ -218,9 +244,17 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
PMP_Success => true,
PMP_Fail => false,
PMP_Continue => match priv {
Machine => true,
_ => false
Machine => if mseccfg.MMWP() == 0b1 /* Make Read, Write and execute denied by default, if condition meets for M mode */
then false
else if mseccfg.MML() == 0b1
then { /* Make execute denied, if condition meets for M mode */
match acc {
Execute(_) => false,
_ => true
}
} else true,
_ => false /* Make Read, Write and execute denied by default for S/U mode */
}
}}}}}}}}}}}}}}}};

if check
Expand All @@ -234,6 +268,10 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
}

function init_pmp() -> unit = {
mseccfg->RLB() = 0b0;
mseccfg->MML() = 0b0;
mseccfg->MMWP() = 0b0;
mseccfgh = EXTZ(0b0);
pmp0cfg = update_A(pmp0cfg, pmpAddrMatchType_to_bits(OFF));
pmp1cfg = update_A(pmp1cfg, pmpAddrMatchType_to_bits(OFF));
pmp2cfg = update_A(pmp2cfg, pmpAddrMatchType_to_bits(OFF));
Expand Down
54 changes: 45 additions & 9 deletions model/riscv_pmp_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,15 @@ bitfield Pmpcfg_ent : bits(8) = {
R : 0 /* read */
}

bitfield Mseccfg_ent : xlenbits = {
RLB : 2, /* Rule Locking Bypass */
MMWP : 1, /* Machine Mode Whitelist Policy */
MML : 0 /* Machine Mode Lockdown */
}

register mseccfg : Mseccfg_ent
register mseccfgh : bits(32)

register pmp0cfg : Pmpcfg_ent
register pmp1cfg : Pmpcfg_ent
register pmp2cfg : Pmpcfg_ent
Expand Down Expand Up @@ -154,15 +163,31 @@ function pmpReadCfgReg(n) = {
}

/* Helpers to handle locked entries */
function pmpLocked(cfg: Pmpcfg_ent) -> bool =
cfg.L() == 0b1

function pmpTORLocked(cfg: Pmpcfg_ent) -> bool =
(cfg.L() == 0b1) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR)

function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
if pmpLocked(cfg) then cfg
else Mk_Pmpcfg_ent(v & 0x9f) // Bits 5 and 6 are zero.
function pmpLockBit(cfg: Pmpcfg_ent) -> bool = cfg.L() == 0b1

function pmpLocked(cfg: Pmpcfg_ent) -> bool = (cfg.L() == 0b1) & (mseccfg.RLB() == 0b0)

function pmpTORLocked(cfg: Pmpcfg_ent) -> bool = (cfg.L() == 0b1) & (mseccfg.RLB() == 0b0) & (pmpAddrMatchType_of_bits(cfg.A()) == TOR)

function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = {
let RWX_001 : Pmpcfg_ent = Mk_Pmpcfg_ent(v[7 .. 3] @ 0b1 @ 0b0 @ 0b0);
let RWX_010 : Pmpcfg_ent = Mk_Pmpcfg_ent(v[7 .. 3] @ 0b0 @ 0b1 @ 0b0);
let RWX_011 : Pmpcfg_ent = Mk_Pmpcfg_ent(v[7 .. 3] @ 0b1 @ 0b1 @ 0b0);
let RWX_101 : Pmpcfg_ent = Mk_Pmpcfg_ent(v[7 .. 3] @ 0b1 @ 0b0 @ 0b1);
let val_to_write : Pmpcfg_ent = Mk_Pmpcfg_ent(v & 0xff);
if pmpLocked(cfg) then cfg /* If locked then configuration is unchanged */
else {
if ((mseccfg.MML() == 0b1) & (mseccfg.RLB() == 0b0) & (v[7] == bitone)) then {
if ((val_to_write == RWX_001) | (val_to_write == RWX_010) | (val_to_write == RWX_011) | (val_to_write == RWX_101))
then cfg /* If condition meets configuration remains same which means pmpcfg writes are ignored */
else Mk_Pmpcfg_ent(v & 0x9f) /* Bits 5 and 6 are zero */
} else {
if (mseccfg.MML() == 0b0) & (v[0] == bitzero) & (v[1] == bitone)
then Mk_Pmpcfg_ent(v & 0x9c) /* Bits 5 and 6 are zero and Bits 0 and 1 are zero because of RW=01 reserved combination */
else Mk_Pmpcfg_ent(v & 0x9f) /* Bits 5 and 6 are zero */
}
}
}

val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
function pmpWriteCfgReg(n, v) = {
Expand Down Expand Up @@ -216,3 +241,14 @@ function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits
if sizeof(xlen) == 32
then { if (locked | tor_locked) then reg else v }
else { if (locked | tor_locked) then reg else EXTZ(v[53..0]) }

function mseccfgWrite(reg: Mseccfg_ent, v: xlenbits) -> Mseccfg_ent = /* to set RLB, need to check PMPCFG_L */
if mseccfg.RLB() == 0b0 & v[2] == bitone then {
if (pmp0cfg.L() == 0b1 | pmp1cfg.L() == 0b1 | pmp2cfg.L() == 0b1 | pmp3cfg.L() == 0b1
| pmp4cfg.L() == 0b1 | pmp5cfg.L() == 0b1 | pmp6cfg.L() == 0b1 | pmp7cfg.L() == 0b1
| pmp8cfg.L() == 0b1 | pmp9cfg.L() == 0b1 | pmp10cfg.L() == 0b1 | pmp11cfg.L() == 0b1
| pmp12cfg.L() == 0b1 | pmp13cfg.L() == 0b1 | pmp14cfg.L() == 0b1 | pmp15cfg.L() == 0b1)
then Mk_Mseccfg_ent(reg.bits() | (v & EXTZ(0b11)))
else Mk_Mseccfg_ent(reg.bits() | (v & EXTZ(0b111)))
}
else Mk_Mseccfg_ent((reg.bits() & EXTZ(0b11)) | (v & EXTZ(0b111))) /* Implements stickiness if once set remains set */
3 changes: 3 additions & 0 deletions model/riscv_sys_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,9 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x343 => p == Machine, // mtval
0x344 => p == Machine, // mip

0x747 => p == Machine, // mseccfg
0x757 => p == Machine & (sizeof(xlen) == 32), // mseccfgh

0x3A0 => p == Machine, // pmpcfg0
0x3A1 => p == Machine & (sizeof(xlen) == 32), // pmpcfg1
0x3A2 => p == Machine, // pmpcfg2
Expand Down

0 comments on commit b57289b

Please sign in to comment.