Hook in csr reads/writes to PMP regs. Locked entries are not yet handled.

3 files changed, 129 insertions, 85 deletions

diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 9a2cf9f..b95caaa 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -34,8 +34,31 @@ function readCSR csr : csreg -> xlenbits = {
     (0x343,  _) => mtval,
     (0x344,  _) => mip.bits(),
 
-    (0x3A0,  _) => pmpcfg0,
+    (0x3A0,  _) => if   sizeof(xlen) == 32     // pmpcfg0
+                   then pmpReadCfgReg_RV32(0)
+                   else pmpReadCfgReg_RV64(0),
+    (0x3A1, 32) => pmpReadCfgReg_RV32(1),      // pmpcfg1
+    (0x3A2,  _) => if   sizeof(xlen) == 32     // pmpcfg2
+                   then pmpReadCfgReg_RV32(2)
+                   else pmpReadCfgReg_RV64(1), // {0,1} internal indices for RV64
+    (0x3A3, 32) => pmpReadCfgReg_RV32(3),      // pmpcfg3
+
     (0x3B0,  _) => pmpaddr0,
+    (0x3B1,  _) => pmpaddr1,
+    (0x3B2,  _) => pmpaddr2,
+    (0x3B3,  _) => pmpaddr3,
+    (0x3B4,  _) => pmpaddr4,
+    (0x3B5,  _) => pmpaddr5,
+    (0x3B6,  _) => pmpaddr6,
+    (0x3B7,  _) => pmpaddr7,
+    (0x3B8,  _) => pmpaddr8,
+    (0x3B9,  _) => pmpaddr9,
+    (0x3BA,  _) => pmpaddr10,
+    (0x3BB,  _) => pmpaddr11,
+    (0x3BC,  _) => pmpaddr12,
+    (0x3BD,  _) => pmpaddr13,
+    (0x3BE,  _) => pmpaddr14,
+    (0x3BF,  _) => pmpaddr15,
 
     /* machine mode counters */
     (0xB00,  _) => mcycle[(sizeof(xlen) - 1) .. 0],
@@ -96,8 +119,36 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x343,  _) => { mtval = value; Some(mtval) },
     (0x344,  _) => { mip = legalize_mip(mip, value); Some(mip.bits()) },
 
-    (0x3A0,  _) => { pmpcfg0 = value; Some(pmpcfg0) },   /* FIXME: legalize */
-    (0x3B0,  _) => { pmpaddr0 = value; Some(pmpaddr0) }, /* FIXME: legalize */
+    // Note: Some(value) returned below is not the legalized value due to locked entries
+    (0x3A0,  _) => { if   sizeof(xlen) == 32                        // pmpcfg0
+                     then pmpWriteCfgReg_RV32(0, value)
+                     else pmpWriteCfgReg_RV64(0, value);
+                     Some(value)
+                   },
+    (0x3A1, 32) => { pmpWriteCfgReg_RV32(1, value); Some(value) },  // pmpcfg1
+    (0x3A2,  _) => { if   sizeof(xlen) == 32                        // pmpcfg2
+                     then pmpWriteCfgReg_RV32(2, value)
+                     else pmpWriteCfgReg_RV64(1, value);            // {0,1} internal indices for RV64
+                     Some(value)
+                   },
+    (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) },
 
     /* 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 d29693d..be8862d 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -86,63 +86,63 @@ function pmpCheck(addr: xlenbits, width: xlenbits, acc: AccessType, priv: Privil
                   -> option(ExceptionType) = {
   // TODO: add 0th entry and addr
   let check : bool =
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg1, pmpaddr1, pmpaddr0) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp1cfg, pmpaddr1, pmpaddr0) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg2, pmpaddr2, pmpaddr1) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp2cfg, pmpaddr2, pmpaddr1) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg3, pmpaddr3, pmpaddr2) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp3cfg, pmpaddr3, pmpaddr2) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg4, pmpaddr4, pmpaddr3) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp4cfg, pmpaddr4, pmpaddr3) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg5, pmpaddr5, pmpaddr4) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp5cfg, pmpaddr5, pmpaddr4) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg6, pmpaddr6, pmpaddr5) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp6cfg, pmpaddr6, pmpaddr5) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg7, pmpaddr7, pmpaddr6) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp7cfg, pmpaddr7, pmpaddr6) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg8, pmpaddr8, pmpaddr7) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp8cfg, pmpaddr8, pmpaddr7) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg9, pmpaddr9, pmpaddr8) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp9cfg, pmpaddr9, pmpaddr8) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg10, pmpaddr10, pmpaddr9) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp10cfg, pmpaddr10, pmpaddr9) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg11, pmpaddr11, pmpaddr10) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp11cfg, pmpaddr11, pmpaddr10) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg12, pmpaddr12, pmpaddr11) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp12cfg, pmpaddr12, pmpaddr11) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg13, pmpaddr13, pmpaddr12) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp13cfg, pmpaddr13, pmpaddr12) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg14, pmpaddr14, pmpaddr13) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp14cfg, pmpaddr14, pmpaddr13) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue =>
-  match pmpMatchEntry(addr, width, acc, priv, pmpcfg15, pmpaddr15, pmpaddr14) {
+  match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) {
     PMP_Success  => true,
     PMP_Fail     => false,
     PMP_Continue => false
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index c99f512..249d913 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -22,23 +22,22 @@ bitfield Pmpcfg_ent : bits(8) = {
   R : 0         /* read */
 }
 
