Refactor CSR code to use scattered functions / mappings for ease of extension.

4 files changed, 151 insertions, 240 deletions

diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail
index ea4f065..8c0cc17 100644
--- a/model/riscv_csr_ext.sail
+++ b/model/riscv_csr_ext.sail
@@ -1,20 +1,13 @@
-/* Extensions may want to add additional CSR registers to the CSR address map.
- * These functions support access to such registers.
- *
- * The default implementation provides access to the CSRs added by the 'N'
- * extension.
- */
 
-/* returns whether a CSR is defined and accessible at a given address
- * and privilege
- */
-function ext_is_CSR_defined(csr : csreg, p : Privilege) -> bool =
-  is_NExt_CSR_defined(csr, p)   // 'N' extension
+/* numeric fallback XXX apparent sail bug prevents this from compiling for C  */
+//mapping clause csr_name_map = reg <-> "UNKNOWN CSR: " ^ hex_bits_12(reg)
+end csr_name_map
 
-/* returns the value of the CSR if it is defined */
-function ext_read_CSR(csr : csreg) -> option(xlenbits) =
-  read_NExt_CSR(csr)
+function clause ext_is_CSR_defined(_, _) = false
+end ext_is_CSR_defined
 
-/* returns false if the CSR is not defined or if the write is unsuccessful */
-function ext_write_CSR(csr : csreg, value : xlenbits) -> bool =
-  write_NExt_CSR(csr, value)
+function clause ext_read_CSR _ = None()
+end ext_read_CSR
+
+function clause ext_write_CSR (_, _) = None()
+end ext_write_CSR
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 09b89ad..7ec161b 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -1,174 +1,119 @@
 /* Mapping of csr addresses to their names. */
 
-val 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",
+val csr_name_map : csreg <-> string
+scattered mapping csr_name_map
 
