From 63cee3512fe6691f671a979555af7351574ead9e Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Fri, 4 Oct 2024 17:37:28 -0700
Subject: [PATCH 01/17] Move floating point CSRs

---
 model/riscv_csr_begin.sail     | 4 ----
 model/riscv_fdext_control.sail | 5 ++++-
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 053776435..24167bca7 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -15,10 +15,6 @@ scattered mapping csr_name_map
 // TODO: These csr_name_map definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* 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"
 /* user entropy source */
 mapping clause csr_name_map = 0x015  <-> "seed"
 /* counter/timers */
diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail
index a1de45c08..9338788df 100644
--- a/model/riscv_fdext_control.sail
+++ b/model/riscv_fdext_control.sail
@@ -24,7 +24,10 @@ function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b0
 enum clause extension = Ext_Zfinx
 function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx()
 
-/* val clause is_CSR_defined : (csreg) -> bool */
+/* Floating Point CSRs */
+mapping clause csr_name_map = 0x001  <-> "fflags"
+mapping clause csr_name_map = 0x002  <-> "frm"
+mapping clause csr_name_map = 0x003  <-> "fcsr"
 
 function clause is_CSR_defined (0x001) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
 function clause is_CSR_defined (0x002) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)

From ee9f214882efbf193715b4741f31580cfab6c5d4 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 14:11:03 -0700
Subject: [PATCH 02/17] Move HPM CSRs and other functions

---
 Makefile                     |   1 +
 model/riscv_csr_begin.sail   | 147 +-------------------------
 model/riscv_hpm_control.sail | 198 +++++++++++++++++++++++++++++++++++
 model/riscv_insts_zicsr.sail |  28 -----
 model/riscv_sys_control.sail |   8 --
 model/riscv_sys_regs.sail    |   4 -
 6 files changed, 200 insertions(+), 186 deletions(-)
 create mode 100644 model/riscv_hpm_control.sail

diff --git a/Makefile b/Makefile
index e97081e29..86de0204d 100644
--- a/Makefile
+++ b/Makefile
@@ -74,6 +74,7 @@ SAIL_SYS_SRCS =  riscv_csr_begin.sail       # Start of CSR scattered definitions
 SAIL_SYS_SRCS += riscv_vext_control.sail    # helpers for the 'V' extension
 SAIL_SYS_SRCS += riscv_sys_exceptions.sail  # default basic helpers for exception handling
 SAIL_SYS_SRCS += riscv_sync_exception.sail  # define the exception structure used in the model
+SAIL_SYS_SRCS += riscv_hpm_control.sail
 SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
 SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 
diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 24167bca7..1647a7437 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -21,68 +21,10 @@ mapping clause csr_name_map = 0x015  <-> "seed"
 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 = 0xC03  <-> "hpmcounter3"
-mapping clause csr_name_map = 0xC04  <-> "hpmcounter4"
-mapping clause csr_name_map = 0xC05  <-> "hpmcounter5"
-mapping clause csr_name_map = 0xC06  <-> "hpmcounter6"
-mapping clause csr_name_map = 0xC07  <-> "hpmcounter7"
-mapping clause csr_name_map = 0xC08  <-> "hpmcounter8"
-mapping clause csr_name_map = 0xC09  <-> "hpmcounter9"
-mapping clause csr_name_map = 0xC0A  <-> "hpmcounter10"
-mapping clause csr_name_map = 0xC0B  <-> "hpmcounter11"
-mapping clause csr_name_map = 0xC0C  <-> "hpmcounter12"
-mapping clause csr_name_map = 0xC0D  <-> "hpmcounter13"
-mapping clause csr_name_map = 0xC0E  <-> "hpmcounter14"
-mapping clause csr_name_map = 0xC0F  <-> "hpmcounter15"
-mapping clause csr_name_map = 0xC10  <-> "hpmcounter16"
-mapping clause csr_name_map = 0xC11  <-> "hpmcounter17"
-mapping clause csr_name_map = 0xC12  <-> "hpmcounter18"
-mapping clause csr_name_map = 0xC13  <-> "hpmcounter19"
-mapping clause csr_name_map = 0xC14  <-> "hpmcounter20"
-mapping clause csr_name_map = 0xC15  <-> "hpmcounter21"
-mapping clause csr_name_map = 0xC16  <-> "hpmcounter22"
-mapping clause csr_name_map = 0xC17  <-> "hpmcounter23"
-mapping clause csr_name_map = 0xC18  <-> "hpmcounter24"
-mapping clause csr_name_map = 0xC19  <-> "hpmcounter25"
-mapping clause csr_name_map = 0xC1A  <-> "hpmcounter26"
-mapping clause csr_name_map = 0xC1B  <-> "hpmcounter27"
-mapping clause csr_name_map = 0xC1C  <-> "hpmcounter28"
-mapping clause csr_name_map = 0xC1D  <-> "hpmcounter29"
-mapping clause csr_name_map = 0xC1E  <-> "hpmcounter30"
-mapping clause csr_name_map = 0xC1F  <-> "hpmcounter31"
 
 mapping clause csr_name_map = 0xC80  <-> "cycleh"
 mapping clause csr_name_map = 0xC81  <-> "timeh"
 mapping clause csr_name_map = 0xC82  <-> "instreth"
-mapping clause csr_name_map = 0xC83  <-> "hpmcounter3h"
-mapping clause csr_name_map = 0xC84  <-> "hpmcounter4h"
-mapping clause csr_name_map = 0xC85  <-> "hpmcounter5h"
-mapping clause csr_name_map = 0xC86  <-> "hpmcounter6h"
-mapping clause csr_name_map = 0xC87  <-> "hpmcounter7h"
-mapping clause csr_name_map = 0xC88  <-> "hpmcounter8h"
-mapping clause csr_name_map = 0xC89  <-> "hpmcounter9h"
-mapping clause csr_name_map = 0xC8A  <-> "hpmcounter10h"
-mapping clause csr_name_map = 0xC8B  <-> "hpmcounter11h"
-mapping clause csr_name_map = 0xC8C  <-> "hpmcounter12h"
-mapping clause csr_name_map = 0xC8D  <-> "hpmcounter13h"
-mapping clause csr_name_map = 0xC8E  <-> "hpmcounter14h"
-mapping clause csr_name_map = 0xC8F  <-> "hpmcounter15h"
-mapping clause csr_name_map = 0xC90  <-> "hpmcounter16h"
-mapping clause csr_name_map = 0xC91  <-> "hpmcounter17h"
-mapping clause csr_name_map = 0xC92  <-> "hpmcounter18h"
-mapping clause csr_name_map = 0xC93  <-> "hpmcounter19h"
-mapping clause csr_name_map = 0xC94  <-> "hpmcounter20h"
-mapping clause csr_name_map = 0xC95  <-> "hpmcounter21h"
-mapping clause csr_name_map = 0xC96  <-> "hpmcounter22h"
-mapping clause csr_name_map = 0xC97  <-> "hpmcounter23h"
-mapping clause csr_name_map = 0xC98  <-> "hpmcounter24h"
-mapping clause csr_name_map = 0xC99  <-> "hpmcounter25h"
-mapping clause csr_name_map = 0xC9A  <-> "hpmcounter26h"
-mapping clause csr_name_map = 0xC9B  <-> "hpmcounter27h"
-mapping clause csr_name_map = 0xC9C  <-> "hpmcounter28h"
-mapping clause csr_name_map = 0xC9D  <-> "hpmcounter29h"
-mapping clause csr_name_map = 0xC9E  <-> "hpmcounter30h"
-mapping clause csr_name_map = 0xC9F  <-> "hpmcounter31h"
 
 /* supervisor trap setup */
 mapping clause csr_name_map = 0x100  <-> "sstatus"
@@ -117,36 +59,6 @@ mapping clause csr_name_map = 0x320  <-> "mcountinhibit"
 /* machine envcfg */
 mapping clause csr_name_map = 0x30A  <-> "menvcfg"
 mapping clause csr_name_map = 0x31A  <-> "menvcfgh"
-/* hardware performance counter event selection */
-mapping clause csr_name_map = 0x323  <-> "mhpmevent3"
-mapping clause csr_name_map = 0x324  <-> "mhpmevent4"
-mapping clause csr_name_map = 0x325  <-> "mhpmevent5"
-mapping clause csr_name_map = 0x326  <-> "mhpmevent6"
-mapping clause csr_name_map = 0x327  <-> "mhpmevent7"
-mapping clause csr_name_map = 0x328  <-> "mhpmevent8"
-mapping clause csr_name_map = 0x329  <-> "mhpmevent9"
-mapping clause csr_name_map = 0x32A  <-> "mhpmevent10"
-mapping clause csr_name_map = 0x32B  <-> "mhpmevent11"
-mapping clause csr_name_map = 0x32C  <-> "mhpmevent12"
-mapping clause csr_name_map = 0x32D  <-> "mhpmevent13"
-mapping clause csr_name_map = 0x32E  <-> "mhpmevent14"
-mapping clause csr_name_map = 0x32F  <-> "mhpmevent15"
-mapping clause csr_name_map = 0x330  <-> "mhpmevent16"
-mapping clause csr_name_map = 0x331  <-> "mhpmevent17"
-mapping clause csr_name_map = 0x332  <-> "mhpmevent18"
-mapping clause csr_name_map = 0x333  <-> "mhpmevent19"
-mapping clause csr_name_map = 0x334  <-> "mhpmevent20"
-mapping clause csr_name_map = 0x335  <-> "mhpmevent21"
-mapping clause csr_name_map = 0x336  <-> "mhpmevent22"
-mapping clause csr_name_map = 0x337  <-> "mhpmevent23"
-mapping clause csr_name_map = 0x338  <-> "mhpmevent24"
-mapping clause csr_name_map = 0x339  <-> "mhpmevent25"
-mapping clause csr_name_map = 0x33A  <-> "mhpmevent26"
-mapping clause csr_name_map = 0x33B  <-> "mhpmevent27"
-mapping clause csr_name_map = 0x33C  <-> "mhpmevent28"
-mapping clause csr_name_map = 0x33D  <-> "mhpmevent29"
-mapping clause csr_name_map = 0x33E  <-> "mhpmevent30"
-mapping clause csr_name_map = 0x33F  <-> "mhpmevent31"
 /* machine trap handling */
 mapping clause csr_name_map = 0x340  <-> "mscratch"
 mapping clause csr_name_map = 0x341  <-> "mepc"
@@ -237,66 +149,9 @@ mapping clause csr_name_map = 0x3EF  <-> "pmpaddr63"
 /* machine counters/timers */
 mapping clause csr_name_map = 0xB00  <-> "mcycle"
 mapping clause csr_name_map = 0xB02  <-> "minstret"
-mapping clause csr_name_map = 0xB03  <-> "mhpmcounter3"
-mapping clause csr_name_map = 0xB04  <-> "mhpmcounter4"
-mapping clause csr_name_map = 0xB05  <-> "mhpmcounter5"
-mapping clause csr_name_map = 0xB06  <-> "mhpmcounter6"
-mapping clause csr_name_map = 0xB07  <-> "mhpmcounter7"
-mapping clause csr_name_map = 0xB08  <-> "mhpmcounter8"
-mapping clause csr_name_map = 0xB09  <-> "mhpmcounter9"
-mapping clause csr_name_map = 0xB0A  <-> "mhpmcounter10"
-mapping clause csr_name_map = 0xB0B  <-> "mhpmcounter11"
-mapping clause csr_name_map = 0xB0C  <-> "mhpmcounter12"
-mapping clause csr_name_map = 0xB0D  <-> "mhpmcounter13"
-mapping clause csr_name_map = 0xB0E  <-> "mhpmcounter14"
-mapping clause csr_name_map = 0xB0F  <-> "mhpmcounter15"
-mapping clause csr_name_map = 0xB10  <-> "mhpmcounter16"
-mapping clause csr_name_map = 0xB11  <-> "mhpmcounter17"
-mapping clause csr_name_map = 0xB12  <-> "mhpmcounter18"
-mapping clause csr_name_map = 0xB13  <-> "mhpmcounter19"
-mapping clause csr_name_map = 0xB14  <-> "mhpmcounter20"
-mapping clause csr_name_map = 0xB15  <-> "mhpmcounter21"
-mapping clause csr_name_map = 0xB16  <-> "mhpmcounter22"
-mapping clause csr_name_map = 0xB17  <-> "mhpmcounter23"
-mapping clause csr_name_map = 0xB18  <-> "mhpmcounter24"
-mapping clause csr_name_map = 0xB19  <-> "mhpmcounter25"
-mapping clause csr_name_map = 0xB1A  <-> "mhpmcounter26"
-mapping clause csr_name_map = 0xB1B  <-> "mhpmcounter27"
-mapping clause csr_name_map = 0xB1C  <-> "mhpmcounter28"
-mapping clause csr_name_map = 0xB1D  <-> "mhpmcounter29"
-mapping clause csr_name_map = 0xB1E  <-> "mhpmcounter30"
-mapping clause csr_name_map = 0xB1F  <-> "mhpmcounter31"
+
 mapping clause csr_name_map = 0xB80  <-> "mcycleh"
 mapping clause csr_name_map = 0xB82  <-> "minstreth"