-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
+register pmp0cfg  : Pmpcfg_ent
+register pmp1cfg  : Pmpcfg_ent
+register pmp2cfg  : Pmpcfg_ent
+register pmp3cfg  : Pmpcfg_ent
+register pmp4cfg  : Pmpcfg_ent
+register pmp5cfg  : Pmpcfg_ent
+register pmp6cfg  : Pmpcfg_ent
+register pmp7cfg  : Pmpcfg_ent
+register pmp8cfg  : Pmpcfg_ent
+register pmp9cfg  : Pmpcfg_ent
+register pmp10cfg : Pmpcfg_ent
+register pmp11cfg : Pmpcfg_ent
+register pmp12cfg : Pmpcfg_ent
+register pmp13cfg : Pmpcfg_ent
+register pmp14cfg : Pmpcfg_ent
+register pmp15cfg : Pmpcfg_ent
 
 bitfield Pmp_addr_64 : bits(64) = {
   addr : 53 .. 0
@@ -69,78 +68,72 @@ register pmpaddr15 : xlenbits
 
 /* Packing and unpacking pmpcfg regs for xlen-width accesses */
 
-val pmpReadCfgReg_RV32 : forall 'n, 0 <= 'n < 4 & xlen == 32 . (atom('n)) -> xlenbits
+val pmpReadCfgReg_RV32 : forall 'n, 0 <= 'n < 4 & xlen == 32 . (atom('n)) -> xlenbits effect {rreg}
 function pmpReadCfgReg_RV32(n) = {
   match n {
-         // fixme cfg0
-    0 => append(pmpcfg3.bits(),  append(pmpcfg2.bits(),  append(pmpcfg1.bits(),  pmpcfg1.bits()))),
-    1 => append(pmpcfg7.bits(),  append(pmpcfg6.bits(),  append(pmpcfg5.bits(),  pmpcfg4.bits()))),
-    2 => append(pmpcfg11.bits(), append(pmpcfg10.bits(), append(pmpcfg9.bits(),  pmpcfg8.bits()))),
-    3 => append(pmpcfg15.bits(), append(pmpcfg14.bits(), append(pmpcfg13.bits(), pmpcfg12.bits())))
+    0 => append(pmp3cfg.bits(),  append(pmp2cfg.bits(),  append(pmp1cfg.bits(),  pmp0cfg.bits()))),
+    1 => append(pmp7cfg.bits(),  append(pmp6cfg.bits(),  append(pmp5cfg.bits(),  pmp4cfg.bits()))),
+    2 => append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(),  pmp8cfg.bits()))),
+    3 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), pmp12cfg.bits())))
   }
 }
 
