Add CSRs for the 'N' extension arch state and expose to CSR read/write.

5 files changed, 322 insertions, 186 deletions

diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
new file mode 100644
index 0000000..f484d8d
--- /dev/null
+++ b/model/riscv_csr_map.sail
@@ -0,0 +1,172 @@
+/* Mapping of csr addresses to their names. */
+
+val cast csr_name : csreg -> string
+function csr_name(csr) = {
+  match (csr) {
+    /* user trap setup */
+    0x000  => "ustatus",
+    0x004  => "uie",
+    0x005  => "utvec",
+    /* user trap handling */
+    0x040  => "uscratch",
+    0x041  => "uepc",
+    0x042  => "ucause",
+    0x043  => "utval",
+    0x044  => "uip",
+
+    /* user floating-point context */
+    0x001  => "fflags",
+    0x002  => "frm",
+    0x003  => "fcsr",
+    /* counter/timers */
+    0xC00  => "cycle",
+    0xC01  => "time",
+    0xC02  => "instret",
+    0xC80  => "cycleh",
+    0xC81  => "timeh",
+    0xC82  => "instreth",
+    /* TODO: other hpm counters */
+    /* supervisor trap setup */
+    0x100  => "sstatus",
+    0x102  => "sedeleg",
+    0x103  => "sideleg",
+    0x104  => "sie",
+    0x105  => "stvec",
+    0x106  => "scounteren",
+    /* supervisor trap handling */
+    0x140  => "sscratch",
+    0x141  => "sepc",
+    0x142  => "scause",
+    0x143  => "stval",
+    0x144  => "sip",
+    /* supervisor protection and translation */
+    0x180  => "satp",
+    /* machine information registers */
+    0xF11  => "mvendorid",
+    0xF12  => "marchid",
+    0xF13  => "mimpid",
+    0xF14  => "mhartid",
+    /* machine trap setup */
+    0x300  => "mstatus",
+    0x301  => "misa",
+    0x302  => "medeleg",
+    0x303  => "mideleg",
+    0x304  => "mie",
+    0x305  => "mtvec",
+    0x306  => "mcounteren",
+    /* machine trap handling */
+    0x340  => "mscratch",
+    0x341  => "mepc",
+    0x342  => "mcause",
+    0x343  => "mtval",
+    0x344  => "mip",
+
+    0x3A0  => "pmpcfg0",
+    0x3B0  => "pmpaddr0",
+    /* TODO: machine protection and translation */
+    /* machine counters/timers */
+    0xB00  => "mcycle",
+    0xB02  => "minstret",
+    0xB80  => "mcycleh",
+    0xB82  => "minstreth",
+    /* TODO: other hpm counters and events */
+    /* trigger/debug */
+    0x7a0  => "tselect",
+    _      => "UNKNOWN"
+  }
+}
+
+mapping csr_name_map : csreg <-> string = {
+    /* user trap setup */
+    0x000  <-> "ustatus",
+    0x004  <-> "uie",
+    0x005  <-> "utvec",
+    /* user trap handling */
+    0x040  <-> "uscratch",
+    0x041  <-> "uepc",
+    0x042  <-> "ucause",
+    0x043  <-> "utval",
+    0x044  <-> "uip",
+    /* user floating-point context */
+    0x001  <-> "fflags",
+    0x002  <-> "frm",
+    0x003  <-> "fcsr",
+    /* counter/timers */
+    0xC00  <-> "cycle",
+    0xC01  <-> "time",
+    0xC02  <-> "instret",
+    0xC80  <-> "cycleh",
+    0xC81  <-> "timeh",
+    0xC82  <-> "instreth",
+    /* TODO: other hpm counters */
+    /* supervisor trap setup */
+    0x100  <-> "sstatus",
+    0x102  <-> "sedeleg",
+    0x103  <-> "sideleg",
+    0x104  <-> "sie",
+    0x105  <-> "stvec",
+    0x106  <-> "scounteren",
+    /* supervisor trap handling */
+    0x140  <-> "sscratch",
+    0x141  <-> "sepc",
+    0x142  <-> "scause",
+    0x143  <-> "stval",
+    0x144  <-> "sip",
+    /* supervisor protection and translation */
+    0x180  <-> "satp",
+    /* machine information registers */
+    0xF11  <-> "mvendorid",
+    0xF12  <-> "marchid",
+    0xF13  <-> "mimpid",
+    0xF14  <-> "mhartid",
+    /* machine trap setup */
+    0x300  <-> "mstatus",
+    0x301  <-> "misa",
+    0x302  <-> "medeleg",
+    0x303  <-> "mideleg",
+    0x304  <-> "mie",
+    0x305  <-> "mtvec",
+    0x306  <-> "mcounteren",
+    /* machine trap handling */
+    0x340  <-> "mscratch",
+    0x341  <-> "mepc",
+    0x342  <-> "mcause",
+    0x343  <-> "mtval",
+    0x344  <-> "mip",
+    /* machine protection and translation */
+    0x3A0  <-> "pmpcfg0",
+    0x3A1  <-> "pmpcfg1",
+    0x3A2  <-> "pmpcfg2",
+    0x3A3  <-> "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 counters/timers */
+    0xB00  <-> "mcycle",
+    0xB02  <-> "minstret",
+    0xB80  <-> "mcycleh",
+    0xB82  <-> "minstreth",
+    /* TODO: other hpm counters and events */
+    /* trigger/debug */
+    0x7a0  <-> "tselect",
+    0x7a1  <-> "tdata1",
+    0x7a2  <-> "tdata2",
+    0x7a3  <-> "tdata3"
+
+    /* numeric fallback */
+    /* reg    <-> hex_bits_12(reg) */
+ }
+
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 8c6cc31..aac2266 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -59,8 +59,12 @@ function readCSR csr : csreg -> xlenbits = {
     /* trigger/debug */
     0x7a0 => ~(tselect),    /* this indicates we don't have any trigger support */
 
-    _     => { print_bits("unhandled read to CSR ", csr);
-               0x0000_0000_0000_0000 }
+    _     =>  /* check extensions */
+              match read_UExt_CSR(csr) {
+                Some(res) => res,
+                None()    => { print_bits("unhandled read to CSR ", csr);
+                               0x0000_0000_0000_0000 }
+              }
   };
   print_reg("CSR " ^ csr ^ " -> " ^ BitStr(res));
   res