-    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"
-  }
-}
+/* user trap setup */
+mapping clause csr_name_map = 0x000  <-> "ustatus"
+mapping clause csr_name_map = 0x004  <-> "uie"
+mapping clause csr_name_map = 0x005  <-> "utvec"
+/* user trap handling */
+mapping clause csr_name_map = 0x040  <-> "uscratch"
+mapping clause csr_name_map = 0x041  <-> "uepc"
+mapping clause csr_name_map = 0x042  <-> "ucause"
+mapping clause csr_name_map = 0x043  <-> "utval"
+mapping clause csr_name_map = 0x044  <-> "uip"
+/* user floating-point context */
+mapping clause csr_name_map = 0x001  <-> "fflags"
+mapping clause csr_name_map = 0x002  <-> "frm"
+mapping clause csr_name_map = 0x003  <-> "fcsr"
+/* counter/timers */
+mapping clause csr_name_map = 0xC00  <-> "cycle"
+mapping clause csr_name_map = 0xC01  <-> "time"
+mapping clause csr_name_map = 0xC02  <-> "instret"
+mapping clause csr_name_map = 0xC80  <-> "cycleh"
+mapping clause csr_name_map = 0xC81  <-> "timeh"
+mapping clause csr_name_map = 0xC82  <-> "instreth"
+/* TODO: other hpm counters */
+/* supervisor trap setup */
+mapping clause csr_name_map = 0x100  <-> "sstatus"
+mapping clause csr_name_map = 0x102  <-> "sedeleg"
+mapping clause csr_name_map = 0x103  <-> "sideleg"
+mapping clause csr_name_map = 0x104  <-> "sie"
+mapping clause csr_name_map = 0x105  <-> "stvec"
+mapping clause csr_name_map = 0x106  <-> "scounteren"
+/* supervisor trap handling */
+mapping clause csr_name_map = 0x140  <-> "sscratch"
+mapping clause csr_name_map = 0x141  <-> "sepc"
+mapping clause csr_name_map = 0x142  <-> "scause"
+mapping clause csr_name_map = 0x143  <-> "stval"
+mapping clause csr_name_map = 0x144  <-> "sip"
+/* supervisor protection and translation */
+mapping clause csr_name_map = 0x180  <-> "satp"
+/* machine information registers */
+mapping clause csr_name_map = 0xF11  <-> "mvendorid"
+mapping clause csr_name_map = 0xF12  <-> "marchid"
+mapping clause csr_name_map = 0xF13  <-> "mimpid"
+mapping clause csr_name_map = 0xF14  <-> "mhartid"
+/* machine trap setup */
+mapping clause csr_name_map = 0x300  <-> "mstatus"
+mapping clause csr_name_map = 0x301  <-> "misa"
+mapping clause csr_name_map = 0x302  <-> "medeleg"
+mapping clause csr_name_map = 0x303  <-> "mideleg"
+mapping clause csr_name_map = 0x304  <-> "mie"
+mapping clause csr_name_map = 0x305  <-> "mtvec"
+mapping clause csr_name_map = 0x306  <-> "mcounteren"
+/* machine trap handling */
+mapping clause csr_name_map = 0x340  <-> "mscratch"
+mapping clause csr_name_map = 0x341  <-> "mepc"
+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 = 0x3A0  <-> "pmpcfg0"
+mapping clause csr_name_map = 0x3A1  <-> "pmpcfg1"
+mapping clause csr_name_map = 0x3A2  <-> "pmpcfg2"
+mapping clause csr_name_map = 0x3A3  <-> "pmpcfg3"
+mapping clause csr_name_map = 0x3B0  <-> "pmpaddr0"
+mapping clause csr_name_map = 0x3B1  <-> "pmpaddr1"
+mapping clause csr_name_map = 0x3B2  <-> "pmpaddr2"
+mapping clause csr_name_map = 0x3B3  <-> "pmpaddr3"
+mapping clause csr_name_map = 0x3B4  <-> "pmpaddr4"
+mapping clause csr_name_map = 0x3B5  <-> "pmpaddr5"
+mapping clause csr_name_map = 0x3B6  <-> "pmpaddr6"
+mapping clause csr_name_map = 0x3B7  <-> "pmpaddr7"
+mapping clause csr_name_map = 0x3B8  <-> "pmpaddr8"
+mapping clause csr_name_map = 0x3B9  <-> "pmpaddr9"
+mapping clause csr_name_map = 0x3BA  <-> "pmpaddr10"
+mapping clause csr_name_map = 0x3BB  <-> "pmpaddr11"
+mapping clause csr_name_map = 0x3BC  <-> "pmpaddr12"
+mapping clause csr_name_map = 0x3BD  <-> "pmpaddr13"
+mapping clause csr_name_map = 0x3BE  <-> "pmpaddr14"
+mapping clause csr_name_map = 0x3BF  <-> "pmpaddr15"
+/* machine counters/timers */
+mapping clause csr_name_map = 0xB00  <-> "mcycle"
+mapping clause csr_name_map = 0xB02  <-> "minstret"
+mapping clause csr_name_map = 0xB80  <-> "mcycleh"
+mapping clause csr_name_map = 0xB82  <-> "minstreth"
+/* TODO: other hpm counters and events */
+/* trigger/debug */
+mapping clause csr_name_map = 0x7a0  <-> "tselect"
+mapping clause csr_name_map = 0x7a1  <-> "tdata1"
+mapping clause csr_name_map = 0x7a2  <-> "tdata2"
+mapping clause csr_name_map = 0x7a3  <-> "tdata3"
 
+val csr_name : csreg -> string
+function csr_name(csr) = csr_name_map(csr)
 overload to_str = {csr_name}
 
-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"
+/* Extensions may want to add additional CSR registers to the CSR address map.
+ * These scattered functions support access to such registers.
+ *
+ * The default implementation provides access to the CSRs added by the 'N'
+ * extension.
+ */
+
+
+/* returns whether a CSR is defined and accessible at a given address
+ * and privilege
+ */
+val ext_is_CSR_defined : (csreg, Privilege) -> bool effect {rreg}
+scattered function ext_is_CSR_defined
 
