diff --git a/Makefile b/Makefile
index e97081e29..de2a9cdbf 100644
--- a/Makefile
+++ b/Makefile
@@ -70,10 +70,12 @@ 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
+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
 
@@ -96,7 +98,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 053776435..bedb657af 100644
--- a/model/riscv_csr_begin.sail
+++ b/model/riscv_csr_begin.sail
@@ -12,320 +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.
-
-/* 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 */
-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"
-mapping clause csr_name_map = 0x104  <-> "sie"
-mapping clause csr_name_map = 0x105  <-> "stvec"
-mapping clause csr_name_map = 0x106  <-> "scounteren"
-/* supervisor trap handling */
-mapping clause csr_name_map = 0x140  <-> "sscratch"
-mapping clause csr_name_map = 0x141  <-> "sepc"
-mapping clause csr_name_map = 0x142  <-> "scause"
-mapping clause csr_name_map = 0x143  <-> "stval"
-mapping clause csr_name_map = 0x144  <-> "sip"
-/* supervisor protection and translation */
-mapping clause csr_name_map = 0x180  <-> "satp"
-/* 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"
-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 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"
-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"
-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"
-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}
 
-/* 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_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)
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..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,159 +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.
-
-/* 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
-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)
-
-/* 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
-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]
-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 */
-
-/* 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(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
-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]
-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]
-
-/* 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()
-
-/* 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(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) }
-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 }
-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 }
-
-/* 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(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 }
-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()
-
 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_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 6379f5676..d22e8d401 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -8,103 +8,11 @@
 
 /* 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]
 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
-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(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
-
-
-/* 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
-
-// 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(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
-
-/* 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
-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
-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
-
-/* 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
-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)
-
-
 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 */
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) }
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 4e810d762..1d9ecb6c2 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -136,16 +136,17 @@ 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
 
 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.
@@ -276,6 +277,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 = {
@@ -307,9 +319,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'
@@ -354,13 +363,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 = {
@@ -383,6 +416,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) = {
@@ -419,6 +456,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) = {
@@ -428,25 +477,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.
@@ -454,6 +515,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)
 
@@ -509,7 +576,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
@@ -517,6 +584,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 */
@@ -585,6 +670,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 = {
@@ -595,6 +684,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());
@@ -628,6 +718,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;
@@ -643,6 +740,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
@@ -650,6 +753,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.
@@ -684,26 +803,14 @@ function legalize_satp32(a : Architecture, o : bits(32), v : bits(32)) -> bits(3
 /* disabled trigger/debug module */
 register tselect : xlenbits
 
-/*
- * 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 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"
 
-/* Mapping of status codes and their actual encodings. */
-mapping opst_code : seed_opst <-> bits(2) = {
-  BIST <-> 0b00,
-  WAIT <-> 0b01,
-  ES16 <-> 0b10,
-  DEAD <-> 0b11
-}
+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 }
 
 /*
  * Entropy Source - Platform access to random bits.
@@ -721,21 +828,7 @@ 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
   STCE   : 63,
@@ -768,9 +861,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];
@@ -785,6 +875,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.
@@ -795,6 +905,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
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
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
 
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 }
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()