@@ -112,7 +116,11 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
   };
   match res {
     Some(v) => print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
-    None()  => print_bits("unhandled write to CSR ", csr)
+    None()  => { /* check extensions */
+                 if write_UExt_CSR(csr, value)
+                 then ()
+                 else print_bits("unhandled write to CSR ", csr)
+               }
   }
 }
 
diff --git a/model/riscv_sys_func.sail b/model/riscv_sys_func.sail
index 4ec3bf4..2576e68 100644
--- a/model/riscv_sys_func.sail
+++ b/model/riscv_sys_func.sail
@@ -1,177 +1,5 @@
 /* Machine-mode and supervisor-mode functionality. */
 
-/* CSR names */
-
-val cast csr_name : csreg -> string
-function csr_name(csr) = {
-  match (csr) {
-    /* user trap setup */
-    0x000  => "ustatus",
-    0x004  => "uie",
-    0x005  => "utvec",
-    /* user trap handling */
-    0x040  => "uscratch",
-    0x041  => "uepc",
-    0x042  => "ucause",
-    0x043  => "utval",
-    0x044  => "uip",
-
-    /* user floating-point context */
-    0x001  => "fflags",
-    0x002  => "frm",
-    0x003  => "fcsr",
-    /* counter/timers */
-    0xC00  => "cycle",
-    0xC01  => "time",
-    0xC02  => "instret",
-    0xC80  => "cycleh",
-    0xC81  => "timeh",
-    0xC82  => "instreth",
-    /* TODO: other hpm counters */
-    /* supervisor trap setup */
-    0x100  => "sstatus",
-    0x102  => "sedeleg",
-    0x103  => "sideleg",
-    0x104  => "sie",
-    0x105  => "stvec",
-    0x106  => "scounteren",
-    /* supervisor trap handling */
-    0x140  => "sscratch",
-    0x141  => "sepc",
-    0x142  => "scause",
-    0x143  => "stval",
-    0x144  => "sip",
-    /* supervisor protection and translation */
-    0x180  => "satp",
-    /* machine information registers */
-    0xF11  => "mvendorid",
-    0xF12  => "marchid",
-    0xF13  => "mimpid",
-    0xF14  => "mhartid",
-    /* machine trap setup */
-    0x300  => "mstatus",
-    0x301  => "misa",
-    0x302  => "medeleg",
-    0x303  => "mideleg",
-    0x304  => "mie",
-    0x305  => "mtvec",
-    0x306  => "mcounteren",
-    /* machine trap handling */
-    0x340  => "mscratch",
-    0x341  => "mepc",
-    0x342  => "mcause",
-    0x343  => "mtval",
-    0x344  => "mip",
-
-    0x3A0  => "pmpcfg0",
-    0x3B0  => "pmpaddr0",
-    /* TODO: machine protection and translation */
-    /* machine counters/timers */
-    0xB00  => "mcycle",
-    0xB02  => "minstret",
-    0xB80  => "mcycleh",
-    0xB82  => "minstreth",
-    /* TODO: other hpm counters and events */
-    /* trigger/debug */
-    0x7a0  => "tselect",
-    _      => "UNKNOWN"
-  }
-}
-
-mapping csr_name_map : csreg <-> string = {
-    /* user trap setup */
-    0x000  <-> "ustatus",
-    0x004  <-> "uie",
-    0x005  <-> "utvec",
-    /* user trap handling */
-    0x040  <-> "uscratch",
-    0x041  <-> "uepc",
-    0x042  <-> "ucause",
-    0x043  <-> "utval",
-    0x044  <-> "uip",
-    /* user floating-point context */
-    0x001  <-> "fflags",
-    0x002  <-> "frm",
-    0x003  <-> "fcsr",
-    /* counter/timers */
-    0xC00  <-> "cycle",
-    0xC01  <-> "time",
-    0xC02  <-> "instret",
-    0xC80  <-> "cycleh",
-    0xC81  <-> "timeh",
-    0xC82  <-> "instreth",
-    /* TODO: other hpm counters */
-    /* supervisor trap setup */
-    0x100  <-> "sstatus",
-    0x102  <-> "sedeleg",
-    0x103  <-> "sideleg",
-    0x104  <-> "sie",
-    0x105  <-> "stvec",
-    0x106  <-> "scounteren",
-    /* supervisor trap handling */
-    0x140  <-> "sscratch",
-    0x141  <-> "sepc",
-    0x142  <-> "scause",
-    0x143  <-> "stval",
-    0x144  <-> "sip",
-    /* supervisor protection and translation */
-    0x180  <-> "satp",
-    /* machine information registers */
-    0xF11  <-> "mvendorid",
-    0xF12  <-> "marchid",
-    0xF13  <-> "mimpid",
-    0xF14  <-> "mhartid",
-    /* machine trap setup */
-    0x300  <-> "mstatus",
-    0x301  <-> "misa",
-    0x302  <-> "medeleg",
-    0x303  <-> "mideleg",
-    0x304  <-> "mie",
-    0x305  <-> "mtvec",
-    0x306  <-> "mcounteren",
-    /* machine trap handling */
-    0x340  <-> "mscratch",
-    0x341  <-> "mepc",
-    0x342  <-> "mcause",
-    0x343  <-> "mtval",
-    0x344  <-> "mip",
-    /* machine protection and translation */
-    0x3A0  <-> "pmpcfg0",
-    0x3A1  <-> "pmpcfg1",
-    0x3A2  <-> "pmpcfg2",
-    0x3A3  <-> "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 counters/timers */
-    0xB00  <-> "mcycle",
-    0xB02  <-> "minstret",
-    0xB80  <-> "mcycleh",
-    0xB82  <-> "minstreth",
-    /* TODO: other hpm counters and events */
-    /* trigger/debug */
-    0x7a0  <-> "tselect",
-    0x7a1  <-> "tdata1",
-    0x7a2  <-> "tdata2",
-    0x7a3  <-> "tdata3"
-
-    /* numeric fallback */
-    /* reg    <-> hex_bits_12(reg) */
- }
-
 
 /* CSR access control */
 