-mapping clause csr_name_map = 0xB83  <-> "mhpmcounter3h"
-mapping clause csr_name_map = 0xB84  <-> "mhpmcounter4h"
-mapping clause csr_name_map = 0xB85  <-> "mhpmcounter5h"
-mapping clause csr_name_map = 0xB86  <-> "mhpmcounter6h"
-mapping clause csr_name_map = 0xB87  <-> "mhpmcounter7h"
-mapping clause csr_name_map = 0xB88  <-> "mhpmcounter8h"
-mapping clause csr_name_map = 0xB89  <-> "mhpmcounter9h"
-mapping clause csr_name_map = 0xB8A  <-> "mhpmcounter10h"
-mapping clause csr_name_map = 0xB8B  <-> "mhpmcounter11h"
-mapping clause csr_name_map = 0xB8C  <-> "mhpmcounter12h"
-mapping clause csr_name_map = 0xB8D  <-> "mhpmcounter13h"
-mapping clause csr_name_map = 0xB8E  <-> "mhpmcounter14h"
-mapping clause csr_name_map = 0xB8F  <-> "mhpmcounter15h"
-mapping clause csr_name_map = 0xB90  <-> "mhpmcounter16h"
-mapping clause csr_name_map = 0xB91  <-> "mhpmcounter17h"
-mapping clause csr_name_map = 0xB92  <-> "mhpmcounter18h"
-mapping clause csr_name_map = 0xB93  <-> "mhpmcounter19h"
-mapping clause csr_name_map = 0xB94  <-> "mhpmcounter20h"
-mapping clause csr_name_map = 0xB95  <-> "mhpmcounter21h"
-mapping clause csr_name_map = 0xB96  <-> "mhpmcounter22h"
-mapping clause csr_name_map = 0xB97  <-> "mhpmcounter23h"
-mapping clause csr_name_map = 0xB98  <-> "mhpmcounter24h"
-mapping clause csr_name_map = 0xB99  <-> "mhpmcounter25h"
-mapping clause csr_name_map = 0xB9A  <-> "mhpmcounter26h"
-mapping clause csr_name_map = 0xB9B  <-> "mhpmcounter27h"
-mapping clause csr_name_map = 0xB9C  <-> "mhpmcounter28h"
-mapping clause csr_name_map = 0xB9D  <-> "mhpmcounter29h"
-mapping clause csr_name_map = 0xB9E  <-> "mhpmcounter30h"
-mapping clause csr_name_map = 0xB9F  <-> "mhpmcounter31h"
 /* trigger/debug */
 mapping clause csr_name_map = 0x7a0  <-> "tselect"
 mapping clause csr_name_map = 0x7a1  <-> "tdata1"
diff --git a/model/riscv_hpm_control.sail b/model/riscv_hpm_control.sail
new file mode 100644
index 000000000..578d39869
--- /dev/null
+++ b/model/riscv_hpm_control.sail
@@ -0,0 +1,198 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* Hardware Performance Monitoring counters */
+enum clause extension = Ext_Zihpm
+function clause extensionEnabled(Ext_Zihpm) = true
+
+/* Hardware performance monitoring counters */
+mapping clause csr_name_map = 0xC03  <-> "hpmcounter3"
+mapping clause csr_name_map = 0xC04  <-> "hpmcounter4"
+mapping clause csr_name_map = 0xC05  <-> "hpmcounter5"
+mapping clause csr_name_map = 0xC06  <-> "hpmcounter6"
+mapping clause csr_name_map = 0xC07  <-> "hpmcounter7"
+mapping clause csr_name_map = 0xC08  <-> "hpmcounter8"
+mapping clause csr_name_map = 0xC09  <-> "hpmcounter9"
+mapping clause csr_name_map = 0xC0A  <-> "hpmcounter10"
+mapping clause csr_name_map = 0xC0B  <-> "hpmcounter11"
+mapping clause csr_name_map = 0xC0C  <-> "hpmcounter12"
+mapping clause csr_name_map = 0xC0D  <-> "hpmcounter13"
+mapping clause csr_name_map = 0xC0E  <-> "hpmcounter14"
+mapping clause csr_name_map = 0xC0F  <-> "hpmcounter15"
+mapping clause csr_name_map = 0xC10  <-> "hpmcounter16"
+mapping clause csr_name_map = 0xC11  <-> "hpmcounter17"
+mapping clause csr_name_map = 0xC12  <-> "hpmcounter18"
+mapping clause csr_name_map = 0xC13  <-> "hpmcounter19"
+mapping clause csr_name_map = 0xC14  <-> "hpmcounter20"
+mapping clause csr_name_map = 0xC15  <-> "hpmcounter21"
+mapping clause csr_name_map = 0xC16  <-> "hpmcounter22"
+mapping clause csr_name_map = 0xC17  <-> "hpmcounter23"
+mapping clause csr_name_map = 0xC18  <-> "hpmcounter24"
+mapping clause csr_name_map = 0xC19  <-> "hpmcounter25"
+mapping clause csr_name_map = 0xC1A  <-> "hpmcounter26"
+mapping clause csr_name_map = 0xC1B  <-> "hpmcounter27"
+mapping clause csr_name_map = 0xC1C  <-> "hpmcounter28"
+mapping clause csr_name_map = 0xC1D  <-> "hpmcounter29"
+mapping clause csr_name_map = 0xC1E  <-> "hpmcounter30"
+mapping clause csr_name_map = 0xC1F  <-> "hpmcounter31"
+
+mapping clause csr_name_map = 0xC83  <-> "hpmcounter3h"
+mapping clause csr_name_map = 0xC84  <-> "hpmcounter4h"
+mapping clause csr_name_map = 0xC85  <-> "hpmcounter5h"
+mapping clause csr_name_map = 0xC86  <-> "hpmcounter6h"
+mapping clause csr_name_map = 0xC87  <-> "hpmcounter7h"
+mapping clause csr_name_map = 0xC88  <-> "hpmcounter8h"
+mapping clause csr_name_map = 0xC89  <-> "hpmcounter9h"
+mapping clause csr_name_map = 0xC8A  <-> "hpmcounter10h"
+mapping clause csr_name_map = 0xC8B  <-> "hpmcounter11h"
+mapping clause csr_name_map = 0xC8C  <-> "hpmcounter12h"
+mapping clause csr_name_map = 0xC8D  <-> "hpmcounter13h"
+mapping clause csr_name_map = 0xC8E  <-> "hpmcounter14h"
+mapping clause csr_name_map = 0xC8F  <-> "hpmcounter15h"
+mapping clause csr_name_map = 0xC90  <-> "hpmcounter16h"
+mapping clause csr_name_map = 0xC91  <-> "hpmcounter17h"
+mapping clause csr_name_map = 0xC92  <-> "hpmcounter18h"
+mapping clause csr_name_map = 0xC93  <-> "hpmcounter19h"
+mapping clause csr_name_map = 0xC94  <-> "hpmcounter20h"
+mapping clause csr_name_map = 0xC95  <-> "hpmcounter21h"
+mapping clause csr_name_map = 0xC96  <-> "hpmcounter22h"
+mapping clause csr_name_map = 0xC97  <-> "hpmcounter23h"
+mapping clause csr_name_map = 0xC98  <-> "hpmcounter24h"
+mapping clause csr_name_map = 0xC99  <-> "hpmcounter25h"
+mapping clause csr_name_map = 0xC9A  <-> "hpmcounter26h"
+mapping clause csr_name_map = 0xC9B  <-> "hpmcounter27h"
+mapping clause csr_name_map = 0xC9C  <-> "hpmcounter28h"
+mapping clause csr_name_map = 0xC9D  <-> "hpmcounter29h"
+mapping clause csr_name_map = 0xC9E  <-> "hpmcounter30h"
+mapping clause csr_name_map = 0xC9F  <-> "hpmcounter31h"
+
+/* hardware performance counter event selection */
+mapping clause csr_name_map = 0x323  <-> "mhpmevent3"
+mapping clause csr_name_map = 0x324  <-> "mhpmevent4"
+mapping clause csr_name_map = 0x325  <-> "mhpmevent5"
+mapping clause csr_name_map = 0x326  <-> "mhpmevent6"
+mapping clause csr_name_map = 0x327  <-> "mhpmevent7"
+mapping clause csr_name_map = 0x328  <-> "mhpmevent8"
+mapping clause csr_name_map = 0x329  <-> "mhpmevent9"
+mapping clause csr_name_map = 0x32A  <-> "mhpmevent10"
+mapping clause csr_name_map = 0x32B  <-> "mhpmevent11"
+mapping clause csr_name_map = 0x32C  <-> "mhpmevent12"
+mapping clause csr_name_map = 0x32D  <-> "mhpmevent13"
+mapping clause csr_name_map = 0x32E  <-> "mhpmevent14"
+mapping clause csr_name_map = 0x32F  <-> "mhpmevent15"
+mapping clause csr_name_map = 0x330  <-> "mhpmevent16"
+mapping clause csr_name_map = 0x331  <-> "mhpmevent17"
+mapping clause csr_name_map = 0x332  <-> "mhpmevent18"
+mapping clause csr_name_map = 0x333  <-> "mhpmevent19"
+mapping clause csr_name_map = 0x334  <-> "mhpmevent20"
+mapping clause csr_name_map = 0x335  <-> "mhpmevent21"
+mapping clause csr_name_map = 0x336  <-> "mhpmevent22"
+mapping clause csr_name_map = 0x337  <-> "mhpmevent23"
+mapping clause csr_name_map = 0x338  <-> "mhpmevent24"
+mapping clause csr_name_map = 0x339  <-> "mhpmevent25"
+mapping clause csr_name_map = 0x33A  <-> "mhpmevent26"
+mapping clause csr_name_map = 0x33B  <-> "mhpmevent27"
+mapping clause csr_name_map = 0x33C  <-> "mhpmevent28"
+mapping clause csr_name_map = 0x33D  <-> "mhpmevent29"
+mapping clause csr_name_map = 0x33E  <-> "mhpmevent30"
+mapping clause csr_name_map = 0x33F  <-> "mhpmevent31"
+
+/* machine hardware performance counters */
+mapping clause csr_name_map = 0xB03  <-> "mhpmcounter3"
+mapping clause csr_name_map = 0xB04  <-> "mhpmcounter4"
+mapping clause csr_name_map = 0xB05  <-> "mhpmcounter5"
+mapping clause csr_name_map = 0xB06  <-> "mhpmcounter6"
+mapping clause csr_name_map = 0xB07  <-> "mhpmcounter7"
+mapping clause csr_name_map = 0xB08  <-> "mhpmcounter8"
+mapping clause csr_name_map = 0xB09  <-> "mhpmcounter9"
+mapping clause csr_name_map = 0xB0A  <-> "mhpmcounter10"
+mapping clause csr_name_map = 0xB0B  <-> "mhpmcounter11"
+mapping clause csr_name_map = 0xB0C  <-> "mhpmcounter12"
+mapping clause csr_name_map = 0xB0D  <-> "mhpmcounter13"
+mapping clause csr_name_map = 0xB0E  <-> "mhpmcounter14"
+mapping clause csr_name_map = 0xB0F  <-> "mhpmcounter15"
+mapping clause csr_name_map = 0xB10  <-> "mhpmcounter16"
+mapping clause csr_name_map = 0xB11  <-> "mhpmcounter17"
+mapping clause csr_name_map = 0xB12  <-> "mhpmcounter18"
+mapping clause csr_name_map = 0xB13  <-> "mhpmcounter19"
+mapping clause csr_name_map = 0xB14  <-> "mhpmcounter20"
+mapping clause csr_name_map = 0xB15  <-> "mhpmcounter21"
+mapping clause csr_name_map = 0xB16  <-> "mhpmcounter22"
+mapping clause csr_name_map = 0xB17  <-> "mhpmcounter23"
+mapping clause csr_name_map = 0xB18  <-> "mhpmcounter24"
+mapping clause csr_name_map = 0xB19  <-> "mhpmcounter25"
+mapping clause csr_name_map = 0xB1A  <-> "mhpmcounter26"
+mapping clause csr_name_map = 0xB1B  <-> "mhpmcounter27"
+mapping clause csr_name_map = 0xB1C  <-> "mhpmcounter28"
+mapping clause csr_name_map = 0xB1D  <-> "mhpmcounter29"
+mapping clause csr_name_map = 0xB1E  <-> "mhpmcounter30"
+mapping clause csr_name_map = 0xB1F  <-> "mhpmcounter31"
+
+mapping clause csr_name_map = 0xB83  <-> "mhpmcounter3h"
+mapping clause csr_name_map = 0xB84  <-> "mhpmcounter4h"
+mapping clause csr_name_map = 0xB85  <-> "mhpmcounter5h"
+mapping clause csr_name_map = 0xB86  <-> "mhpmcounter6h"
+mapping clause csr_name_map = 0xB87  <-> "mhpmcounter7h"
+mapping clause csr_name_map = 0xB88  <-> "mhpmcounter8h"
+mapping clause csr_name_map = 0xB89  <-> "mhpmcounter9h"
+mapping clause csr_name_map = 0xB8A  <-> "mhpmcounter10h"
+mapping clause csr_name_map = 0xB8B  <-> "mhpmcounter11h"
+mapping clause csr_name_map = 0xB8C  <-> "mhpmcounter12h"
+mapping clause csr_name_map = 0xB8D  <-> "mhpmcounter13h"
+mapping clause csr_name_map = 0xB8E  <-> "mhpmcounter14h"
+mapping clause csr_name_map = 0xB8F  <-> "mhpmcounter15h"
+mapping clause csr_name_map = 0xB90  <-> "mhpmcounter16h"
+mapping clause csr_name_map = 0xB91  <-> "mhpmcounter17h"
+mapping clause csr_name_map = 0xB92  <-> "mhpmcounter18h"
+mapping clause csr_name_map = 0xB93  <-> "mhpmcounter19h"
+mapping clause csr_name_map = 0xB94  <-> "mhpmcounter20h"
+mapping clause csr_name_map = 0xB95  <-> "mhpmcounter21h"
+mapping clause csr_name_map = 0xB96  <-> "mhpmcounter22h"
+mapping clause csr_name_map = 0xB97  <-> "mhpmcounter23h"
+mapping clause csr_name_map = 0xB98  <-> "mhpmcounter24h"
+mapping clause csr_name_map = 0xB99  <-> "mhpmcounter25h"
+mapping clause csr_name_map = 0xB9A  <-> "mhpmcounter26h"
+mapping clause csr_name_map = 0xB9B  <-> "mhpmcounter27h"
+mapping clause csr_name_map = 0xB9C  <-> "mhpmcounter28h"
+mapping clause csr_name_map = 0xB9D  <-> "mhpmcounter29h"
+mapping clause csr_name_map = 0xB9E  <-> "mhpmcounter30h"
+mapping clause csr_name_map = 0xB9F  <-> "mhpmcounter31h"
+
+/* Hardware Performance Monitoring event selection */
+function clause is_CSR_defined(0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) // mhpmevent3..31
+function clause read_CSR(0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmevent(hpmidx_from_bits(index))
+function clause write_CSR((0b0011001 /* 0x320 */ @ index : bits(5), value) if unsigned(index) >= 3) = {
+  let index = hpmidx_from_bits(index);
+  write_mhpmevent(index, value);
+  read_mhpmevent(index)
+}
+
+/* Hardware Performance Monitoring machine mode counters */
+function clause is_CSR_defined(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) // mhpmcounter3..31
+function clause is_CSR_defined(0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & (xlen == 32) // mhpmcounterh3..31
+
+function clause read_CSR(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index))
+function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index))
+
+function clause write_CSR((0b1011000 /* 0xB00 */ @ index : bits(5), value) if unsigned(index) >= 3) = {
+  let index = hpmidx_from_bits(index);
+  write_mhpmcounter(index, value);
+  read_mhpmcounter(index)
+}
+function clause write_CSR((0b1011100 /* 0xB80 */ @ index : bits(5), value) if xlen == 32 & unsigned(index) >= 3) = {
+  let index = hpmidx_from_bits(index);
+  write_mhpmcounterh(index, value);
+  read_mhpmcounterh(index)
+}
+
+/* Hardware Performance Monitoring user mode counters */
+function clause is_CSR_defined(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) // hpmcounter3..31
+function clause is_CSR_defined(0b1100100 /* 0xC80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) & (xlen == 32) // hpmcounterh3..31
+
+function clause read_CSR(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index))
+function clause read_CSR(0b1100100 /* 0xC80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index))
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 5e4d47b9e..e7b62ecb9 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -42,9 +42,6 @@ function clause read_CSR(0x310 if xlen == 32) = mstatush.bits
 function clause read_CSR(0x31A if xlen == 32) = menvcfg.bits[63 .. 32]
 function clause read_CSR(0x320) = zero_extend(mcountinhibit.bits)
 
-/* Hardware Performance Monitoring event selection */
-function clause read_CSR(0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmevent(hpmidx_from_bits(index))
-
 function clause read_CSR(0x340) = mscratch
 function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
 function clause read_CSR(0x342) = mcause.bits
@@ -65,10 +62,6 @@ function clause read_CSR(0xB02) = minstret[(xlen - 1) .. 0]
 function clause read_CSR(0xB80 if xlen == 32)= mcycle[63 .. 32]
 function clause read_CSR(0xB82 if xlen == 32) = minstret[63 .. 32]
 
-/* Hardware Performance Monitoring machine mode counters */
-function clause read_CSR(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index))
-function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index))
-
 /* trigger/debug */
 function clause read_CSR(0x7a0) = ~(tselect)  /* this indicates we don't have any trigger support */
 
