Checked locked flag on PMP reg writes, and add the special case for the pmpaddr0 check.

3 files changed, 64 insertions, 62 deletions

diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index b95caaa..85a0a1e 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -133,22 +133,22 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
                    },
     (0x3A3, 32) => { pmpWriteCfgReg_RV32(3, value); Some(value) },  // pmpcfg3
 
-    (0x3B0,  _) => { pmpaddr0  = value; Some(pmpaddr0) },
-    (0x3B1,  _) => { pmpaddr1  = value; Some(pmpaddr1) },
-    (0x3B2,  _) => { pmpaddr2  = value; Some(pmpaddr2) },
-    (0x3B3,  _) => { pmpaddr3  = value; Some(pmpaddr3) },
-    (0x3B4,  _) => { pmpaddr4  = value; Some(pmpaddr4) },
-    (0x3B5,  _) => { pmpaddr5  = value; Some(pmpaddr5) },
-    (0x3B6,  _) => { pmpaddr6  = value; Some(pmpaddr6) },
-    (0x3B7,  _) => { pmpaddr7  = value; Some(pmpaddr7) },
-    (0x3B8,  _) => { pmpaddr8  = value; Some(pmpaddr8) },
-    (0x3B9,  _) => { pmpaddr9  = value; Some(pmpaddr9) },
-    (0x3BA,  _) => { pmpaddr10 = value; Some(pmpaddr10) },
-    (0x3BB,  _) => { pmpaddr11 = value; Some(pmpaddr11) },
-    (0x3BC,  _) => { pmpaddr12 = value; Some(pmpaddr12) },
-    (0x3BD,  _) => { pmpaddr13 = value; Some(pmpaddr13) },
-    (0x3BE,  _) => { pmpaddr14 = value; Some(pmpaddr14) },
-    (0x3BF,  _) => { pmpaddr15 = value; Some(pmpaddr15) },
+    (0x3B0,  _) => { pmpaddr0  = pmpWriteAddr(pmp0cfg,  pmpaddr0,  value); Some(pmpaddr0) },
+    (0x3B1,  _) => { pmpaddr1  = pmpWriteAddr(pmp1cfg,  pmpaddr1,  value); Some(pmpaddr1) },
+    (0x3B2,  _) => { pmpaddr2  = pmpWriteAddr(pmp2cfg,  pmpaddr2,  value); Some(pmpaddr2) },
+    (0x3B3,  _) => { pmpaddr3  = pmpWriteAddr(pmp3cfg,  pmpaddr3,  value); Some(pmpaddr3) },
+    (0x3B4,  _) => { pmpaddr4  = pmpWriteAddr(pmp4cfg,  pmpaddr4,  value); Some(pmpaddr4) },
+    (0x3B5,  _) => { pmpaddr5  = pmpWriteAddr(pmp5cfg,  pmpaddr5,  value); Some(pmpaddr5) },
+    (0x3B6,  _) => { pmpaddr6  = pmpWriteAddr(pmp6cfg,  pmpaddr6,  value); Some(pmpaddr6) },
+    (0x3B7,  _) => { pmpaddr7  = pmpWriteAddr(pmp7cfg,  pmpaddr7,  value); Some(pmpaddr7) },
+    (0x3B8,  _) => { pmpaddr8  = pmpWriteAddr(pmp8cfg,  pmpaddr8,  value); Some(pmpaddr8) },
+    (0x3B9,  _) => { pmpaddr9  = pmpWriteAddr(pmp9cfg,  pmpaddr9,  value); Some(pmpaddr9) },
+    (0x3BA,  _) => { pmpaddr10 = pmpWriteAddr(pmp10cfg, pmpaddr10, value); Some(pmpaddr10) },
+    (0x3BB,  _) => { pmpaddr11 = pmpWriteAddr(pmp11cfg, pmpaddr11, value); Some(pmpaddr11) },
+    (0x3BC,  _) => { pmpaddr12 = pmpWriteAddr(pmp12cfg, pmpaddr12, value); Some(pmpaddr12) },
+    (0x3BD,  _) => { pmpaddr13 = pmpWriteAddr(pmp13cfg, pmpaddr13, value); Some(pmpaddr13) },
+    (0x3BE,  _) => { pmpaddr14 = pmpWriteAddr(pmp14cfg, pmpaddr14, value); Some(pmpaddr14) },
+    (0x3BF,  _) => { pmpaddr15 = pmpWriteAddr(pmp15cfg, pmpaddr15, value); Some(pmpaddr15) },
 
     /* machine mode counters */
     (0xB00,  _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index be8862d..4260888 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -1,6 +1,7 @@
 /* address ranges */
 
 // TODO: handle PMP grain > 4 (i.e. G > 0).
+// TODO: handle the 34-bit paddr32 on RV32
 
 /* [min, max) of the matching range. */
 type pmp_addr_range = option((xlenbits, xlenbits))
@@ -84,8 +85,11 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType, priv: P
 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, pmp0cfg, pmpaddr0, zeros()) {
+    PMP_Success  => true,
+    PMP_Fail     => false,
+    PMP_Continue =>
   match pmpMatchEntry(addr, width, acc, priv, pmp1cfg, pmpaddr1, pmpaddr0) {
     PMP_Success  => true,
     PMP_Fail     => false,
@@ -146,7 +150,7 @@ function pmpCheck(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privil
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue => false
-  }}}}}}}}}}}}}}};
+  }}}}}}}}}}}}}}}};
 
   if   check
   then None()
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index 249d913..5d1ee40 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -39,14 +39,6 @@ register pmp13cfg : Pmpcfg_ent
 register pmp14cfg : Pmpcfg_ent
 register pmp15cfg : Pmpcfg_ent
 