@@ -225,17 +53,8 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool =
     /* disabled trigger/debug module */
     0x7a0 => p == Machine,
 
-    /* user-mode: 'N' extension */
-    0x000 => haveUsrMode(),                  // ustatus
-    0x004 => haveUsrMode(),                  // uie
-    0x005 => haveUsrMode(),                  // utvec
-    0x040 => haveUsrMode(),                  // uscratch
-    0x041 => haveUsrMode(),                  // uepc
-    0x042 => haveUsrMode(),                  // ucause
-    0x043 => haveUsrMode(),                  // utval
-    0x044 => haveUsrMode(),                  // uip
-
-    _     => false
+    /* check extensions */
+    _     => is_UExt_CSR_defined(csr, p)   // 'N' extension
   }
 
 val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
diff --git a/model/riscv_uext_func.sail b/model/riscv_uext_func.sail
new file mode 100644
index 0000000..1bcabe5
--- /dev/null
+++ b/model/riscv_uext_func.sail
@@ -0,0 +1,54 @@
+/* Functional specification for the 'N' user-level interrupts standard extension. */
+
+function is_UExt_CSR_defined(csr : bits(12), p : Privilege) -> bool =
+  match (csr) {
+    0x000 => haveUsrMode(),                  // ustatus
+    0x004 => haveUsrMode(),                  // uie
+    0x005 => haveUsrMode(),                  // utvec
+    0x040 => haveUsrMode(),                  // uscratch
+    0x041 => haveUsrMode(),                  // uepc
+    0x042 => haveUsrMode(),                  // ucause
+    0x043 => haveUsrMode(),                  // utval
+    0x044 => haveUsrMode(),                  // uip
+    _     => false
+  }
+
+function read_UExt_CSR csr : csreg -> option(xlenbits) = {
+  let res : option(xlenbits) =
+  match csr {
+    0x000 => Some(lower_sstatus(lower_mstatus(mstatus)).bits()),
+    0x004 => Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits()),
+    0x005 => Some(utvec.bits()),
+    0x040 => Some(uscratch),
+    0x041 => Some(uepc),
+    0x042 => Some(ucause.bits()),
+    0x043 => Some(utval),
+    0x044 => Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits()),
+    _     => None()
+  };
+  res
+}
+
+function write_UExt_CSR(csr : csreg, value : xlenbits) -> bool = {
+  let res : option(xlenbits) =
+  match csr {
+    0x000 => { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits()) },
+    0x004 => { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value);
+               mie = lift_sie(mie, mideleg, sie);
+               Some(mie.bits()) },
+    0x005 => { utvec = legalize_tvec(utvec, value); Some(utvec.bits()) },
+    0x040 => { uscratch = value; Some(uscratch) },
+    0x041 => { uepc = value; Some(uepc) },
+    0x042 => { ucause->bits() = value; Some(ucause.bits()) },
+    0x043 => { utval = value; Some(utval) },
+    0x044 => { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value);
+               mip = lift_sip(mip, mideleg, sip);
+               Some(mip.bits()) },
+    _     => None()
+  };
+  match res {
+    Some(v) => { print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")");
+                 true },
+    None()  => false
+  }
+}
diff --git a/model/riscv_uext_regs.sail b/model/riscv_uext_regs.sail
new file mode 100644
index 0000000..a8cc38c
--- /dev/null
+++ b/model/riscv_uext_regs.sail
@@ -0,0 +1,83 @@
+/* Architectural state for the 'N' user-level interrupts standard extension. */
+
+/* ustatus reveals a subset of mstatus */
+bitfield Ustatus : bits(64) = {
+  UPIE : 4,
+  UIE  : 0
+}
+
+/* This is a view, so there is no register defined. */
+function lower_sstatus(s : Sstatus) -> Ustatus = {
+  let u = Mk_Ustatus(EXTZ(0b0));
+  let u = update_UPIE(u, s.UPIE());
+  let u = update_UIE(u, s.UIE());
+  u
+}
+
+function lift_ustatus(s : Sstatus, u : Ustatus) -> Sstatus = {
+  let s = update_UPIE(s, u.UPIE());
+  let s = update_UIE(s, u.UIE());
+  s
+}
+
+function legalize_ustatus(m : Mstatus, v : xlenbits) -> Mstatus = {
+  let u = Mk_Ustatus(v);
+  let s = lower_mstatus(m);     // lower current mstatus to sstatus
+  let s = lift_ustatus(s, u);   // get updated sstatus
+  let m = lift_sstatus(m, s);   // lift it to an updated mstatus
+  m
+}
+
+bitfield Uinterrupts : bits(64) = {
+  UEI : 8,  /* external interrupt */
+  UTI : 4,  /* timer interrupt    */
+  USI : 0   /* software interrupt */
+}
+
+/* Provides the uip read view of sip (s) as delegated by sideleg (d). */
+function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
+  let u : Uinterrupts = Mk_Uinterrupts(EXTZ(0b0));
+  let u = update_UEI(u, s.UEI() & d.UEI());
+  let u = update_UTI(u, s.UTI() & d.UTI());
+  let u = update_USI(u, s.USI() & d.USI());
+  u
+}
+
+/* Provides the uie read view of sie as delegated by sideleg. */
+function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
+  let u : Uinterrupts = Mk_Uinterrupts(EXTZ(0b0));
+  let u = update_UEI(u, s.UEI() & d.UEI());
+  let u = update_UTI(u, s.UTI() & d.UTI());
+  let u = update_USI(u, s.USI() & d.USI());
+  u
+}
+
+/* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */
+function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
+  let s : Sinterrupts = o;
+  let s = if d.USI() == true then update_USI(s, u.USI()) else s;
+  s
+}
+
+function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterrupts = {
+  lift_uip(s, d, Mk_Uinterrupts(v))
+}
+
+/* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */
+function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
+  let s : Sinterrupts = o;
+  let s = if d.UEI() == true then update_UEI(s, u.UEI()) else s;
+  let s = if d.UTI() == true then update_UTI(s, u.UTI()) else s;
+  let s = if d.USI() == true then update_USI(s, u.USI()) else s;
+  s
+}
+
+function legalize_uie(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterrupts = {
+  lift_uie(s, d, Mk_Uinterrupts(v))
+}
+
+register utvec    : Mtvec
+register uscratch : xlenbits
+register uepc     : xlenbits
+register ucause   : Mcause
+register utval    : xlenbits