@@ -93,10 +86,6 @@ function clause read_CSR(0xC80 if xlen == 32) = mcycle[63 .. 32]
 function clause read_CSR(0xC81 if xlen == 32) = mtime[63 .. 32]
 function clause read_CSR(0xC82 if xlen == 32) = minstret[63 .. 32]
 
-/* Hardware Performance Monitoring user mode counters */
-function clause read_CSR(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index))
-function clause read_CSR(0b1100100 /* 0xC80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index))
-
 /* user mode: Zkr */
 function clause read_CSR(0x015) = read_seed_csr()
 
@@ -138,23 +127,6 @@ function clause write_CSR(0xB02, value) = { minstret[(xlen - 1) .. 0] = value; m
 function clause write_CSR((0xB80, value) if xlen == 32) = { mcycle[63 .. 32] = value; value }
 function clause write_CSR((0xB82, value) if xlen == 32) = { minstret[63 .. 32] = value; minstret_increment = false; value }
 
-/* Hardware Performance Monitoring machine mode counters */
-function clause write_CSR((0b0011001 /* 0x320 */ @ index : bits(5), value) if unsigned(index) >= 3) = {
-  let index = hpmidx_from_bits(index);
-  write_mhpmevent(index, value);
-  read_mhpmevent(index)
-}
-function clause write_CSR((0b1011000 /* 0xB00 */ @ index : bits(5), value) if unsigned(index) >= 3) = {
-  let index = hpmidx_from_bits(index);
-  write_mhpmcounter(index, value);
-  read_mhpmcounter(index)
-}
-function clause write_CSR((0b1011100 /* 0xB80 */ @ index : bits(5), value) if xlen == 32 & unsigned(index) >= 3) = {
-  let index = hpmidx_from_bits(index);
-  write_mhpmcounterh(index, value);
-  read_mhpmcounterh(index)
-}
-
 /* trigger/debug */
 function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
 
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 6379f5676..9e1122d47 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -56,18 +56,13 @@ function clause is_CSR_defined(0x3D) @ idx : bits(4) = sys_pmp_count() > unsigne
 function clause is_CSR_defined(0x3E) @ idx : bits(4) = sys_pmp_count() > unsigned(0b11 @ idx)
 
 /* counters */
-function clause is_CSR_defined(0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) // mhpmevent3..31
 
 function clause is_CSR_defined(0xB00) = true // mcycle
 function clause is_CSR_defined(0xB02) = true // minstret
 
-function clause is_CSR_defined(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) // mhpmcounter3..31
-
 function clause is_CSR_defined(0xB80) = xlen == 32 // mcycleh
 function clause is_CSR_defined(0xB82) = xlen == 32 // minstreth
 
-function clause is_CSR_defined(0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & (xlen == 32) // mhpmcounterh3..31
-
 /* disabled trigger/debug module */
 function clause is_CSR_defined(0x7a0) = true
 
@@ -93,14 +88,11 @@ function clause is_CSR_defined(0xC00) = extensionEnabled(Ext_U) // cycle
 function clause is_CSR_defined(0xC01) = extensionEnabled(Ext_U) // time
 function clause is_CSR_defined(0xC02) = extensionEnabled(Ext_U) // instret
 
-function clause is_CSR_defined(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) // hpmcounter3..31
 
 function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (xlen == 32) // cycleh
 function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (xlen == 32) // timeh
 function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (xlen == 32) // instreth
 
-function clause is_CSR_defined(0b1100100 /* 0xC80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) & (xlen == 32) // hpmcounterh3..31
-
 /* user mode: Zkr */
 function clause is_CSR_defined(0x015) = extensionEnabled(Ext_Zkr)
 
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 4e810d762..51a6e5687 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -142,10 +142,6 @@ function clause extensionEnabled(Ext_U) = misa[U] == 0b1
 enum clause extension = Ext_S
 function clause extensionEnabled(Ext_S) = misa[S] == 0b1
 
-/* Hardware Performance Monitoring counters */
-enum clause extension = Ext_Zihpm
-function clause extensionEnabled(Ext_Zihpm) = true
-
 /*
  * Illegal values legalized to least privileged mode supported.
  * Note: the only valid combinations of supported modes are M, M+U, M+S+U.

From 53f95eba116c715a23338470822f0180a7fa97e8 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 14:31:51 -0700
Subject: [PATCH 03/17] Move machine info CSRs

---
 Makefile                     |  4 ++--
 model/riscv_csr_begin.sail   |  6 ------
 model/riscv_insts_zicsr.sail |  5 -----
 model/riscv_sys_control.sail |  6 ------
 model/riscv_sys_regs.sail    | 20 +++++++++++++++++++-
 5 files changed, 21 insertions(+), 20 deletions(-)

diff --git a/Makefile b/Makefile
index 86de0204d..267553eb1 100644
--- a/Makefile
+++ b/Makefile
@@ -70,7 +70,6 @@ SAIL_SEQ_INST_SRCS  = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sa
 SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.sail riscv_csr_end.sail
 
 # System and platform sources
-SAIL_SYS_SRCS =  riscv_csr_begin.sail       # Start of CSR scattered definitions.
 SAIL_SYS_SRCS += riscv_vext_control.sail    # helpers for the 'V' extension
 SAIL_SYS_SRCS += riscv_sys_exceptions.sail  # default basic helpers for exception handling
 SAIL_SYS_SRCS += riscv_sync_exception.sail  # define the exception structure used in the model
@@ -97,7 +96,8 @@ SAIL_VM_SRCS += riscv_vmem.sail
 # Non-instruction sources
 PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
 
-SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
+SAIL_REGS_SRCS =  riscv_csr_begin.sail       # Start of CSR scattered definitions.
+SAIL_REGS_SRCS += riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
 SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
 SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS)
 SAIL_REGS_SRCS += riscv_vreg_type.sail riscv_vext_regs.sail
diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 1647a7437..0ac0344f0 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -41,12 +41,6 @@ mapping clause csr_name_map = 0x144  <-> "sip"
 mapping clause csr_name_map = 0x180  <-> "satp"
 /* supervisor envcfg */
 mapping clause csr_name_map = 0x10A  <-> "senvcfg"
-/* 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"
-mapping clause csr_name_map = 0xF15  <-> "mconfigptr"
 /* machine trap setup */
 mapping clause csr_name_map = 0x300  <-> "mstatus"
 mapping clause csr_name_map = 0x301  <-> "misa"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index e7b62ecb9..18d0c407e 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -25,11 +25,6 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
 // corresponding to their extensions rather than all be here.
 
 /* machine mode */
-function clause read_CSR(0xF11) = zero_extend(mvendorid)
-function clause read_CSR(0xF12) = marchid
-function clause read_CSR(0xF13) = mimpid
-function clause read_CSR(0xF14) = mhartid
-function clause read_CSR(0xF15) = mconfigptr
 function clause read_CSR(0x300) = mstatus.bits
 function clause read_CSR(0x301) = misa.bits
 function clause read_CSR(0x302) = medeleg.bits
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 9e1122d47..72246e8c7 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -19,12 +19,6 @@ function csrPriv(csr : csreg) -> priv_level = csr[9..8]
 // TODO: These is_CSR_defined definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* machine mode: informational */
-function clause is_CSR_defined(0xf11) = true // mvendorid
-function clause is_CSR_defined(0xf12) = true // marchdid
-function clause is_CSR_defined(0xf13) = true // mimpid
-function clause is_CSR_defined(0xf14) = true // mhartid
-function clause is_CSR_defined(0xf15) = true // mconfigptr
 /* machine mode: trap setup */
 function clause is_CSR_defined(0x300) = true // mstatus
 function clause is_CSR_defined(0x301) = true // misa
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 51a6e5687..e02c2b4b5 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -505,7 +505,7 @@ function write_mhpmcounterh(index : hpmidx, value : bits(32)) -> unit =
 function write_mhpmevent(index : hpmidx, value : xlenbits) -> unit =
   if sys_writable_hpm_counters()[index] == bitone then mhpmevent[index] = value
 
-/* informational registers */
+/* machine information registers */
 register mvendorid : bits(32)
 register mimpid : xlenbits
 register marchid : xlenbits
@@ -513,6 +513,24 @@ register marchid : xlenbits
 register mhartid : xlenbits
 register mconfigptr : xlenbits
 
+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"
+mapping clause csr_name_map = 0xF15  <-> "mconfigptr"
+
+function clause is_CSR_defined(0xf11) = true // mvendorid
+function clause is_CSR_defined(0xf12) = true // marchdid
+function clause is_CSR_defined(0xf13) = true // mimpid
+function clause is_CSR_defined(0xf14) = true // mhartid
+function clause is_CSR_defined(0xf15) = true // mconfigptr
+
+function clause read_CSR(0xF11) = zero_extend(mvendorid)
+function clause read_CSR(0xF12) = marchid
+function clause read_CSR(0xF13) = mimpid
+function clause read_CSR(0xF14) = mhartid
+function clause read_CSR(0xF15) = mconfigptr
+
 /* S-mode registers */
 
 /* sstatus reveals a subset of mstatus */

From b1cb9a419a0235654636cf4d378e7a0fd0b836c0 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 14:36:31 -0700
Subject: [PATCH 04/17] Move PMP CSRs

---
 model/riscv_csr_begin.sail   |  81 --------------------------
 model/riscv_insts_zicsr.sail |  21 -------
 model/riscv_pmp_regs.sail    | 108 +++++++++++++++++++++++++++++++++++
 model/riscv_sys_control.sail |   9 ---
 4 files changed, 108 insertions(+), 111 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 0ac0344f0..e252caa4e 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -59,87 +59,6 @@ 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 = 0x3A4  <-> "pmpcfg4"
-mapping clause csr_name_map = 0x3A5  <-> "pmpcfg5"
-mapping clause csr_name_map = 0x3A6  <-> "pmpcfg6"
-mapping clause csr_name_map = 0x3A7  <-> "pmpcfg7"
-mapping clause csr_name_map = 0x3A8  <-> "pmpcfg8"
-mapping clause csr_name_map = 0x3A9  <-> "pmpcfg9"
-mapping clause csr_name_map = 0x3AA  <-> "pmpcfg10"
-mapping clause csr_name_map = 0x3AB  <-> "pmpcfg11"
-mapping clause csr_name_map = 0x3AC  <-> "pmpcfg12"
-mapping clause csr_name_map = 0x3AD  <-> "pmpcfg13"
-mapping clause csr_name_map = 0x3AE  <-> "pmpcfg14"
-mapping clause csr_name_map = 0x3AF  <-> "pmpcfg15"
-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"
-mapping clause csr_name_map = 0x3C0  <-> "pmpaddr16"
-mapping clause csr_name_map = 0x3C1  <-> "pmpaddr17"
-mapping clause csr_name_map = 0x3C2  <-> "pmpaddr18"
-mapping clause csr_name_map = 0x3C3  <-> "pmpaddr19"
-mapping clause csr_name_map = 0x3C4  <-> "pmpaddr20"
-mapping clause csr_name_map = 0x3C5  <-> "pmpaddr21"
-mapping clause csr_name_map = 0x3C6  <-> "pmpaddr22"
-mapping clause csr_name_map = 0x3C7  <-> "pmpaddr23"
-mapping clause csr_name_map = 0x3C8  <-> "pmpaddr24"
-mapping clause csr_name_map = 0x3C9  <-> "pmpaddr25"
-mapping clause csr_name_map = 0x3CA  <-> "pmpaddr26"
-mapping clause csr_name_map = 0x3CB  <-> "pmpaddr27"
-mapping clause csr_name_map = 0x3CC  <-> "pmpaddr28"
-mapping clause csr_name_map = 0x3CD  <-> "pmpaddr29"
-mapping clause csr_name_map = 0x3CE  <-> "pmpaddr30"
-mapping clause csr_name_map = 0x3CF  <-> "pmpaddr31"
-mapping clause csr_name_map = 0x3D0  <-> "pmpaddr32"
-mapping clause csr_name_map = 0x3D1  <-> "pmpaddr33"
-mapping clause csr_name_map = 0x3D2  <-> "pmpaddr34"
-mapping clause csr_name_map = 0x3D3  <-> "pmpaddr35"
-mapping clause csr_name_map = 0x3D4  <-> "pmpaddr36"
-mapping clause csr_name_map = 0x3D5  <-> "pmpaddr37"
-mapping clause csr_name_map = 0x3D6  <-> "pmpaddr38"
-mapping clause csr_name_map = 0x3D7  <-> "pmpaddr39"
-mapping clause csr_name_map = 0x3D8  <-> "pmpaddr40"
-mapping clause csr_name_map = 0x3D9  <-> "pmpaddr41"
-mapping clause csr_name_map = 0x3DA  <-> "pmpaddr42"
-mapping clause csr_name_map = 0x3DB  <-> "pmpaddr43"
-mapping clause csr_name_map = 0x3DC  <-> "pmpaddr44"
-mapping clause csr_name_map = 0x3DD  <-> "pmpaddr45"
-mapping clause csr_name_map = 0x3DE  <-> "pmpaddr46"
-mapping clause csr_name_map = 0x3DF  <-> "pmpaddr47"
-mapping clause csr_name_map = 0x3E0  <-> "pmpaddr48"
-mapping clause csr_name_map = 0x3E1  <-> "pmpaddr49"
-mapping clause csr_name_map = 0x3E2  <-> "pmpaddr50"
-mapping clause csr_name_map = 0x3E3  <-> "pmpaddr51"
-mapping clause csr_name_map = 0x3E4  <-> "pmpaddr52"
-mapping clause csr_name_map = 0x3E5  <-> "pmpaddr53"
-mapping clause csr_name_map = 0x3E6  <-> "pmpaddr54"
-mapping clause csr_name_map = 0x3E7  <-> "pmpaddr55"
-mapping clause csr_name_map = 0x3E8  <-> "pmpaddr56"
-mapping clause csr_name_map = 0x3E9  <-> "pmpaddr57"
-mapping clause csr_name_map = 0x3EA  <-> "pmpaddr58"
-mapping clause csr_name_map = 0x3EB  <-> "pmpaddr59"
-mapping clause csr_name_map = 0x3EC  <-> "pmpaddr60"
-mapping clause csr_name_map = 0x3ED  <-> "pmpaddr61"
-mapping clause csr_name_map = 0x3EE  <-> "pmpaddr62"
-mapping clause csr_name_map = 0x3EF  <-> "pmpaddr63"
 /* machine counters/timers */
 mapping clause csr_name_map = 0xB00  <-> "mcycle"
 mapping clause csr_name_map = 0xB02  <-> "minstret"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 18d0c407e..ee4e52e3e 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -43,14 +43,6 @@ function clause read_CSR(0x342) = mcause.bits
 function clause read_CSR(0x343) = mtval
 function clause read_CSR(0x344) = mip.bits
 
-// pmpcfgN
-function clause read_CSR(0x3A @ idx : bits(4) if idx[0] == bitzero | xlen == 32) = pmpReadCfgReg(unsigned(idx))
-// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
-function clause read_CSR(0x3B @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b00 @ idx))
-function clause read_CSR(0x3C @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b01 @ idx))
-function clause read_CSR(0x3D @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b10 @ idx))
-function clause read_CSR(0x3E @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b11 @ idx))
-
 /* machine mode counters */
 function clause read_CSR(0xB00) = mcycle[(xlen - 1) .. 0]
 function clause read_CSR(0xB02) = minstret[(xlen - 1) .. 0]