-val pmpReadCfgReg_RV64 : forall 'n, 0 <= 'n < 2 & xlen == 64 . (atom('n)) -> xlenbits
+val pmpReadCfgReg_RV64 : forall 'n, 0 <= 'n < 2 & xlen == 64 . (atom('n)) -> xlenbits effect {rreg}
 function pmpReadCfgReg_RV64(n) = {
   match n {
-         // fixme cfg0
-    0 => append(pmpcfg7.bits(),  append(pmpcfg6.bits(),  append(pmpcfg5.bits(),  append(pmpcfg4.bits(),  append(pmpcfg3.bits(),  append(pmpcfg2.bits(),  append(pmpcfg1.bits(),  pmpcfg1.bits()))))))),
-    1 => append(pmpcfg15.bits(), append(pmpcfg14.bits(), append(pmpcfg13.bits(), append(pmpcfg12.bits(), append(pmpcfg11.bits(), append(pmpcfg10.bits(), append(pmpcfg9.bits(),  pmpcfg8.bits())))))))
+    0 => append(pmp7cfg.bits(),  append(pmp6cfg.bits(),  append(pmp5cfg.bits(),  append(pmp4cfg.bits(),  append(pmp3cfg.bits(),  append(pmp2cfg.bits(),  append(pmp1cfg.bits(),  pmp0cfg.bits()))))))),
+    1 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), append(pmp12cfg.bits(), append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(),  pmp8cfg.bits())))))))
   }
 }
 
-val pmpWriteCfgReg_RV32 : forall 'n, 0 <= 'n < 4 & xlen == 32 . (atom('n), xlenbits) -> unit
+// FIXME: handle locked
+val pmpWriteCfgReg_RV32 : forall 'n, 0 <= 'n < 4 & xlen == 32 . (atom('n), xlenbits) -> unit effect {wreg}
 function pmpWriteCfgReg_RV32(n, v) = {
   match n {
-    0 => { pmpcfg1  = Mk_Pmpcfg_ent(v[7 ..0]);  // fixme
-           pmpcfg1  = Mk_Pmpcfg_ent(v[15..8]);
-           pmpcfg2  = Mk_Pmpcfg_ent(v[23..16]);
-           pmpcfg3  = Mk_Pmpcfg_ent(v[31..24]);
-           ()
+    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])
          },
-    1 => { pmpcfg4  = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmpcfg5  = Mk_Pmpcfg_ent(v[15..8]);
-           pmpcfg6  = Mk_Pmpcfg_ent(v[23..16]);
-           pmpcfg7  = Mk_Pmpcfg_ent(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])
          },
-    2 => { pmpcfg8  = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmpcfg9  = Mk_Pmpcfg_ent(v[15..8]);
-           pmpcfg10 = Mk_Pmpcfg_ent(v[23..16]);
-           pmpcfg11 = Mk_Pmpcfg_ent(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])
          },
-    3 => { pmpcfg12 = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmpcfg13 = Mk_Pmpcfg_ent(v[15..8]);
-           pmpcfg14 = Mk_Pmpcfg_ent(v[23..16]);
-           pmpcfg15 = Mk_Pmpcfg_ent(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])
          }
   }
 }
 
-val pmpWriteCfgReg_RV64 : forall 'n, 0 <= 'n < 2 & xlen == 64 . (atom('n), xlenbits) -> unit
+// FIXME: handle locked
+val pmpWriteCfgReg_RV64 : forall 'n, 0 <= 'n < 2 & xlen == 64 . (atom('n), xlenbits) -> unit effect {wreg}
 function pmpWriteCfgReg_RV64(n, v) = {
   match n {
-    0 => { pmpcfg1  = Mk_Pmpcfg_ent(v[7 ..0]);  // fixme
-           pmpcfg1  = Mk_Pmpcfg_ent(v[15..8]);
-           pmpcfg2  = Mk_Pmpcfg_ent(v[23..16]);
-           pmpcfg3  = Mk_Pmpcfg_ent(v[31..24]);
-           pmpcfg4  = Mk_Pmpcfg_ent(v[39..32]);
-           pmpcfg5  = Mk_Pmpcfg_ent(v[47..40]);
-           pmpcfg6  = Mk_Pmpcfg_ent(v[55..48]);
-           pmpcfg7  = Mk_Pmpcfg_ent(v[63..56]);
-           ()
+    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])
          },
-    1 => { pmpcfg8  = Mk_Pmpcfg_ent(v[7 ..0]);
-           pmpcfg9  = Mk_Pmpcfg_ent(v[15..8]);
-           pmpcfg10 = Mk_Pmpcfg_ent(v[23..16]);
-           pmpcfg11 = Mk_Pmpcfg_ent(v[31..24]);
-           pmpcfg12 = Mk_Pmpcfg_ent(v[39..32]);
-           pmpcfg13 = Mk_Pmpcfg_ent(v[47..40]);
-           pmpcfg14 = Mk_Pmpcfg_ent(v[55..48]);
-           pmpcfg15 = Mk_Pmpcfg_ent(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])
          }
   }
 }