-    /* numeric fallback */
-    /* reg    <-> hex_bits_12(reg) */
- }
+/* returns the value of the CSR if it is defined */
+val ext_read_CSR : csreg -> option(xlenbits) effect {rreg}
+scattered function ext_read_CSR
 
+/* returns new value (after legalisation) if the CSR is defined */
+val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) effect {rreg, wreg}
+scattered function ext_write_CSR
\ No newline at end of file
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index ee30ec0..dd8a4a0 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -162,16 +162,12 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x144,  _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) },
     (0x180,  _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) },
 
-    _           => None()
+    _           => ext_write_CSR(csr, value)
   };
   match res {
     Some(v) => if   get_config_print_reg()
                then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
-    None()  => { /* check extensions */
-                 if   ext_write_CSR(csr, value)
-                 then ()
-                 else print_bits("unhandled write to CSR ", csr)
-               }
+    None()  => print_bits("unhandled write to CSR ", csr)
   }
 }
 
diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail
index 13f9ae5..b0ced4a 100644
--- a/model/riscv_next_control.sail
+++ b/model/riscv_next_control.sail
@@ -1,55 +1,32 @@
 /* Functional specification for the 'N' user-level interrupts standard extension. */
 
-function is_NExt_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 clause ext_is_CSR_defined(0x000, _) = haveUsrMode() // ustatus
+function clause ext_is_CSR_defined(0x004, _) = haveUsrMode() // uie
+function clause ext_is_CSR_defined(0x005, _) = haveUsrMode() // utvec
+function clause ext_is_CSR_defined(0x040, _) = haveUsrMode() // uscratch
+function clause ext_is_CSR_defined(0x041, _) = haveUsrMode() // uepc
+function clause ext_is_CSR_defined(0x042, _) = haveUsrMode() // ucause
+function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() // utval
+function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() // uip
 
-function read_NExt_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(get_utvec()),
-    0x040 => Some(uscratch),
-    0x041 => Some(get_xret_target(User) & pc_alignment_mask()),
-    0x042 => Some(ucause.bits()),
-    0x043 => Some(utval),
-    0x044 => Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits()),
-    _     => None()
-  };
-  res
-}
+function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits())
+function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits())
+function clause ext_read_CSR(0x005) = Some(get_utvec())
+function clause ext_read_CSR(0x040) = Some(uscratch)
+function clause ext_read_CSR(0x041) = Some(get_xret_target(User) & pc_alignment_mask())
+function clause ext_read_CSR(0x042) = Some(ucause.bits())
+function clause ext_read_CSR(0x043) = Some(utval)
+function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits())
 
-function write_NExt_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 => { Some(set_utvec(value)) },
-    0x040 => { uscratch = value; Some(uscratch) },
-    0x041 => { Some(set_xret_target(User, value)) },
-    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) => { if   get_config_print_reg()
-                 then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")");
-                 true },
-    None()  => false
-  }
-}
+function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits()) }
+function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value);
+                                                 mie = lift_sie(mie, mideleg, sie);
+                                                 Some(mie.bits()) }
+function clause ext_write_CSR(0x005, value) = { Some(set_utvec(value)) }
+function clause ext_write_CSR(0x040, value) = { uscratch = value; Some(uscratch) }
+function clause ext_write_CSR(0x041, value) = { Some(set_xret_target(User, value)) }
+function clause ext_write_CSR(0x042, value) = { ucause->bits() = value; Some(ucause.bits()) }
+function clause ext_write_CSR(0x043, value) = { utval = value; Some(utval) }
+function clause ext_write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value);
+                                                 mip = lift_sip(mip, mideleg, sip);
+                                                 Some(mip.bits()) }