@@ -103,19 +95,6 @@ function clause write_CSR(0x342, value) = { mcause.bits = value; mcause.bits }
 function clause write_CSR(0x343, value) = { mtval = value; mtval }
 function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.bits }
 
-// pmpcfgN
-function clause write_CSR((0x3A @ idx : bits(4), value) if idx[0] == bitzero | xlen == 32) = {
-  let idx = unsigned(idx);
-  pmpWriteCfgReg(idx, value);
-  pmpReadCfgReg(idx)
-}
-
-// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
-function clause write_CSR(0x3B @ idx : bits(4), value) = { let idx = unsigned(0b00 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
-function clause write_CSR(0x3C @ idx : bits(4), value) = { let idx = unsigned(0b01 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
-function clause write_CSR(0x3D @ idx : bits(4), value) = { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
-function clause write_CSR(0x3E @ idx : bits(4), value) = { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
-
 /* machine mode counters */
 function clause write_CSR(0xB00, value) = { mcycle[(xlen - 1) .. 0] = value; value }
 function clause write_CSR(0xB02, value) = { minstret[(xlen - 1) .. 0] = value; minstret_increment = false; value }
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index 3764f3533..0eacf8cbf 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -146,3 +146,111 @@ function pmpWriteAddrReg(n : range(0, 63), v : xlenbits) -> unit = {
     v,
   );
 }
+
+/* PMP CSRs */
+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 = 0x3A4  <-> "pmpcfg4"
+mapping clause csr_name_map = 0x3A5  <-> "pmpcfg5"
+mapping clause csr_name_map = 0x3A6  <-> "pmpcfg6"
+mapping clause csr_name_map = 0x3A7  <-> "pmpcfg7"
+mapping clause csr_name_map = 0x3A8  <-> "pmpcfg8"
+mapping clause csr_name_map = 0x3A9  <-> "pmpcfg9"
+mapping clause csr_name_map = 0x3AA  <-> "pmpcfg10"
+mapping clause csr_name_map = 0x3AB  <-> "pmpcfg11"
+mapping clause csr_name_map = 0x3AC  <-> "pmpcfg12"
+mapping clause csr_name_map = 0x3AD  <-> "pmpcfg13"
+mapping clause csr_name_map = 0x3AE  <-> "pmpcfg14"
+mapping clause csr_name_map = 0x3AF  <-> "pmpcfg15"
+
+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"
+mapping clause csr_name_map = 0x3C0  <-> "pmpaddr16"
+mapping clause csr_name_map = 0x3C1  <-> "pmpaddr17"
+mapping clause csr_name_map = 0x3C2  <-> "pmpaddr18"
+mapping clause csr_name_map = 0x3C3  <-> "pmpaddr19"
+mapping clause csr_name_map = 0x3C4  <-> "pmpaddr20"
+mapping clause csr_name_map = 0x3C5  <-> "pmpaddr21"
+mapping clause csr_name_map = 0x3C6  <-> "pmpaddr22"
+mapping clause csr_name_map = 0x3C7  <-> "pmpaddr23"
+mapping clause csr_name_map = 0x3C8  <-> "pmpaddr24"
+mapping clause csr_name_map = 0x3C9  <-> "pmpaddr25"
+mapping clause csr_name_map = 0x3CA  <-> "pmpaddr26"
+mapping clause csr_name_map = 0x3CB  <-> "pmpaddr27"
+mapping clause csr_name_map = 0x3CC  <-> "pmpaddr28"
+mapping clause csr_name_map = 0x3CD  <-> "pmpaddr29"
+mapping clause csr_name_map = 0x3CE  <-> "pmpaddr30"
+mapping clause csr_name_map = 0x3CF  <-> "pmpaddr31"
+mapping clause csr_name_map = 0x3D0  <-> "pmpaddr32"
+mapping clause csr_name_map = 0x3D1  <-> "pmpaddr33"
+mapping clause csr_name_map = 0x3D2  <-> "pmpaddr34"
+mapping clause csr_name_map = 0x3D3  <-> "pmpaddr35"
+mapping clause csr_name_map = 0x3D4  <-> "pmpaddr36"
+mapping clause csr_name_map = 0x3D5  <-> "pmpaddr37"
+mapping clause csr_name_map = 0x3D6  <-> "pmpaddr38"
+mapping clause csr_name_map = 0x3D7  <-> "pmpaddr39"
+mapping clause csr_name_map = 0x3D8  <-> "pmpaddr40"
+mapping clause csr_name_map = 0x3D9  <-> "pmpaddr41"
+mapping clause csr_name_map = 0x3DA  <-> "pmpaddr42"
+mapping clause csr_name_map = 0x3DB  <-> "pmpaddr43"
+mapping clause csr_name_map = 0x3DC  <-> "pmpaddr44"
+mapping clause csr_name_map = 0x3DD  <-> "pmpaddr45"
+mapping clause csr_name_map = 0x3DE  <-> "pmpaddr46"
+mapping clause csr_name_map = 0x3DF  <-> "pmpaddr47"
+mapping clause csr_name_map = 0x3E0  <-> "pmpaddr48"
+mapping clause csr_name_map = 0x3E1  <-> "pmpaddr49"
+mapping clause csr_name_map = 0x3E2  <-> "pmpaddr50"
+mapping clause csr_name_map = 0x3E3  <-> "pmpaddr51"
+mapping clause csr_name_map = 0x3E4  <-> "pmpaddr52"
+mapping clause csr_name_map = 0x3E5  <-> "pmpaddr53"
+mapping clause csr_name_map = 0x3E6  <-> "pmpaddr54"
+mapping clause csr_name_map = 0x3E7  <-> "pmpaddr55"
+mapping clause csr_name_map = 0x3E8  <-> "pmpaddr56"
+mapping clause csr_name_map = 0x3E9  <-> "pmpaddr57"
+mapping clause csr_name_map = 0x3EA  <-> "pmpaddr58"
+mapping clause csr_name_map = 0x3EB  <-> "pmpaddr59"
+mapping clause csr_name_map = 0x3EC  <-> "pmpaddr60"
+mapping clause csr_name_map = 0x3ED  <-> "pmpaddr61"
+mapping clause csr_name_map = 0x3EE  <-> "pmpaddr62"
+mapping clause csr_name_map = 0x3EF  <-> "pmpaddr63"
+
+// pmpcfgN
+function clause is_CSR_defined(0x3A) @ idx : bits(4) = sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | xlen == 32)
+function clause read_CSR(0x3A @ idx : bits(4) if idx[0] == bitzero | xlen == 32) = pmpReadCfgReg(unsigned(idx))
+function clause write_CSR((0x3A @ idx : bits(4), value) if idx[0] == bitzero | xlen == 32) = {
+  let idx = unsigned(idx);
+  pmpWriteCfgReg(idx, value);
+  pmpReadCfgReg(idx)
+}
+
+// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
+function clause is_CSR_defined(0x3B) @ idx : bits(4) = sys_pmp_count() > unsigned(0b00 @ idx)
+function clause is_CSR_defined(0x3C) @ idx : bits(4) = sys_pmp_count() > unsigned(0b01 @ idx)
+function clause is_CSR_defined(0x3D) @ idx : bits(4) = sys_pmp_count() > unsigned(0b10 @ idx)
+function clause is_CSR_defined(0x3E) @ idx : bits(4) = sys_pmp_count() > unsigned(0b11 @ idx)
+
+function clause read_CSR(0x3B @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b00 @ idx))
+function clause read_CSR(0x3C @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b01 @ idx))
+function clause read_CSR(0x3D @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b10 @ idx))
+function clause read_CSR(0x3E @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b11 @ idx))
+
+function clause write_CSR(0x3B @ idx : bits(4), value) = { let idx = unsigned(0b00 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
+function clause write_CSR(0x3C @ idx : bits(4), value) = { let idx = unsigned(0b01 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
+function clause write_CSR(0x3D @ idx : bits(4), value) = { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
+function clause write_CSR(0x3E @ idx : bits(4), value) = { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 72246e8c7..b1cb6efe0 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -40,15 +40,6 @@ function clause is_CSR_defined(0x342) = true // mcause
 function clause is_CSR_defined(0x343) = true // mtval
 function clause is_CSR_defined(0x344) = true // mip
 
-// pmpcfgN
-function clause is_CSR_defined(0x3A) @ idx : bits(4) = sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | xlen == 32)
-
-// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
-function clause is_CSR_defined(0x3B) @ idx : bits(4) = sys_pmp_count() > unsigned(0b00 @ idx)
-function clause is_CSR_defined(0x3C) @ idx : bits(4) = sys_pmp_count() > unsigned(0b01 @ idx)
-function clause is_CSR_defined(0x3D) @ idx : bits(4) = sys_pmp_count() > unsigned(0b10 @ idx)
-function clause is_CSR_defined(0x3E) @ idx : bits(4) = sys_pmp_count() > unsigned(0b11 @ idx)
-
 /* counters */
 
 function clause is_CSR_defined(0xB00) = true // mcycle

From 2088b080609a0a258c67b00fd063639bd45e9755 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 14:39:01 -0700
Subject: [PATCH 05/17] Move Vector CSRs

---
 model/riscv_csr_begin.sail    | 8 --------
 model/riscv_vext_control.sail | 8 ++++++++
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index e252caa4e..f28749fc1 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -70,14 +70,6 @@ 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"
-/* vector csrs */
-mapping clause csr_name_map = 0x008  <-> "vstart"
-mapping clause csr_name_map = 0x009  <-> "vxsat"
-mapping clause csr_name_map = 0x00A  <-> "vxrm"
-mapping clause csr_name_map = 0x00F  <-> "vcsr"
-mapping clause csr_name_map = 0xC20  <-> "vl"
-mapping clause csr_name_map = 0xC21  <-> "vtype"
-mapping clause csr_name_map = 0xC22  <-> "vlenb"
 
 val csr_name : csreg -> string
 overload to_str = {csr_name}
diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail
index 167b44a1c..0113ad636 100755
--- a/model/riscv_vext_control.sail
+++ b/model/riscv_vext_control.sail
@@ -6,6 +6,14 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+mapping clause csr_name_map = 0x008  <-> "vstart"
+mapping clause csr_name_map = 0x009  <-> "vxsat"
+mapping clause csr_name_map = 0x00A  <-> "vxrm"
+mapping clause csr_name_map = 0x00F  <-> "vcsr"
+mapping clause csr_name_map = 0xC20  <-> "vl"
+mapping clause csr_name_map = 0xC21  <-> "vtype"
+mapping clause csr_name_map = 0xC22  <-> "vlenb"
+
 function clause is_CSR_defined (0x008) = true
 function clause is_CSR_defined (0x009) = true
 function clause is_CSR_defined (0x00A) = true

From fb91e05db0a69346d4d53113a11437a8a9de20b6 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 14:50:14 -0700
Subject: [PATCH 06/17] Move trigger/debug CSRs

---
 model/riscv_csr_begin.sail   | 5 -----
 model/riscv_insts_zicsr.sail | 6 ------
 model/riscv_sys_control.sail | 3 ---
 model/riscv_sys_regs.sail    | 9 +++++++++
 4 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index f28749fc1..cc6619239 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -65,11 +65,6 @@ mapping clause csr_name_map = 0xB02  <-> "minstret"
 
 mapping clause csr_name_map = 0xB80  <-> "mcycleh"
 mapping clause csr_name_map = 0xB82  <-> "minstreth"
-/* 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
 overload to_str = {csr_name}
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index ee4e52e3e..8d8d92803 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -49,9 +49,6 @@ function clause read_CSR(0xB02) = minstret[(xlen - 1) .. 0]
 function clause read_CSR(0xB80 if xlen == 32)= mcycle[63 .. 32]
 function clause read_CSR(0xB82 if xlen == 32) = minstret[63 .. 32]
 
-/* trigger/debug */
-function clause read_CSR(0x7a0) = ~(tselect)  /* this indicates we don't have any trigger support */
-
 /* supervisor mode */
 function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
@@ -101,9 +98,6 @@ function clause write_CSR(0xB02, value) = { minstret[(xlen - 1) .. 0] = value; m
 function clause write_CSR((0xB80, value) if xlen == 32) = { mcycle[63 .. 32] = value; value }
 function clause write_CSR((0xB82, value) if xlen == 32) = { minstret[63 .. 32] = value; minstret_increment = false; value }
 
-/* trigger/debug */
-function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
-
 /* supervisor mode */
 function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index b1cb6efe0..3ce3245f2 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -48,9 +48,6 @@ function clause is_CSR_defined(0xB02) = true // minstret
 function clause is_CSR_defined(0xB80) = xlen == 32 // mcycleh
 function clause is_CSR_defined(0xB82) = xlen == 32 // minstreth
 
-/* disabled trigger/debug module */
-function clause is_CSR_defined(0x7a0) = true
-
 /* supervisor mode: trap setup */
 function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
 function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index e02c2b4b5..e3ef3bb40 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -698,6 +698,15 @@ function legalize_satp32(a : Architecture, o : bits(32), v : bits(32)) -> bits(3
 /* disabled trigger/debug module */
 register tselect : xlenbits
 
+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"
+
+function clause is_CSR_defined(0x7a0) = true
+function clause read_CSR(0x7a0) = ~(tselect)  /* this indicates we don't have any trigger support */
+function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
+
 /*
  * The seed CSR (entropy source)
  * ------------------------------------------------------------

From c0d3f0c64db8ac5518ccb6df0956432a9616d025 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 14:59:44 -0700
Subject: [PATCH 07/17] Move envcfg CSRs

---
 model/riscv_csr_begin.sail   |  5 -----
 model/riscv_insts_zicsr.sail |  7 -------
 model/riscv_sys_control.sail |  3 ---
 model/riscv_sys_regs.sail    | 25 ++++++++++++++++++++++---
 4 files changed, 22 insertions(+), 18 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index cc6619239..f69b6bf66 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -39,8 +39,6 @@ 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"
-/* supervisor envcfg */
-mapping clause csr_name_map = 0x10A  <-> "senvcfg"
 /* machine trap setup */
 mapping clause csr_name_map = 0x300  <-> "mstatus"
 mapping clause csr_name_map = 0x301  <-> "misa"
@@ -50,9 +48,6 @@ mapping clause csr_name_map = 0x304  <-> "mie"
 mapping clause csr_name_map = 0x305  <-> "mtvec"
 mapping clause csr_name_map = 0x306  <-> "mcounteren"
 mapping clause csr_name_map = 0x320  <-> "mcountinhibit"
-/* machine envcfg */
-mapping clause csr_name_map = 0x30A  <-> "menvcfg"
-mapping clause csr_name_map = 0x31A  <-> "menvcfgh"
 /* machine trap handling */
 mapping clause csr_name_map = 0x340  <-> "mscratch"
 mapping clause csr_name_map = 0x341  <-> "mepc"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 8d8d92803..1b4ef6088 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -32,9 +32,7 @@ function clause read_CSR(0x303) = mideleg.bits
 function clause read_CSR(0x304) = mie.bits
 function clause read_CSR(0x305) = get_mtvec()
 function clause read_CSR(0x306) = zero_extend(mcounteren.bits)
-function clause read_CSR(0x30A) = menvcfg.bits[xlen - 1 .. 0]
 function clause read_CSR(0x310 if xlen == 32) = mstatush.bits
-function clause read_CSR(0x31A if xlen == 32) = menvcfg.bits[63 .. 32]
 function clause read_CSR(0x320) = zero_extend(mcountinhibit.bits)
 
 function clause read_CSR(0x340) = mscratch
@@ -54,7 +52,6 @@ function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
 function clause read_CSR(0x105) = get_stvec()
 function clause read_CSR(0x106) = zero_extend(scounteren.bits)
-function clause read_CSR(0x10A) = senvcfg.bits[xlen - 1 .. 0]
 function clause read_CSR(0x140) = sscratch
 function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask()
 function clause read_CSR(0x142) = scause.bits
@@ -81,10 +78,7 @@ function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg,
 function clause write_CSR(0x304, value) = { mie = legalize_mie(mie, value); mie.bits }
 function clause write_CSR(0x305, value) = { set_mtvec(value) }
 function clause write_CSR(0x306, value) = { mcounteren = legalize_mcounteren(mcounteren, value); zero_extend(mcounteren.bits) }
-function clause write_CSR((0x30A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); menvcfg.bits[31 .. 0] }
-function clause write_CSR((0x30A, value) if xlen == 64) = { menvcfg = legalize_menvcfg(menvcfg, value); menvcfg.bits }
 function clause write_CSR((0x310, value) if xlen == 32) = { mstatush.bits } // ignore writes for now
-function clause write_CSR((0x31A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); menvcfg.bits[63 .. 32] }
 function clause write_CSR(0x320, value) = { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); zero_extend(mcountinhibit.bits) }
 function clause write_CSR(0x340, value) = { mscratch = value; mscratch }
 function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
@@ -103,7 +97,6 @@ function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus,
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
 function clause write_CSR(0x105, value) = { set_stvec(value) }
 function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) }
-function clause write_CSR(0x10A, value) = { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); senvcfg.bits[xlen - 1 .. 0] }
 function clause write_CSR(0x140, value) = { sscratch = value; sscratch }
 function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
 function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 3ce3245f2..7e902eaeb 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -27,9 +27,7 @@ function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) // mideleg
 function clause is_CSR_defined(0x304) = true // mie
 function clause is_CSR_defined(0x305) = true // mtvec
 function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren
-function clause is_CSR_defined(0x30A) = extensionEnabled(Ext_U) // menvcfg
 function clause is_CSR_defined(0x310) = xlen == 32 // mstatush
-function clause is_CSR_defined(0x31A) = extensionEnabled(Ext_U) & (xlen == 32) // menvcfgh
 function clause is_CSR_defined(0x320) = true // mcountinhibit
 
 
@@ -53,7 +51,6 @@ function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
 function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
 function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
 function clause is_CSR_defined(0x106) = extensionEnabled(Ext_S) // scounteren
-function clause is_CSR_defined(0x10A) = extensionEnabled(Ext_S) // senvcfg
 
 /* supervisor mode: trap handling */
 function clause is_CSR_defined(0x140) = extensionEnabled(Ext_S) // sscratch
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index e3ef3bb40..612eca877 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -759,6 +759,7 @@ function read_seed_csr() -> xlenbits = {
 /* Writes to the seed CSR are ignored */
 function write_seed_csr () -> xlenbits = zeros()
 
+// envcfg Resisters
 bitfield MEnvcfg : bits(64) = {
   // Supervisor TimeCmp Extension
   STCE   : 63,
@@ -791,9 +792,6 @@ bitfield SEnvcfg : xlenbits = {
   FIOM   : 0,
 }
 
-register menvcfg : MEnvcfg
-register senvcfg : SEnvcfg
-
 function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = {
   let v = Mk_MEnvcfg(v);
   let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0];
@@ -808,6 +806,26 @@ function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = {
   o
 }
 
+register menvcfg : MEnvcfg
+register senvcfg : SEnvcfg
+
+mapping clause csr_name_map = 0x30A  <-> "menvcfg"
+mapping clause csr_name_map = 0x31A  <-> "menvcfgh"
+mapping clause csr_name_map = 0x10A  <-> "senvcfg"
+
+function clause is_CSR_defined(0x30A) = extensionEnabled(Ext_U) // menvcfg
+function clause is_CSR_defined(0x31A) = extensionEnabled(Ext_U) & (xlen == 32) // menvcfgh
+function clause is_CSR_defined(0x10A) = extensionEnabled(Ext_S) // senvcfg
+
+function clause read_CSR(0x30A) = menvcfg.bits[xlen - 1 .. 0]
+function clause read_CSR(0x31A if xlen == 32) = menvcfg.bits[63 .. 32]
+function clause read_CSR(0x10A) = senvcfg.bits[xlen - 1 .. 0]
+
+function clause write_CSR((0x30A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); menvcfg.bits[31 .. 0] }
+function clause write_CSR((0x30A, value) if xlen == 64) = { menvcfg = legalize_menvcfg(menvcfg, value); menvcfg.bits }
+function clause write_CSR((0x31A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); menvcfg.bits[63 .. 32] }
+function clause write_CSR(0x10A, value) = { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); senvcfg.bits[xlen - 1 .. 0] }
+
 // Return whether or not FIOM is currently active, based on the current
 // privilege and the menvcfg/senvcfg settings. This means that I/O fences
 // imply memory fence.
@@ -818,6 +836,7 @@ function is_fiom_active() -> bool = {
     User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1,
   }
 }
+
 /* vector csrs */
 register vstart : bits(16) /* use the largest possible length of vstart */
 register vl     : xlenbits

From 89f2504e13f9ab4af05cd69b6d995bd3a0208bef Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 15:31:18 -0700
Subject: [PATCH 08/17] Move SATP CSR

---
 model/riscv_csr_begin.sail   |  2 --
 model/riscv_insts_zicsr.sail |  2 --
 model/riscv_sys_control.sail |  3 ---
 model/riscv_vmem.sail        | 10 +++++++---
 4 files changed, 7 insertions(+), 10 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index f69b6bf66..9a67ac962 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -37,8 +37,6 @@ 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 trap setup */
 mapping clause csr_name_map = 0x300  <-> "mstatus"
 mapping clause csr_name_map = 0x301  <-> "misa"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 1b4ef6088..9f285e05d 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -57,7 +57,6 @@ function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mas
 function clause read_CSR(0x142) = scause.bits
 function clause read_CSR(0x143) = stval
 function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits
-function clause read_CSR(0x180) = satp
 
 /* user mode counters */
 function clause read_CSR(0xC00) = mcycle[(xlen - 1) .. 0]
@@ -102,7 +101,6 @@ function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
 function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits }
 function clause write_CSR(0x143, value) = { stval = value; stval }
 function clause write_CSR(0x144, value) = { mip = legalize_sip(mip, mideleg, value); mip.bits }
-function clause write_CSR(0x180, value) = { satp = legalize_satp(cur_Architecture(), satp, value); satp }
 
 /* user mode: seed (entropy source). writes are ignored */
 function clause write_CSR(0x015, value) = write_seed_csr()
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 7e902eaeb..83a59cc8d 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -59,9 +59,6 @@ function clause is_CSR_defined(0x142) = extensionEnabled(Ext_S) // scause
 function clause is_CSR_defined(0x143) = extensionEnabled(Ext_S) // stval
 function clause is_CSR_defined(0x144) = extensionEnabled(Ext_S) // sip
 
-/* supervisor mode: address translation */
-function clause is_CSR_defined(0x180) = extensionEnabled(Ext_S) // satp
-
 /* user mode: counters */
 function clause is_CSR_defined(0xC00) = extensionEnabled(Ext_U) // cycle
 function clause is_CSR_defined(0xC01) = extensionEnabled(Ext_U) // time
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
index 6b394354d..17a44c268 100644
--- a/model/riscv_vmem.sail
+++ b/model/riscv_vmem.sail
@@ -177,9 +177,6 @@ function pt_walk(sv_params,
 // ****************************************************************
 // Architectural SATP CSR
 
-// PUBLIC: see also riscv_insts_zicsr.sail and other CSR-related files
-register satp : xlenbits
-
 // See riscv_sys_regs.sail for legalize_satp{32,64}().
 // WARNING: those functions legalize Mode but not ASID?
 // PUBLIC: invoked from writeCSR() to fixup WARL fields
@@ -205,6 +202,13 @@ function legalize_satp(a : Architecture,
     internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(xlen))
 }
 
+// PUBLIC
+register satp : xlenbits
+mapping clause csr_name_map = 0x180  <-> "satp"
+function clause is_CSR_defined(0x180) = extensionEnabled(Ext_S)
+function clause read_CSR(0x180) = satp
+function clause write_CSR(0x180, value) = { satp = legalize_satp(cur_Architecture(), satp, value); satp }
+
 // ----------------
 // Fields of SATP
 

From ce8f5bf146bfc8a71af532c7775b17672b664c27 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 15:43:03 -0700
Subject: [PATCH 09/17] Move entropy seed CSR

---
 Makefile                     |  1 +
 model/riscv_csr_begin.sail   |  2 --
 model/riscv_insts_zicsr.sail |  5 ----
 model/riscv_sys_control.sail |  6 -----
 model/riscv_sys_regs.sail    | 36 ---------------------------
 model/riscv_zkr_control.sail | 48 ++++++++++++++++++++++++++++++++++++
 6 files changed, 49 insertions(+), 49 deletions(-)
 create mode 100644 model/riscv_zkr_control.sail

diff --git a/Makefile b/Makefile
index 267553eb1..f59bfe6b5 100644
--- a/Makefile
+++ b/Makefile
@@ -74,6 +74,7 @@ SAIL_SYS_SRCS += riscv_vext_control.sail    # helpers for the 'V' extension
 SAIL_SYS_SRCS += riscv_sys_exceptions.sail  # default basic helpers for exception handling
 SAIL_SYS_SRCS += riscv_sync_exception.sail  # define the exception structure used in the model
 SAIL_SYS_SRCS += riscv_hpm_control.sail
+SAIL_SYS_SRCS += riscv_zkr_control.sail
 SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
 SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 
diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 9a67ac962..493ea9eee 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -15,8 +15,6 @@ scattered mapping csr_name_map
 // TODO: These csr_name_map definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* user entropy source */
-mapping clause csr_name_map = 0x015  <-> "seed"
 /* counter/timers */
 mapping clause csr_name_map = 0xC00  <-> "cycle"
 mapping clause csr_name_map = 0xC01  <-> "time"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 9f285e05d..820eaf178 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -66,9 +66,6 @@ function clause read_CSR(0xC80 if xlen == 32) = mcycle[63 .. 32]
 function clause read_CSR(0xC81 if xlen == 32) = mtime[63 .. 32]
 function clause read_CSR(0xC82 if xlen == 32) = minstret[63 .. 32]
 
-/* user mode: Zkr */
-function clause read_CSR(0x015) = read_seed_csr()
-
 /* machine mode */
 function clause write_CSR(0x300, value) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
@@ -102,8 +99,6 @@ function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits }
 function clause write_CSR(0x143, value) = { stval = value; stval }
 function clause write_CSR(0x144, value) = { mip = legalize_sip(mip, mideleg, value); mip.bits }
 
