Add PMP address and entry matching, and priority logic.

This is specialized for now for the smallest PMP grain of 4 bytes.

3 files changed, 218 insertions, 36 deletions

diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
new file mode 100644
index 0000000..d29693d
--- /dev/null
+++ b/model/riscv_pmp_control.sail
@@ -0,0 +1,159 @@
+/* address ranges */
+
+// TODO: handle PMP grain > 4 (i.e. G > 0).
+
+/* [min, max) of the matching range. */
+type pmp_addr_range = option((xlenbits, xlenbits))
+
+function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmp_addr_range = {
+  match pmpAddrMatchType_of_bits(cfg.A()) {
+    OFF   => None(),
+    TOR   => { Some ((prev_pmpaddr << 2, pmpaddr << 2)) },
+    NA4   => { // TODO: I find the spec unclear for entries marked NA4 and G = 1.
+               // (for G >= 2, it is the same as NAPOT). In particular, it affects
+               // whether pmpaddr[0] is always read as 0.
+               let lo = pmpaddr << 2;
+               Some((lo, lo + 4))
+             },
+    NAPOT => { let mask = pmpaddr ^ (pmpaddr + 1);  // generate 1s in signifying bits
+               let lo   = pmpaddr & (~ (mask));
+               let len  = mask + 1;
+               Some((lo << 2, (lo + len) << 2))
+             }
+  }
+}
+
+/* permission checks */
+
+val pmpCheckRWX: (Pmpcfg_ent, AccessType) -> bool
+function pmpCheckRWX(ent, acc) = {
+  match acc {
+    Read      => ent.R() == true,
+    Write     => ent.W() == true,
+    ReadWrite => ent.R() == true & ent.W() == true,
+    Execute   => ent.X() == true
+  }
+}
+
+// this needs to be called with the effective current privilege.
+val pmpCheckPerms: (Pmpcfg_ent, AccessType, Privilege) -> bool
+function pmpCheckPerms(ent, acc, priv) = {
+  match priv {
+    Machine => if   ent.L() == true
+               then pmpCheckRWX(ent, acc)
+               else true,
+    _       => pmpCheckRWX(ent, acc)
+  }
+}
+
+/* matching logic */
+
+enum pmpAddrMatch = {PMP_NoMatch, PMP_PartialMatch, PMP_Match}
+
+function pmpMatchAddr(addr: xlenbits, width: xlenbits, rng: pmp_addr_range) -> pmpAddrMatch = {
+  match rng {
+    None()         => PMP_NoMatch,
+    Some((lo, hi)) => if   hi <_u lo   /* to handle mis-configuration */
+                      then PMP_NoMatch
+                      else {
+                        if      (addr + width <_u lo) | (hi <_u addr)
+                        then    PMP_NoMatch
+                        else if (lo <=_u addr) & (addr + width <=_u hi)
+                        then    PMP_Match
+                        else    PMP_PartialMatch
+                      }
+  }
+}
+
+enum pmpMatch = {PMP_Success, PMP_Continue, PMP_Fail}
+
+function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privilege,
+                       ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits) -> pmpMatch = {
+  let rng = pmpAddrRange(ent, pmpaddr, prev_pmpaddr);
+  match pmpMatchAddr(addr, width, rng) {
+    PMP_NoMatch      => PMP_Continue,
+    PMP_PartialMatch => PMP_Fail,
+    PMP_Match        => if   pmpCheckPerms(ent, acc, priv)
+                        then PMP_Success
+                        else PMP_Fail
+  }
+}
+
+/* priority checks */
+
+function pmpCheck(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privilege,
+                  ent: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits)
+                  -> option(ExceptionType) = {
+  // TODO: add 0th entry and addr
+  let check : bool =
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg1, pmpaddr1, pmpaddr0) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg2, pmpaddr2, pmpaddr1) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg3, pmpaddr3, pmpaddr2) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg4, pmpaddr4, pmpaddr3) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg5, pmpaddr5, pmpaddr4) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg6, pmpaddr6, pmpaddr5) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg7, pmpaddr7, pmpaddr6) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg8, pmpaddr8, pmpaddr7) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg9, pmpaddr9, pmpaddr8) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg10, pmpaddr10, pmpaddr9) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg11, pmpaddr11, pmpaddr10) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg12, pmpaddr12, pmpaddr11) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg13, pmpaddr13, pmpaddr12) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg14, pmpaddr14, pmpaddr13) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
+  match pmpMatchEntry(addr, width, acc, priv, pmpcfg15, pmpaddr15, pmpaddr14) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue => false
+  }}}}}}}}}}}}}}};
+
+  if   check
+  then None()
+  else match acc {
+    Read      => Some(E_Load_Access_Fault),
+    Write     => Some(E_SAMO_Access_Fault),
+    ReadWrite => Some(E_SAMO_Access_Fault),
+    Execute   => Some(E_Fetch_Access_Fault)
+  }
+}
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index 827f9fd..f73dfa8 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -1,3 +1,5 @@
+/* PMP configuration entries */
+
 enum PmpAddrMatchType = {OFF, TOR, NA4, NAPOT}
 
 val cast pmpAddrMatchType_of_bits : bits(2) -> PmpAddrMatchType
