diff --git a/Makefile b/Makefile
index de2a9cdbf..3d8835260 100644
--- a/Makefile
+++ b/Makefile
@@ -73,7 +73,7 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 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_zihpm.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
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 6fd736846..fa3ad5fb4 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -547,38 +547,6 @@ function retire_instruction() -> unit = {
   if minstret_increment then minstret = minstret + 1;
 }
 
-// HPM (Hardware Performance Monitoring) counters. The lowest three values are
-// not used but they are defined for simplicity.
-register mhpmcounter : vector(32, bits(64))
-
-// HPM events selector. These control what the HPM counters measure. The lowest
-// three values are not used but they are defined for simplicity.
-register mhpmevent : vector(32, xlenbits)
-
-// Valid HPM counter indices. The lowest three are used for mcycle, mtime and minstret.
-type hpmidx = range(3, 31)
-
-// Convert the lowest 5 bits of a CSR index to an hpmidx. Asserts if it is 0..2.
-function hpmidx_from_bits(b : bits(5)) -> hpmidx = {
-  let index = unsigned(b);
-  assert(index >= 3, "unreachable HPM index");
-  index
-}
-
-function read_mhpmcounter(index : hpmidx) -> xlenbits = mhpmcounter[index][(xlen - 1) .. 0]
-function read_mhpmcounterh(index : hpmidx) -> bits(32) = mhpmcounter[index][63 .. 32]
-function read_mhpmevent(index : hpmidx) -> xlenbits = mhpmevent[index]
-
-// Write the HPM CSRs. These return the new value of the CSR, for use in writeCSR.
-function write_mhpmcounter(index : hpmidx, value : xlenbits) -> unit =
-  if sys_writable_hpm_counters()[index] == bitone then mhpmcounter[index][(xlen - 1) .. 0] = value
-
-function write_mhpmcounterh(index : hpmidx, value : bits(32)) -> unit =
-  if sys_writable_hpm_counters()[index] == bitone then mhpmcounter[index][63 .. 32] = value
-
-function write_mhpmevent(index : hpmidx, value : xlenbits) -> unit =
-  if sys_writable_hpm_counters()[index] == bitone then mhpmevent[index] = value
-
 /* machine information registers */
 register mvendorid : bits(32)
 register mimpid : xlenbits
diff --git a/model/riscv_hpm_control.sail b/model/riscv_zihpm.sail
similarity index 88%
rename from model/riscv_hpm_control.sail
rename to model/riscv_zihpm.sail
index 578d39869..1fba75267 100644
--- a/model/riscv_hpm_control.sail
+++ b/model/riscv_zihpm.sail
@@ -163,6 +163,38 @@ mapping clause csr_name_map = 0xB9D  <-> "mhpmcounter29h"
 mapping clause csr_name_map = 0xB9E  <-> "mhpmcounter30h"
 mapping clause csr_name_map = 0xB9F  <-> "mhpmcounter31h"
 
+// HPM (Hardware Performance Monitoring) counters. The lowest three values are
+// not used but they are defined for simplicity.
+register mhpmcounter : vector(32, bits(64))
+
+// HPM events selector. These control what the HPM counters measure. The lowest
+// three values are not used but they are defined for simplicity.
+register mhpmevent : vector(32, xlenbits)
+
+// Valid HPM counter indices. The lowest three are used for mcycle, mtime and minstret.
+type hpmidx = range(3, 31)
+
+// Convert the lowest 5 bits of a CSR index to an hpmidx. Asserts if it is 0..2.
+function hpmidx_from_bits(b : bits(5)) -> hpmidx = {
+  let index = unsigned(b);
+  assert(index >= 3, "unreachable HPM index");
+  index
+}
+
+function read_mhpmcounter(index : hpmidx) -> xlenbits = mhpmcounter[index][(xlen - 1) .. 0]
+function read_mhpmcounterh(index : hpmidx) -> bits(32) = mhpmcounter[index][63 .. 32]
+function read_mhpmevent(index : hpmidx) -> xlenbits = mhpmevent[index]
+
+// Write the HPM CSRs. These return the new value of the CSR, for use in writeCSR.
+function write_mhpmcounter(index : hpmidx, value : xlenbits) -> unit =
+  if sys_writable_hpm_counters()[index] == bitone then mhpmcounter[index][(xlen - 1) .. 0] = value
+
+function write_mhpmcounterh(index : hpmidx, value : bits(32)) -> unit =
+  if sys_writable_hpm_counters()[index] == bitone then mhpmcounter[index][63 .. 32] = value
+
+function write_mhpmevent(index : hpmidx, value : xlenbits) -> unit =
+  if sys_writable_hpm_counters()[index] == bitone then mhpmevent[index] = value
+
 /* 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))