-/* user mode: seed (entropy source). writes are ignored */
-function clause write_CSR(0x015, value) = write_seed_csr()
 
 function clause execute CSR(csr, rs1, rd, is_imm, op) = {
   let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1);
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 83a59cc8d..e21182f11 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -8,9 +8,6 @@
 
 /* Machine-mode and supervisor-mode functionality. */
 
-enum clause extension = Ext_Zkr
-function clause extensionEnabled(Ext_Zkr) = true
-
 /* CSR access control */
 
 function csrAccess(csr : csreg) -> csrRW = csr[11..10]
@@ -69,9 +66,6 @@ function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (xlen == 32) /
 function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (xlen == 32) // timeh
 function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (xlen == 32) // instreth
 
-/* user mode: Zkr */
-function clause is_CSR_defined(0x015) = extensionEnabled(Ext_Zkr)
-
 
 val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
 function check_CSR_access(csrrw, csrpr, p, isWrite) =
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 612eca877..182be4d6f 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -707,27 +707,6 @@ function clause is_CSR_defined(0x7a0) = true
 function clause read_CSR(0x7a0) = ~(tselect)  /* this indicates we don't have any trigger support */
 function clause write_CSR(0x7a0, value) = { tselect = value; tselect }
 
-/*
- * The seed CSR (entropy source)
- * ------------------------------------------------------------
- */
-
-/* Valid return states for reading the seed CSR. */
-enum seed_opst = {
-  BIST, // Built-in-self-test. No randomness sampled.
-  ES16, // Entropy-sample-16. Valid 16-bits of randomness sampled.
-  WAIT, // Device still gathering entropy.
-  DEAD  // Fatal device compromise. No randomness sampled.
-}
-
-/* Mapping of status codes and their actual encodings. */
-mapping opst_code : seed_opst <-> bits(2) = {
-  BIST <-> 0b00,
-  WAIT <-> 0b01,
-  ES16 <-> 0b10,
-  DEAD <-> 0b11
-}
-
 /*
  * Entropy Source - Platform access to random bits.
  * WARNING: This function currently lacks a proper side-effect annotation.
@@ -744,21 +723,6 @@ val get_16_random_bits = impure {
     lem: "plat_get_16_random_bits"
 } : unit -> bits(16)
 
-/* Entropy source spec requires an Illegal opcode exception be raised if the
- * seed register is read without also being written. This function is only
- * called once we know the CSR is being written, and all other access control
- * checks have been done.
- */
-function read_seed_csr() -> xlenbits = {
-  let reserved_bits : bits(6) = 0b000000;
-  let custom_bits : bits(8) = 0x00;
-  let seed : bits(16) = get_16_random_bits();
-  zero_extend(opst_code(ES16) @ reserved_bits @ custom_bits @ seed)
-}
-
-/* Writes to the seed CSR are ignored */
-function write_seed_csr () -> xlenbits = zeros()
-
 // envcfg Resisters
 bitfield MEnvcfg : bits(64) = {
   // Supervisor TimeCmp Extension
diff --git a/model/riscv_zkr_control.sail b/model/riscv_zkr_control.sail
new file mode 100644
index 000000000..4284cce43
--- /dev/null
+++ b/model/riscv_zkr_control.sail
@@ -0,0 +1,48 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* Zkr entropy seed source */
+enum clause extension = Ext_Zkr
+function clause extensionEnabled(Ext_Zkr) = true
+
+/* Valid return states for reading the seed CSR. */
+enum seed_opst = {
+  BIST, // Built-in-self-test. No randomness sampled.
+  ES16, // Entropy-sample-16. Valid 16-bits of randomness sampled.
+  WAIT, // Device still gathering entropy.
+  DEAD  // Fatal device compromise. No randomness sampled.
+}
+
+/* Mapping of status codes and their actual encodings. */
+mapping opst_code : seed_opst <-> bits(2) = {
+  BIST <-> 0b00,
+  WAIT <-> 0b01,
+  ES16 <-> 0b10,
+  DEAD <-> 0b11
+}
+
+/* Entropy source spec requires an Illegal opcode exception be raised if the
+ * seed register is read without also being written. This function is only
+ * called once we know the CSR is being written, and all other access control
+ * checks have been done.
+ */
+function read_seed_csr() -> xlenbits = {
+  let reserved_bits : bits(6) = 0b000000;
+  let custom_bits : bits(8) = 0x00;
+  let seed : bits(16) = get_16_random_bits();
+  zero_extend(opst_code(ES16) @ reserved_bits @ custom_bits @ seed)
+}
+
+/* Writes to the seed CSR are ignored */
+function write_seed_csr () -> xlenbits = zeros()
+
+/* CSR mapping */
+mapping clause csr_name_map = 0x015  <-> "seed"
+function clause is_CSR_defined(0x015) = extensionEnabled(Ext_Zkr)
+function clause read_CSR(0x015) = read_seed_csr()
+function clause write_CSR(0x015, value) = write_seed_csr()

From 37f8bd56c638a7972fade67237f1da6f568f010f Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 15:50:45 -0700
Subject: [PATCH 10/17] Move Zicntr CSRs

---
 Makefile                        |  1 +
 model/riscv_csr_begin.sail      | 15 ----------
 model/riscv_insts_zicsr.sail    | 20 -------------
 model/riscv_sys_control.sail    | 18 ------------
 model/riscv_zicntr_control.sail | 51 +++++++++++++++++++++++++++++++++
 5 files changed, 52 insertions(+), 53 deletions(-)
 create mode 100644 model/riscv_zicntr_control.sail

diff --git a/Makefile b/Makefile
index f59bfe6b5..de2a9cdbf 100644
--- a/Makefile
+++ b/Makefile
@@ -75,6 +75,7 @@ SAIL_SYS_SRCS += riscv_sys_exceptions.sail  # default basic helpers for exceptio
 SAIL_SYS_SRCS += riscv_sync_exception.sail  # define the exception structure used in the model
 SAIL_SYS_SRCS += riscv_hpm_control.sail
 SAIL_SYS_SRCS += riscv_zkr_control.sail
+SAIL_SYS_SRCS += riscv_zicntr_control.sail
 SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
 SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 
diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 493ea9eee..ef3c728d2 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -15,15 +15,6 @@ scattered mapping csr_name_map
 // TODO: These csr_name_map definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* 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"
-
 /* supervisor trap setup */
 mapping clause csr_name_map = 0x100  <-> "sstatus"
 mapping clause csr_name_map = 0x104  <-> "sie"
@@ -50,12 +41,6 @@ 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 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"
 
 val csr_name : csreg -> string
 overload to_str = {csr_name}
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 820eaf178..5e91042bb 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -41,12 +41,6 @@ function clause read_CSR(0x342) = mcause.bits
 function clause read_CSR(0x343) = mtval
 function clause read_CSR(0x344) = mip.bits
 
-/* machine mode counters */
-function clause read_CSR(0xB00) = mcycle[(xlen - 1) .. 0]
-function clause read_CSR(0xB02) = minstret[(xlen - 1) .. 0]
-function clause read_CSR(0xB80 if xlen == 32)= mcycle[63 .. 32]
-function clause read_CSR(0xB82 if xlen == 32) = minstret[63 .. 32]
-
 /* supervisor mode */
 function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
@@ -58,14 +52,6 @@ function clause read_CSR(0x142) = scause.bits
 function clause read_CSR(0x143) = stval
 function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits
 
-/* user mode counters */
-function clause read_CSR(0xC00) = mcycle[(xlen - 1) .. 0]
-function clause read_CSR(0xC01) = mtime[(xlen - 1) .. 0]
-function clause read_CSR(0xC02) = minstret[(xlen - 1) .. 0]
-function clause read_CSR(0xC80 if xlen == 32) = mcycle[63 .. 32]
-function clause read_CSR(0xC81 if xlen == 32) = mtime[63 .. 32]
-function clause read_CSR(0xC82 if xlen == 32) = minstret[63 .. 32]
-
 /* machine mode */
 function clause write_CSR(0x300, value) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
@@ -82,12 +68,6 @@ function clause write_CSR(0x342, value) = { mcause.bits = value; mcause.bits }
 function clause write_CSR(0x343, value) = { mtval = value; mtval }
 function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.bits }
 