@@ -20,12 +22,23 @@ bitfield Pmpcfg_ent : bits(8) = {
   R : 0         /* read */
 }
 
-type Pmpcfg_reg = vector(xlen_bytes, dec, Pmpcfg_ent)
-
-register Pmpcfg0 : Pmpcfg_reg
-register Pmpcfg1 : Pmpcfg_reg
-register Pmpcfg2 : Pmpcfg_reg
-register Pmpcfg3 : Pmpcfg_reg
+register pmpcfg0 : xlenbits // fixme
+//register pmpcfg0 : Pmpcfg_reg
+register pmpcfg1  : Pmpcfg_ent
+register pmpcfg2  : Pmpcfg_ent
+register pmpcfg3  : Pmpcfg_ent
+register pmpcfg4  : Pmpcfg_ent
+register pmpcfg5  : Pmpcfg_ent
+register pmpcfg6  : Pmpcfg_ent
+register pmpcfg7  : Pmpcfg_ent
+register pmpcfg8  : Pmpcfg_ent
+register pmpcfg9  : Pmpcfg_ent
+register pmpcfg10 : Pmpcfg_ent
+register pmpcfg11 : Pmpcfg_ent
+register pmpcfg12 : Pmpcfg_ent
+register pmpcfg13 : Pmpcfg_ent
+register pmpcfg14 : Pmpcfg_ent
+register pmpcfg15 : Pmpcfg_ent
 
 bitfield Pmp_addr_64 : bits(64) = {
   addr : 53 .. 0
@@ -35,30 +48,45 @@ bitfield Pmp_addr_32 : bits(32) = {
   addr : 31 .. 0
 }
 
-val pmpCheckRWX: (Pmpcfg_ent, AccessType) -> option(ExceptionType)
-function pmpCheckRWX(ent, acc) = {
-  match acc {
-    Read      => if   ent.R() == true
-                 then None()
-                 else Some(E_Load_Access_Fault),
-    Write     => if   ent.W() == true
-                 then None()
-                 else Some(E_SAMO_Access_Fault),
-    ReadWrite => if   ent.R() == true & ent.W() == true
-                 then None()
-                 else Some(E_SAMO_Access_Fault),
-    Execute   => if   ent.X() == true
-                 then None()
-                 else Some(E_Fetch_Access_Fault)
-  }
-}
+/* PMP address configuration */
 
-val pmpCheckPerms: (Pmpcfg_ent, AccessType, Privilege) -> option(ExceptionType)
-function pmpCheckPerms(ent, acc, priv) = {
-  match priv {
-    Machine => if   ent.L() == true
-               then pmpCheckRWX(ent, acc)
-               else None(),
-    _       => pmpCheckRWX(ent, acc)
-  }
+register pmpaddr0  : xlenbits
+register pmpaddr1  : xlenbits
+register pmpaddr2  : xlenbits
+register pmpaddr3  : xlenbits
+register pmpaddr4  : xlenbits
+register pmpaddr5  : xlenbits
+register pmpaddr6  : xlenbits
+register pmpaddr7  : xlenbits
+register pmpaddr8  : xlenbits
+register pmpaddr9  : xlenbits
+register pmpaddr10 : xlenbits
+register pmpaddr11 : xlenbits
+register pmpaddr12 : xlenbits
+register pmpaddr13 : xlenbits
+register pmpaddr14 : xlenbits
+register pmpaddr15 : xlenbits
+
+val pmpReadReg : forall 'n, 0 <= 'n < 16 . (atom('n), PmpAddrMatchType) -> xlenbits
+function pmpReadReg(n, amt) = {
+  let r : xlenbits =
+    match n {
+      0  => pmpaddr0,
+      1  => pmpaddr1,
+      2  => pmpaddr2,
+      3  => pmpaddr3,
+      4  => pmpaddr4,
+      5  => pmpaddr5,
+      6  => pmpaddr6,
+      7  => pmpaddr7,
+      8  => pmpaddr8,
+      9  => pmpaddr9,
+      10 => pmpaddr10,
+      11 => pmpaddr11,
+      12 => pmpaddr12,
+      13 => pmpaddr13,
+      14 => pmpaddr14,
+      15 => pmpaddr15
+    };
+  r
 }
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 783785a..27e0c00 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -408,11 +408,6 @@ register marchid : xlenbits
 /* TODO: this should be readonly, and always 0 for now */
 register mhartid : xlenbits
 
-/* physical memory protection configuration */
-register pmpaddr0 : xlenbits
-register pmpcfg0 : xlenbits
-
-
 /* S-mode registers */
 
 /* sstatus reveals a subset of mstatus */