-bitfield Pmp_addr_64 : bits(64) = {
-  addr : 53 .. 0
-}
-
-bitfield Pmp_addr_32 : bits(32) = {
-  addr : 31 .. 0
-}
-
 /* PMP address configuration */
 
 register pmpaddr0  : xlenbits
@@ -86,54 +78,60 @@ function pmpReadCfgReg_RV64(n) = {
   }
 }
 
-// FIXME: handle locked
-val pmpWriteCfgReg_RV32 : forall 'n, 0 <= 'n < 4 & xlen == 32 . (atom('n), xlenbits) -> unit effect {wreg}
+function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
+  if cfg.L() == true then cfg else Mk_Pmpcfg_ent(v)
+
+val pmpWriteCfgReg_RV32 : forall 'n, 0 <= 'n < 4 & xlen == 32 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
 function pmpWriteCfgReg_RV32(n, v) = {
   match n {
-    0 => { pmp0cfg  = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmp1cfg  = Mk_Pmpcfg_ent(v[15..8]);
-           pmp2cfg  = Mk_Pmpcfg_ent(v[23..16]);
-           pmp3cfg  = Mk_Pmpcfg_ent(v[31..24])
+    0 => { pmp0cfg  = pmpWriteCfg(pmp0cfg,  v[7 ..0]);
+           pmp1cfg  = pmpWriteCfg(pmp1cfg,  v[15..8]);
+           pmp2cfg  = pmpWriteCfg(pmp2cfg,  v[23..16]);
+           pmp3cfg  = pmpWriteCfg(pmp3cfg,  v[31..24]);
          },
-    1 => { pmp4cfg  = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmp5cfg  = Mk_Pmpcfg_ent(v[15..8]);
-           pmp6cfg  = Mk_Pmpcfg_ent(v[23..16]);
-           pmp7cfg  = Mk_Pmpcfg_ent(v[31..24])
+    1 => { pmp4cfg  = pmpWriteCfg(pmp4cfg,  v[7 ..0]);
+           pmp5cfg  = pmpWriteCfg(pmp5cfg,  v[15..8]);
+           pmp6cfg  = pmpWriteCfg(pmp6cfg,  v[23..16]);
+           pmp7cfg  = pmpWriteCfg(pmp7cfg,  v[31..24]);
          },
-    2 => { pmp8cfg8 = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmp9cfg9 = Mk_Pmpcfg_ent(v[15..8]);
-           pmp10cfg = Mk_Pmpcfg_ent(v[23..16]);
-           pmp11cfg = Mk_Pmpcfg_ent(v[31..24])
+    2 => { pmp8cfg8 = pmpWriteCfg(pmp8cfg,  v[7 ..0]);
+           pmp9cfg9 = pmpWriteCfg(pmp9cfg,  v[15..8]);
+           pmp10cfg = pmpWriteCfg(pmp10cfg, v[23..16]);
+           pmp11cfg = pmpWriteCfg(pmp11cfg, v[31..24]);
          },
-    3 => { pmp12cfg = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmp13cfg = Mk_Pmpcfg_ent(v[15..8]);
-           pmp14cfg = Mk_Pmpcfg_ent(v[23..16]);
-           pmp15cfg = Mk_Pmpcfg_ent(v[31..24])
+    3 => { pmp12cfg = pmpWriteCfg(pmp12cfg, v[7 ..0]);
+           pmp13cfg = pmpWriteCfg(pmp13cfg, v[15..8]);
+           pmp14cfg = pmpWriteCfg(pmp14cfg, v[23..16]);
+           pmp15cfg = pmpWriteCfg(pmp15cfg, v[31..24]);
          }
   }
 }
 
-// FIXME: handle locked
-val pmpWriteCfgReg_RV64 : forall 'n, 0 <= 'n < 2 & xlen == 64 . (atom('n), xlenbits) -> unit effect {wreg}
+val pmpWriteCfgReg_RV64 : forall 'n, 0 <= 'n < 2 & xlen == 64 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
 function pmpWriteCfgReg_RV64(n, v) = {
   match n {
-    0 => { pmp0cfg  = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmp1cfg  = Mk_Pmpcfg_ent(v[15..8]);
-           pmp2cfg  = Mk_Pmpcfg_ent(v[23..16]);
-           pmp3cfg  = Mk_Pmpcfg_ent(v[31..24]);
-           pmp4cfg  = Mk_Pmpcfg_ent(v[39..32]);
-           pmp5cfg  = Mk_Pmpcfg_ent(v[47..40]);
-           pmp6cfg  = Mk_Pmpcfg_ent(v[55..48]);
-           pmp7cfg  = Mk_Pmpcfg_ent(v[63..56])
+    0 => { pmp0cfg  = pmpWriteCfg(pmp0cfg,  v[7 ..0]);
+           pmp1cfg  = pmpWriteCfg(pmp1cfg,  v[15..8]);
+           pmp2cfg  = pmpWriteCfg(pmp2cfg,  v[23..16]);
+           pmp3cfg  = pmpWriteCfg(pmp3cfg,  v[31..24]);
+           pmp4cfg  = pmpWriteCfg(pmp4cfg,  v[39..32]);
+           pmp5cfg  = pmpWriteCfg(pmp5cfg,  v[47..40]);
+           pmp6cfg  = pmpWriteCfg(pmp6cfg,  v[55..48]);
+           pmp7cfg  = pmpWriteCfg(pmp7cfg,  v[63..56])
          },
-    1 => { pmp8cfg8 = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmp9cfg9 = Mk_Pmpcfg_ent(v[15..8]);
-           pmp10cfg = Mk_Pmpcfg_ent(v[23..16]);
-           pmp11cfg = Mk_Pmpcfg_ent(v[31..24]);
-           pmp12cfg = Mk_Pmpcfg_ent(v[39..32]);
-           pmp13cfg = Mk_Pmpcfg_ent(v[47..40]);
-           pmp14cfg = Mk_Pmpcfg_ent(v[55..48]);
-           pmp15cfg = Mk_Pmpcfg_ent(v[63..56])
+    1 => { pmp8cfg8 = pmpWriteCfg(pmp8cfg,  v[7 ..0]);
+           pmp9cfg9 = pmpWriteCfg(pmp9cfg,  v[15..8]);
+           pmp10cfg = pmpWriteCfg(pmp10cfg, v[23..16]);
+           pmp11cfg = pmpWriteCfg(pmp11cfg, v[31..24]);
+           pmp12cfg = pmpWriteCfg(pmp12cfg, v[39..32]);
+           pmp13cfg = pmpWriteCfg(pmp13cfg, v[47..40]);
+           pmp14cfg = pmpWriteCfg(pmp14cfg, v[55..48]);
+           pmp15cfg = pmpWriteCfg(pmp15cfg, v[63..56])
          }
   }
 }
+
+function pmpWriteAddr(cfg: Pmpcfg_ent, reg: xlenbits, v: xlenbits) -> xlenbits =
+  if   sizeof(xlen) == 32
+  then { if cfg.L() == true then reg else v }
+  else { if cfg.L() == true then reg else EXTZ(v[53..0]) }