-/* machine mode counters */
-function clause write_CSR(0xB00, value) = { mcycle[(xlen - 1) .. 0] = value; value }
-function clause write_CSR(0xB02, value) = { minstret[(xlen - 1) .. 0] = value; minstret_increment = false; value }
-function clause write_CSR((0xB80, value) if xlen == 32) = { mcycle[63 .. 32] = value; value }
-function clause write_CSR((0xB82, value) if xlen == 32) = { minstret[63 .. 32] = value; minstret_increment = false; value }
-
 /* supervisor mode */
 function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index e21182f11..693c5b755 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -35,14 +35,6 @@ function clause is_CSR_defined(0x342) = true // mcause
 function clause is_CSR_defined(0x343) = true // mtval
 function clause is_CSR_defined(0x344) = true // mip
 
-/* counters */
-
-function clause is_CSR_defined(0xB00) = true // mcycle
-function clause is_CSR_defined(0xB02) = true // minstret
-
-function clause is_CSR_defined(0xB80) = xlen == 32 // mcycleh
-function clause is_CSR_defined(0xB82) = xlen == 32 // minstreth
-
 /* supervisor mode: trap setup */
 function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
 function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
@@ -56,16 +48,6 @@ function clause is_CSR_defined(0x142) = extensionEnabled(Ext_S) // scause
 function clause is_CSR_defined(0x143) = extensionEnabled(Ext_S) // stval
 function clause is_CSR_defined(0x144) = extensionEnabled(Ext_S) // sip
 
-/* user mode: counters */
-function clause is_CSR_defined(0xC00) = extensionEnabled(Ext_U) // cycle
-function clause is_CSR_defined(0xC01) = extensionEnabled(Ext_U) // time
-function clause is_CSR_defined(0xC02) = extensionEnabled(Ext_U) // instret
-
-
-function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (xlen == 32) // cycleh
-function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (xlen == 32) // timeh
-function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (xlen == 32) // instreth
-
 
 val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
 function check_CSR_access(csrrw, csrpr, p, isWrite) =
diff --git a/model/riscv_zicntr_control.sail b/model/riscv_zicntr_control.sail
new file mode 100644
index 000000000..136b991ae
--- /dev/null
+++ b/model/riscv_zicntr_control.sail
@@ -0,0 +1,51 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* user counters/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"
+
+function clause is_CSR_defined(0xC00) = extensionEnabled(Ext_U) // cycle
+function clause is_CSR_defined(0xC01) = extensionEnabled(Ext_U) // time
+function clause is_CSR_defined(0xC02) = extensionEnabled(Ext_U) // instret
+function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (xlen == 32) // cycleh
+function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (xlen == 32) // timeh
+function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (xlen == 32) // instreth
+
+function clause read_CSR(0xC00) = mcycle[(xlen - 1) .. 0]
+function clause read_CSR(0xC01) = mtime[(xlen - 1) .. 0]
+function clause read_CSR(0xC02) = minstret[(xlen - 1) .. 0]
+function clause read_CSR(0xC80 if xlen == 32) = mcycle[63 .. 32]
+function clause read_CSR(0xC81 if xlen == 32) = mtime[63 .. 32]
+function clause read_CSR(0xC82 if xlen == 32) = minstret[63 .. 32]
+
+
+/* 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"
+
+function clause is_CSR_defined(0xB00) = true // mcycle
+function clause is_CSR_defined(0xB02) = true // minstret
+function clause is_CSR_defined(0xB80) = xlen == 32 // mcycleh
+function clause is_CSR_defined(0xB82) = xlen == 32 // minstreth
+
+function clause read_CSR(0xB00) = mcycle[(xlen - 1) .. 0]
+function clause read_CSR(0xB02) = minstret[(xlen - 1) .. 0]
+function clause read_CSR(0xB80 if xlen == 32)= mcycle[63 .. 32]
+function clause read_CSR(0xB82 if xlen == 32) = minstret[63 .. 32]
+
+function clause write_CSR(0xB00, value) = { mcycle[(xlen - 1) .. 0] = value; value }
+function clause write_CSR(0xB02, value) = { minstret[(xlen - 1) .. 0] = value; minstret_increment = false; value }
+function clause write_CSR((0xB80, value) if xlen == 32) = { mcycle[63 .. 32] = value; value }
+function clause write_CSR((0xB82, value) if xlen == 32) = { minstret[63 .. 32] = value; minstret_increment = false; value }

From 1a250811927c65db25cbfb27fc5662b762230891 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 21:13:42 -0700
Subject: [PATCH 11/17] Move s/mcount CSRs

---
 model/riscv_csr_begin.sail   |  3 ---
 model/riscv_insts_zicsr.sail |  6 ------
 model/riscv_sys_control.sail |  3 ---
 model/riscv_sys_regs.sail    | 30 ++++++++++++++++++++++++------
 4 files changed, 24 insertions(+), 18 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index ef3c728d2..6eb41a4db 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -19,7 +19,6 @@ scattered mapping csr_name_map
 mapping clause csr_name_map = 0x100  <-> "sstatus"
 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"
@@ -33,8 +32,6 @@ 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"
-mapping clause csr_name_map = 0x320  <-> "mcountinhibit"
 /* machine trap handling */
 mapping clause csr_name_map = 0x340  <-> "mscratch"
 mapping clause csr_name_map = 0x341  <-> "mepc"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 5e91042bb..0608c0877 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -31,9 +31,7 @@ function clause read_CSR(0x302) = medeleg.bits
 function clause read_CSR(0x303) = mideleg.bits
 function clause read_CSR(0x304) = mie.bits
 function clause read_CSR(0x305) = get_mtvec()
-function clause read_CSR(0x306) = zero_extend(mcounteren.bits)
 function clause read_CSR(0x310 if xlen == 32) = mstatush.bits
-function clause read_CSR(0x320) = zero_extend(mcountinhibit.bits)
 
 function clause read_CSR(0x340) = mscratch
 function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
@@ -45,7 +43,6 @@ function clause read_CSR(0x344) = mip.bits
 function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
 function clause read_CSR(0x105) = get_stvec()
-function clause read_CSR(0x106) = zero_extend(scounteren.bits)
 function clause read_CSR(0x140) = sscratch
 function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask()
 function clause read_CSR(0x142) = scause.bits
@@ -59,9 +56,7 @@ function clause write_CSR(0x302, value) = { medeleg = legalize_medeleg(medeleg,
 function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits }
 function clause write_CSR(0x304, value) = { mie = legalize_mie(mie, value); mie.bits }
 function clause write_CSR(0x305, value) = { set_mtvec(value) }
-function clause write_CSR(0x306, value) = { mcounteren = legalize_mcounteren(mcounteren, value); zero_extend(mcounteren.bits) }
 function clause write_CSR((0x310, value) if xlen == 32) = { mstatush.bits } // ignore writes for now
-function clause write_CSR(0x320, value) = { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); zero_extend(mcountinhibit.bits) }
 function clause write_CSR(0x340, value) = { mscratch = value; mscratch }
 function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
 function clause write_CSR(0x342, value) = { mcause.bits = value; mcause.bits }
@@ -72,7 +67,6 @@ function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.
 function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
 function clause write_CSR(0x105, value) = { set_stvec(value) }
-function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) }
 function clause write_CSR(0x140, value) = { sscratch = value; sscratch }
 function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
 function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 693c5b755..e62bad3f3 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -23,9 +23,7 @@ function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) // medeleg
 function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) // mideleg
 function clause is_CSR_defined(0x304) = true // mie
 function clause is_CSR_defined(0x305) = true // mtvec
-function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren
 function clause is_CSR_defined(0x310) = xlen == 32 // mstatush
-function clause is_CSR_defined(0x320) = true // mcountinhibit
 
 
 /* machine mode: trap handling */
@@ -39,7 +37,6 @@ function clause is_CSR_defined(0x344) = true // mip
 function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
 function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
 function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
-function clause is_CSR_defined(0x106) = extensionEnabled(Ext_S) // scounteren
 
 /* supervisor mode: trap handling */
 function clause is_CSR_defined(0x140) = extensionEnabled(Ext_S) // sscratch
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 182be4d6f..348299c68 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -424,25 +424,37 @@ bitfield Counteren : bits(32) = {
   CY   : 0
 }
 
-register mcounteren : Counteren
-register scounteren : Counteren
-
-function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
+// scounteren
+function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
   let supported_counters = sys_writable_hpm_counters()[31 .. 3] @ 0b111;
   Mk_Counteren(v[31 .. 0] & supported_counters)
 }
 
-function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
+register scounteren : Counteren
+mapping clause csr_name_map = 0x106  <-> "scounteren"
+function clause is_CSR_defined(0x106) = extensionEnabled(Ext_S) // scounteren
+function clause read_CSR(0x106) = zero_extend(scounteren.bits)
+function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) }
+
+// mcounteren
+function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
   let supported_counters = sys_writable_hpm_counters()[31 .. 3] @ 0b111;
   Mk_Counteren(v[31 .. 0] & supported_counters)
 }
 
+register mcounteren : Counteren
+mapping clause csr_name_map = 0x306  <-> "mcounteren"
+function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren
+function clause read_CSR(0x306) = zero_extend(mcounteren.bits)
+function clause write_CSR(0x306, value) = { mcounteren = legalize_mcounteren(mcounteren, value); zero_extend(mcounteren.bits) }
+
+
+// mcountinhibit
 bitfield Counterin : bits(32) = {
   HPM  : 31 .. 3,
   IR : 2,
   CY : 0
 }
-register mcountinhibit : Counterin
 
 function legalize_mcountinhibit(c : Counterin, v : xlenbits) -> Counterin = {
   // Note the 0 in 0b101 is because the mtimer counter can't be paused.
@@ -450,6 +462,12 @@ function legalize_mcountinhibit(c : Counterin, v : xlenbits) -> Counterin = {
   Mk_Counterin(v[31 .. 0] & supported_counters)
 }
 
+register mcountinhibit : Counterin
+mapping clause csr_name_map = 0x320  <-> "mcountinhibit"
+function clause is_CSR_defined(0x320) = true // mcountinhibit
+function clause read_CSR(0x320) = zero_extend(mcountinhibit.bits)
+function clause write_CSR(0x320, value) = { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); zero_extend(mcountinhibit.bits) }
+
 register mcycle : bits(64)
 register mtime : bits(64)
 

From 8dc4736c20018cd25a713a4db703673baf16d3d5 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 21:35:07 -0700
Subject: [PATCH 12/17] move status CSRs

---
 model/riscv_csr_begin.sail   |  2 --
 model/riscv_insts_zicsr.sail |  6 ------
 model/riscv_sys_control.sail |  3 ---
 model/riscv_sys_regs.sail    | 15 +++++++++++++++
 4 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 6eb41a4db..4d7a0d674 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -16,7 +16,6 @@ scattered mapping csr_name_map
 // corresponding to their extensions rather than all be here.
 
 /* supervisor trap setup */
-mapping clause csr_name_map = 0x100  <-> "sstatus"
 mapping clause csr_name_map = 0x104  <-> "sie"
 mapping clause csr_name_map = 0x105  <-> "stvec"
 /* supervisor trap handling */
@@ -26,7 +25,6 @@ mapping clause csr_name_map = 0x142  <-> "scause"
 mapping clause csr_name_map = 0x143  <-> "stval"
 mapping clause csr_name_map = 0x144  <-> "sip"
 /* 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"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 0608c0877..5ccb67896 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -25,13 +25,11 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
 // corresponding to their extensions rather than all be here.
 
 /* machine mode */
-function clause read_CSR(0x300) = mstatus.bits
 function clause read_CSR(0x301) = misa.bits
 function clause read_CSR(0x302) = medeleg.bits
 function clause read_CSR(0x303) = mideleg.bits
 function clause read_CSR(0x304) = mie.bits
 function clause read_CSR(0x305) = get_mtvec()
-function clause read_CSR(0x310 if xlen == 32) = mstatush.bits
 
 function clause read_CSR(0x340) = mscratch
 function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
@@ -40,7 +38,6 @@ function clause read_CSR(0x343) = mtval
 function clause read_CSR(0x344) = mip.bits
 
 /* supervisor mode */
-function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
 function clause read_CSR(0x105) = get_stvec()
 function clause read_CSR(0x140) = sscratch
@@ -50,13 +47,11 @@ function clause read_CSR(0x143) = stval
 function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits
 
 /* machine mode */
-function clause write_CSR(0x300, value) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
 function clause write_CSR(0x302, value) = { medeleg = legalize_medeleg(medeleg, value); medeleg.bits }
 function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits }
 function clause write_CSR(0x304, value) = { mie = legalize_mie(mie, value); mie.bits }
 function clause write_CSR(0x305, value) = { set_mtvec(value) }
-function clause write_CSR((0x310, value) if xlen == 32) = { mstatush.bits } // ignore writes for now
 function clause write_CSR(0x340, value) = { mscratch = value; mscratch }
 function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
 function clause write_CSR(0x342, value) = { mcause.bits = value; mcause.bits }
@@ -64,7 +59,6 @@ function clause write_CSR(0x343, value) = { mtval = value; mtval }
 function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.bits }
 
 /* supervisor mode */
-function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
 function clause write_CSR(0x105, value) = { set_stvec(value) }
 function clause write_CSR(0x140, value) = { sscratch = value; sscratch }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index e62bad3f3..e184c1753 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -17,13 +17,11 @@ function csrPriv(csr : csreg) -> priv_level = csr[9..8]
 // corresponding to their extensions rather than all be here.
 
 /* machine mode: trap setup */
-function clause is_CSR_defined(0x300) = true // mstatus
 function clause is_CSR_defined(0x301) = true // misa
 function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) // medeleg
 function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) // mideleg
 function clause is_CSR_defined(0x304) = true // mie
 function clause is_CSR_defined(0x305) = true // mtvec
-function clause is_CSR_defined(0x310) = xlen == 32 // mstatush
 
 
 /* machine mode: trap handling */
@@ -34,7 +32,6 @@ function clause is_CSR_defined(0x343) = true // mtval
 function clause is_CSR_defined(0x344) = true // mip
 
 /* supervisor mode: trap setup */
-function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
 function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
 function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
 
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 348299c68..2e8244da3 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -272,6 +272,17 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
   } else m
 }
 
+mapping clause csr_name_map = 0x300  <-> "mstatus"
+
+function clause is_CSR_defined(0x300) = true // mstatus
+function clause is_CSR_defined(0x310) = xlen == 32 // mstatush
+
+function clause read_CSR(0x300) = mstatus.bits
+function clause read_CSR(0x310 if xlen == 32) = mstatush.bits
+
+function clause write_CSR(0x300, value) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits }
+function clause write_CSR((0x310, value) if xlen == 32) = { mstatush.bits } // ignore writes for now
+
 /* architecture and extension checks */
 
 function cur_Architecture() -> Architecture = {
@@ -617,6 +628,10 @@ function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = {
   legalize_mstatus(m, lift_sstatus(m, Mk_Sstatus(v)).bits)
 }
 
+mapping clause csr_name_map = 0x100  <-> "sstatus"
+function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus
+function clause read_CSR(0x100) = lower_mstatus(mstatus).bits
+function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits }
 
 
 bitfield Sinterrupts : xlenbits = {

From dc4e8c1100c5d80353f086f484e38464625cc5c5 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 21:45:57 -0700
Subject: [PATCH 13/17] Move machine trap CSRs

---
 model/riscv_csr_begin.sail   |  7 ------
 model/riscv_insts_zicsr.sail | 15 ------------
 model/riscv_sys_control.sail |  7 ------
 model/riscv_sys_regs.sail    | 45 ++++++++++++++++++++++++++++++++----
 4 files changed, 41 insertions(+), 33 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 4d7a0d674..3466f7e0e 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -26,16 +26,9 @@ mapping clause csr_name_map = 0x143  <-> "stval"
 mapping clause csr_name_map = 0x144  <-> "sip"
 /* machine trap setup */
 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"
 /* 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"
 
 val csr_name : csreg -> string
 overload to_str = {csr_name}
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 5ccb67896..d9fb11849 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -26,16 +26,8 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
 
 /* machine mode */
 function clause read_CSR(0x301) = misa.bits
-function clause read_CSR(0x302) = medeleg.bits
-function clause read_CSR(0x303) = mideleg.bits
-function clause read_CSR(0x304) = mie.bits
 function clause read_CSR(0x305) = get_mtvec()
-
-function clause read_CSR(0x340) = mscratch
 function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
-function clause read_CSR(0x342) = mcause.bits
-function clause read_CSR(0x343) = mtval
-function clause read_CSR(0x344) = mip.bits
 
 /* supervisor mode */
 function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
@@ -48,15 +40,8 @@ function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits
 
 /* machine mode */
 function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
-function clause write_CSR(0x302, value) = { medeleg = legalize_medeleg(medeleg, value); medeleg.bits }
-function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits }
-function clause write_CSR(0x304, value) = { mie = legalize_mie(mie, value); mie.bits }
 function clause write_CSR(0x305, value) = { set_mtvec(value) }
-function clause write_CSR(0x340, value) = { mscratch = value; mscratch }
 function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
-function clause write_CSR(0x342, value) = { mcause.bits = value; mcause.bits }
-function clause write_CSR(0x343, value) = { mtval = value; mtval }
-function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.bits }
 
 /* supervisor mode */
 function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index e184c1753..dbc325330 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -18,18 +18,11 @@ function csrPriv(csr : csreg) -> priv_level = csr[9..8]
 
 /* machine mode: trap setup */
 function clause is_CSR_defined(0x301) = true // misa
-function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) // medeleg
-function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) // mideleg
-function clause is_CSR_defined(0x304) = true // mie
 function clause is_CSR_defined(0x305) = true // mtvec
 
 
 /* machine mode: trap handling */
-function clause is_CSR_defined(0x340) = true // mscratch
 function clause is_CSR_defined(0x341) = true // mepc
-function clause is_CSR_defined(0x342) = true // mcause
-function clause is_CSR_defined(0x343) = true // mtval
-function clause is_CSR_defined(0x344) = true // mip
 
 /* supervisor mode: trap setup */
 function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 2e8244da3..3416e7bd8 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -314,9 +314,6 @@ bitfield Minterrupts : xlenbits = {
   MSI : 3,  /* software interrupts */
   SSI : 1,
 }
-register mip     : Minterrupts /* Pending */
-register mie     : Minterrupts /* Enabled */
-register mideleg : Minterrupts /* Delegation to S-mode */
 
 function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = {
   /* The only writable bits are the S-mode bits, and with the 'N'
@@ -361,13 +358,37 @@ bitfield Medeleg : xlenbits = {
   Fetch_Access_Fault: 1,
   Fetch_Addr_Align  : 0
 }
-register medeleg : Medeleg  /* Delegation to S-mode */
 
 function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = {
   /* M-EnvCalls delegation is not supported */
   [Mk_Medeleg(v) with MEnvCall = 0b0]
 }
 
+register mie     : Minterrupts /* Enabled */
+register mip     : Minterrupts /* Pending */
+register medeleg : Medeleg  /* Delegation to S-mode */
+register mideleg : Minterrupts /* Delegation to S-mode */
+
+mapping clause csr_name_map = 0x304  <-> "mie"
+mapping clause csr_name_map = 0x344  <-> "mip"
+mapping clause csr_name_map = 0x302  <-> "medeleg"
+mapping clause csr_name_map = 0x303  <-> "mideleg"
+
+function clause is_CSR_defined(0x304) = true // mie
+function clause is_CSR_defined(0x344) = true // mip
+function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) // medeleg
+function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) // mideleg
+
+function clause read_CSR(0x304) = mie.bits
+function clause read_CSR(0x344) = mip.bits
+function clause read_CSR(0x302) = medeleg.bits
+function clause read_CSR(0x303) = mideleg.bits
+
+function clause write_CSR(0x304, value) = { mie = legalize_mie(mie, value); mie.bits }
+function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.bits }
+function clause write_CSR(0x302, value) = { medeleg = legalize_medeleg(medeleg, value); medeleg.bits }
+function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits }
+
 /* registers for trap handling */
 
 bitfield Mtvec : xlenbits = {
@@ -390,6 +411,10 @@ bitfield Mcause : xlenbits = {
   Cause       : xlen - 2 .. 0
 }
 register mcause : Mcause
+mapping clause csr_name_map = 0x342  <-> "mcause"
+function clause is_CSR_defined(0x342) = true // mcause
+function clause read_CSR(0x342) = mcause.bits
+function clause write_CSR(0x342, value) = { mcause.bits = value; mcause.bits }
 
 /* Interpreting the trap-vector address */
 function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
@@ -426,6 +451,18 @@ function pc_alignment_mask() -> xlenbits =
 register mtval    : xlenbits
 register mscratch : xlenbits
 
+mapping clause csr_name_map = 0x343  <-> "mtval"
+mapping clause csr_name_map = 0x340  <-> "mscratch"
+
+function clause is_CSR_defined(0x343) = true // mtval
+function clause is_CSR_defined(0x340) = true // mscratch
+
+function clause read_CSR(0x343) = mtval
+function clause read_CSR(0x340) = mscratch
+
+function clause write_CSR(0x343, value) = { mtval = value; mtval }
+function clause write_CSR(0x340, value) = { mscratch = value; mscratch }
+
 /* counters */
 
 bitfield Counteren : bits(32) = {

From 7e664439c7c58af0010c104964aaabb727cf2dca Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 22:34:15 -0700
Subject: [PATCH 14/17] Move several supervisor trap CSRs

---
 model/riscv_csr_begin.sail   |  5 -----
 model/riscv_insts_zicsr.sail | 12 ++----------
 model/riscv_sys_control.sail |  6 +-----
 model/riscv_sys_regs.sail    | 30 ++++++++++++++++++++++++++++++
 4 files changed, 33 insertions(+), 20 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 3466f7e0e..2b10af29a 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -16,14 +16,9 @@ scattered mapping csr_name_map
 // corresponding to their extensions rather than all be here.
 
 /* supervisor trap setup */
-mapping clause csr_name_map = 0x104  <-> "sie"
 mapping clause csr_name_map = 0x105  <-> "stvec"
 /* 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"
 /* machine trap setup */
 mapping clause csr_name_map = 0x301  <-> "misa"
 mapping clause csr_name_map = 0x305  <-> "mtvec"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index d9fb11849..38431d046 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -30,13 +30,9 @@ function clause read_CSR(0x305) = get_mtvec()
 function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
 
 /* supervisor mode */
-function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
 function clause read_CSR(0x105) = get_stvec()
-function clause read_CSR(0x140) = sscratch
 function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask()
-function clause read_CSR(0x142) = scause.bits
-function clause read_CSR(0x143) = stval
-function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits
+
 
 /* machine mode */
 function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
@@ -44,13 +40,9 @@ function clause write_CSR(0x305, value) = { set_mtvec(value) }
 function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
 
 /* supervisor mode */
-function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
 function clause write_CSR(0x105, value) = { set_stvec(value) }
-function clause write_CSR(0x140, value) = { sscratch = value; sscratch }
 function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
-function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits }
-function clause write_CSR(0x143, value) = { stval = value; stval }
-function clause write_CSR(0x144, value) = { mip = legalize_sip(mip, mideleg, value); mip.bits }
+
 
 
 function clause execute CSR(csr, rs1, rd, is_imm, op) = {
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index dbc325330..d791f1c31 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -25,15 +25,11 @@ function clause is_CSR_defined(0x305) = true // mtvec
 function clause is_CSR_defined(0x341) = true // mepc
 
 /* supervisor mode: trap setup */
-function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
 function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
 
 /* supervisor mode: trap handling */
-function clause is_CSR_defined(0x140) = extensionEnabled(Ext_S) // sscratch
 function clause is_CSR_defined(0x141) = extensionEnabled(Ext_S) // sepc
-function clause is_CSR_defined(0x142) = extensionEnabled(Ext_S) // scause
-function clause is_CSR_defined(0x143) = extensionEnabled(Ext_S) // stval
-function clause is_CSR_defined(0x144) = extensionEnabled(Ext_S) // sip
+
 
 
 val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 3416e7bd8..83889fa7c 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -679,6 +679,7 @@ bitfield Sinterrupts : xlenbits = {
   SSI : 1,  /* software interrupts */
 }
 
+// sip
 /* Provides the sip read view of mip (m) as delegated by mideleg (d). */
 function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = {
   let s : Sinterrupts = Mk_Sinterrupts(zeros());
@@ -712,6 +713,13 @@ function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr
   lift_sip(m, d, Mk_Sinterrupts(v))
 }
 
+mapping clause csr_name_map = 0x144  <-> "sip"
+function clause is_CSR_defined(0x144) = extensionEnabled(Ext_S) // sip
+function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits
+function clause write_CSR(0x144, value) = { mip = legalize_sip(mip, mideleg, value); mip.bits }
+
+
+// sie
 /* Returns the new value of mie from the previous mie (o) and the written sie (s) as delegated by mideleg (d). */
 function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
   let m : Minterrupts = o;
@@ -727,6 +735,12 @@ function legalize_sie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr
 }
 
 
+mapping clause csr_name_map = 0x104  <-> "sie"
+function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie
+function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits
+function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits }
+
+
 /* other non-VM related supervisor state */
 register stvec    : Mtvec
 register sscratch : xlenbits
@@ -734,6 +748,22 @@ register sepc     : xlenbits
 register scause   : Mcause
 register stval    : xlenbits
 
+mapping clause csr_name_map = 0x140  <-> "sscratch"
+mapping clause csr_name_map = 0x142  <-> "scause"
+mapping clause csr_name_map = 0x143  <-> "stval"
+
+function clause is_CSR_defined(0x140) = extensionEnabled(Ext_S) // sscratch
+function clause is_CSR_defined(0x142) = extensionEnabled(Ext_S) // scause
+function clause is_CSR_defined(0x143) = extensionEnabled(Ext_S) // stval
+
+function clause read_CSR(0x140) = sscratch
+function clause read_CSR(0x142) = scause.bits
+function clause read_CSR(0x143) = stval
+
+function clause write_CSR(0x140, value) = { sscratch = value; sscratch }
+function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits }
+function clause write_CSR(0x143, value) = { stval = value; stval }
+
 /*
  * S-mode address translation and protection (satp) layout.
  * The actual satp register is defined in an architecture-specific file.

From 6b3a88ef017b4568dafd5ecd01ad0218260af049 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 22:41:20 -0700
Subject: [PATCH 15/17] Move MISA csr

---
 model/riscv_csr_begin.sail   | 1 -
 model/riscv_insts_zicsr.sail | 4 ----
 model/riscv_sys_control.sail | 2 --
 model/riscv_sys_regs.sail    | 5 +++++
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 2b10af29a..e520189b5 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -20,7 +20,6 @@ mapping clause csr_name_map = 0x105  <-> "stvec"
 /* supervisor trap handling */
 mapping clause csr_name_map = 0x141  <-> "sepc"
 /* machine trap setup */
-mapping clause csr_name_map = 0x301  <-> "misa"
 mapping clause csr_name_map = 0x305  <-> "mtvec"
 /* machine trap handling */
 mapping clause csr_name_map = 0x341  <-> "mepc"
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 38431d046..557b197b9 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -25,7 +25,6 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
 // corresponding to their extensions rather than all be here.
 
 /* machine mode */
-function clause read_CSR(0x301) = misa.bits
 function clause read_CSR(0x305) = get_mtvec()
 function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
 
@@ -33,9 +32,7 @@ function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
 function clause read_CSR(0x105) = get_stvec()
 function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask()
 
-
 /* machine mode */
-function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
 function clause write_CSR(0x305, value) = { set_mtvec(value) }
 function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
 
@@ -44,7 +41,6 @@ function clause write_CSR(0x105, value) = { set_stvec(value) }
 function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
 
 
-
 function clause execute CSR(csr, rs1, rd, is_imm, op) = {
   let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1);
   let isWrite : bool = match op {
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index d791f1c31..dafcea385 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -17,10 +17,8 @@ function csrPriv(csr : csreg) -> priv_level = csr[9..8]
 // corresponding to their extensions rather than all be here.
 
 /* machine mode: trap setup */
-function clause is_CSR_defined(0x301) = true // misa
 function clause is_CSR_defined(0x305) = true // mtvec
 
-
 /* machine mode: trap handling */
 function clause is_CSR_defined(0x341) = true // mepc
 
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 83889fa7c..1d9ecb6c2 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -136,6 +136,11 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
   }
 }
 
+mapping clause csr_name_map = 0x301  <-> "misa"
+function clause is_CSR_defined(0x301) = true // misa
+function clause read_CSR(0x301) = misa.bits
+function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits }
+
 enum clause extension = Ext_U
 function clause extensionEnabled(Ext_U) = misa[U] == 0b1
 

From 1353bab63c1ee641c3983397c7c4e77c10d805df Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 22:49:56 -0700
Subject: [PATCH 16/17] Move remaining trap CSRs

---
 model/riscv_csr_begin.sail      |  9 ---------
 model/riscv_insts_zicsr.sail    | 16 ----------------
 model/riscv_sys_control.sail    | 10 ----------
 model/riscv_sys_exceptions.sail | 20 ++++++++++++++++++++
 4 files changed, 20 insertions(+), 35 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index e520189b5..63b802f4c 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -15,15 +15,6 @@ scattered mapping csr_name_map
 // TODO: These csr_name_map definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* supervisor trap setup */
-mapping clause csr_name_map = 0x105  <-> "stvec"
-/* supervisor trap handling */
-mapping clause csr_name_map = 0x141  <-> "sepc"
-/* machine trap setup */
-mapping clause csr_name_map = 0x305  <-> "mtvec"
-/* machine trap handling */
-mapping clause csr_name_map = 0x341  <-> "mepc"
-
 val csr_name : csreg -> string
 overload to_str = {csr_name}
 
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 557b197b9..795ad1af3 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -24,22 +24,6 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
 // TODO: These read/write_CSR definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* machine mode */
-function clause read_CSR(0x305) = get_mtvec()
-function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
-
-/* supervisor mode */
-function clause read_CSR(0x105) = get_stvec()
-function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask()
-
-/* machine mode */
-function clause write_CSR(0x305, value) = { set_mtvec(value) }
-function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }
-
-/* supervisor mode */
-function clause write_CSR(0x105, value) = { set_stvec(value) }
-function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
-
 
 function clause execute CSR(csr, rs1, rd, is_imm, op) = {
   let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1);
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index dafcea385..a036d23cf 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -16,17 +16,7 @@ function csrPriv(csr : csreg) -> priv_level = csr[9..8]
 // TODO: These is_CSR_defined definitions should be moved to the files
 // corresponding to their extensions rather than all be here.
 
-/* machine mode: trap setup */
-function clause is_CSR_defined(0x305) = true // mtvec
 
-/* machine mode: trap handling */
-function clause is_CSR_defined(0x341) = true // mepc
-
-/* supervisor mode: trap setup */
-function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
-
-/* supervisor mode: trap handling */
-function clause is_CSR_defined(0x141) = extensionEnabled(Ext_S) // sepc
 
 
 
diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail
index 4e4b550ad..a4e5d6434 100644
--- a/model/riscv_sys_exceptions.sail
+++ b/model/riscv_sys_exceptions.sail
@@ -77,3 +77,23 @@ function set_stvec(value : xlenbits) -> xlenbits = {
   stvec = legalize_tvec(stvec, value);
   stvec.bits
 }
+
+mapping clause csr_name_map = 0x105  <-> "stvec"
+mapping clause csr_name_map = 0x141  <-> "sepc"
+mapping clause csr_name_map = 0x305  <-> "mtvec"
+mapping clause csr_name_map = 0x341  <-> "mepc"
+
+function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec
+function clause is_CSR_defined(0x141) = extensionEnabled(Ext_S) // sepc
+function clause is_CSR_defined(0x305) = true // mtvec
+function clause is_CSR_defined(0x341) = true // mepc
+
+function clause read_CSR(0x105) = get_stvec()
+function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask()
+function clause read_CSR(0x305) = get_mtvec()
+function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask()
+
+function clause write_CSR(0x105, value) = { set_stvec(value) }
+function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) }
+function clause write_CSR(0x305, value) = { set_mtvec(value) }
+function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) }

From 472456e0c9dccbd113a02338037ad778d8d02247 Mon Sep 17 00:00:00 2001
From: Jordan Carlin <jordanmcarlin@gmail.com>
Date: Sat, 12 Oct 2024 22:52:17 -0700
Subject: [PATCH 17/17] Cleanup CSR comments

---
 model/riscv_csr_begin.sail   | 11 -----------
 model/riscv_insts_zicsr.sail |  5 -----
 model/riscv_sys_control.sail |  7 -------
 3 files changed, 23 deletions(-)

diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail
index 63b802f4c..bedb657af 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -12,20 +12,9 @@ val csr_name_map : csreg <-> string
 
 scattered mapping csr_name_map
 
-// TODO: These csr_name_map definitions should be moved to the files
-// corresponding to their extensions rather than all be here.
-
 val csr_name : csreg -> string
 overload to_str = {csr_name}
 
-/* 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 exists
  */
 val is_CSR_defined : (csreg) -> bool
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 795ad1af3..0df999dcc 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -8,7 +8,6 @@
 
 /* ****************************************************************** */
 /* This file specifies the instructions in the 'Zicsr' extension.     */
-
 /* ****************************************************************** */
 union clause ast = CSR  : (csreg, regidx, regidx, bool, csrop)
 
@@ -21,10 +20,6 @@ mapping encdec_csrop : csrop <-> bits(2) = {
 mapping clause encdec = CSR(csr, rs1, rd, is_imm, op)
   <-> csr @ rs1 @ bool_bits(is_imm) @ encdec_csrop(op) @ rd @ 0b1110011
 
-// TODO: These read/write_CSR definitions should be moved to the files
-// corresponding to their extensions rather than all be here.
-
-
 function clause execute CSR(csr, rs1, rd, is_imm, op) = {
   let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1);
   let isWrite : bool = match op {
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index a036d23cf..d22e8d401 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -13,13 +13,6 @@
 function csrAccess(csr : csreg) -> csrRW = csr[11..10]
 function csrPriv(csr : csreg) -> priv_level = csr[9..8]
 
-// TODO: These is_CSR_defined definitions should be moved to the files
-// corresponding to their extensions rather than all be here.
-
-
-
-
-
 val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
 function check_CSR_access(csrrw, csrpr, p, isWrite) =
     not(isWrite == true & csrrw == 0b11)  /* read/write */