diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index cbd3ae319..691b1efb3 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -87,6 +87,11 @@ bool sys_enable_writable_misa(unit u)
   return rv_enable_writable_misa;
 }
 
+mach_bits sys_writable_hpm_counters(unit u)
+{
+  return rv_writable_hpm_counters;
+}
+
 bool plat_enable_dirty_update(unit u)
 {
   return rv_enable_dirty_update;
diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h
index 58792319c..5f145b778 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -20,6 +20,7 @@ uint64_t sys_pmp_grain(unit);
 bool plat_enable_dirty_update(unit);
 bool plat_enable_misaligned_access(unit);
 bool plat_mtval_has_illegal_inst_bits(unit);
+mach_bits sys_writable_hpm_counters(unit u);
 
 mach_bits plat_ram_base(unit);
 mach_bits plat_ram_size(unit);
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index a76e683d4..4ae06c03e 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -22,6 +22,7 @@ bool rv_enable_dirty_update = false;
 bool rv_enable_misaligned = false;
 bool rv_mtval_has_illegal_inst_bits = false;
 bool rv_enable_writable_fiom = true;
+uint64_t rv_writable_hpm_counters = 0xFFFFFFFF;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x4000000);
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index d8acd3b59..367806be9 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -26,6 +26,7 @@ extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
 extern bool rv_mtval_has_illegal_inst_bits;
 extern bool rv_enable_writable_fiom;
+extern uint64_t rv_writable_hpm_counters;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 6478919ca..520d7e74b 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -32,10 +32,69 @@ 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"
-/* TODO: other hpm counters */
+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 = 0x102  <-> "sedeleg"
@@ -70,6 +129,36 @@ mapping clause csr_name_map = 0x306  <-> "mcounteren"
 mapping clause csr_name_map = 0x320  <-> "mcountinhibit"
 /* machine envcfg */
 mapping clause csr_name_map = 0x30A  <-> "menvcfg"
+/* 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"
@@ -160,9 +249,66 @@ 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"
-/* TODO: other hpm counters and events */
+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_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index f2980fb9e..fb2869613 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -42,6 +42,9 @@ function readCSR csr : csreg -> xlenbits = {
     (0x31A, 32) => menvcfg.bits[63 .. 32],
     (0x320,  _) => zero_extend(mcountinhibit.bits),
 
+    /* Hardware Performance Monitoring event selection */
+    (0b0011001 /* 0x320 */ @ index : bits(5), _) if unsigned(index) >= 3 => read_mhpmevent(hpmidx_from_bits(index)),
+
     (0x340,  _) => mscratch,
     (0x341,  _) => get_xret_target(Machine) & pc_alignment_mask(),
     (0x342,  _) => mcause.bits,
@@ -62,6 +65,10 @@ function readCSR csr : csreg -> xlenbits = {
     (0xB80, 32) => mcycle[63 .. 32],
     (0xB82, 32) => minstret[63 .. 32],
 
+    /* Hardware Performance Monitoring machine mode counters */
+    (0b1011000 /* 0xB00 */ @ index : bits(5), _) if unsigned(index) >= 3 => read_mhpmcounter(hpmidx_from_bits(index)),
+    (0b1011100 /* 0xB80 */ @ index : bits(5), 32) if unsigned(index) >= 3 => read_mhpmcounterh(hpmidx_from_bits(index)),
+
     /* vector */
     (0x008, _) => zero_extend(vstart),
     (0x009, _) => zero_extend(vxsat),
@@ -97,6 +104,10 @@ function readCSR csr : csreg -> xlenbits = {
     (0xC81, 32) => mtime[63 .. 32],
     (0xC82, 32) => minstret[63 .. 32],
 
+    /* Hardware Performance Monitoring user mode counters */
+    (0b1100000 /* 0xC00 */ @ index : bits(5), _) if unsigned(index) >= 3 => read_mhpmcounter(hpmidx_from_bits(index)),
+    (0b1100100 /* 0xC80 */ @ index : bits(5), 32) if unsigned(index) >= 3 => read_mhpmcounterh(hpmidx_from_bits(index)),
+
     /* user mode: Zkr */
     (0x015,  _) => read_seed_csr(),
 
@@ -152,6 +163,23 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) },
     (0xB82, 32) => { minstret[63 .. 32] = value; minstret_increment = false; Some(value) },
 
+    /* Hardware Performance Monitoring machine mode counters */
+    (0b0011001 /* 0x320 */ @ index : bits(5), _) if unsigned(index) >= 3 => {
+      let index = hpmidx_from_bits(index);
+      write_mhpmevent(index, value);
+      Some(read_mhpmevent(index))
+    },
+    (0b1011000 /* 0xB00 */ @ index : bits(5), _) if unsigned(index) >= 3 => {
+      let index = hpmidx_from_bits(index);
+      write_mhpmcounter(index, value);
+      Some(read_mhpmcounter(index))
+    },
+    (0b1011100 /* 0xB80 */ @ index : bits(5), 32) if unsigned(index) >= 3 => {
+      let index = hpmidx_from_bits(index);
+      write_mhpmcounterh(index, value);
+      Some(read_mhpmcounterh(index))
+    },
+
     /* trigger/debug */
     (0x7a0,  _) => { tselect = value; Some(tselect) },
 
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 2cd5df2be..ce4e0175a 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -51,12 +51,20 @@ function is_CSR_defined (csr : csreg) -> bool =
     0x3C @ idx : bits(4) => sys_pmp_count() > unsigned(0b01 @ idx),
     0x3D @ idx : bits(4) => sys_pmp_count() > unsigned(0b10 @ idx),
     0x3E @ idx : bits(4) => sys_pmp_count() > unsigned(0b11 @ idx),
+
+    /* counters */
+    0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm), // mhpmevent3..31
+
     0xB00 => true, // mcycle
     0xB02 => true, // minstret
 
+    0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm), // mhpmcounter3..31
+
     0xB80 => sizeof(xlen) == 32, // mcycleh
     0xB82 => sizeof(xlen) == 32, // minstreth
 
+    0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm) & (sizeof(xlen) == 32), // mhpmcounterh3..31
+
     /* disabled trigger/debug module */
     0x7a0 => true,
 
@@ -84,10 +92,14 @@ function is_CSR_defined (csr : csreg) -> bool =
     0xC01 => extensionEnabled(Ext_U),    // time
     0xC02 => extensionEnabled(Ext_U),    // instret
 
+    0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U), // hpmcounter3..31
+
     0xC80 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32),     // cycleh
     0xC81 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32),     // timeh
     0xC82 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32),     // instreth
 
+    0b1100100 /* 0xC80 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // hpmcounterh3..31
+
     /* user mode: Zkr */
     0x015 => extensionEnabled(Ext_Zkr),
 
@@ -111,22 +123,16 @@ function feature_enabled_for_priv(p : Privilege, machine_enable_bit : bit, super
   User => machine_enable_bit == bitone & (not(extensionEnabled(Ext_S)) | supervisor_enable_bit == bitone),
 }
 
-function check_Counteren(csr : csreg, p : Privilege) -> bool =
-  match(csr, p) {
-    (0xC00, Supervisor) => mcounteren[CY] == 0b1,
-    (0xC01, Supervisor) => mcounteren[TM] == 0b1,
-    (0xC02, Supervisor) => mcounteren[IR] == 0b1,
-
-    (0xC00, User) => mcounteren[CY] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[CY] == 0b1),
-    (0xC01, User) => mcounteren[TM] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[TM] == 0b1),
-    (0xC02, User) => mcounteren[IR] == 0b1 & (not(extensionEnabled(Ext_S)) | scounteren[IR] == 0b1),
-
-    (_, _) => /* no HPM counters for now */
-              if   0xC03 <=_u csr & csr <=_u 0xC1F
-              then false
-              else true
-  }
+// Return true if the counter is enabled OR the CSR is not a counter.
+function check_Counteren(csr : csreg, p : Privilege) -> bool = {
+  // Check if it is not a counter.
+  if csr <_u 0xC00 | 0xC1F <_u csr
+  then return true;
 
+  // Check the relevant bit in m/scounteren.
+  let index = unsigned(csr[4 .. 0]);
+  feature_enabled_for_priv(p, mcounteren.bits[index], scounteren.bits[index])
+}
 
 /* Seed may only be accessed if we are doing a write, and access has been
  * allowed in the current priv mode
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 6d1afd0ee..452670e31 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -102,6 +102,9 @@ val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pm
    G=0 -> 4 bytes, G=10 -> 4096 bytes. */
 val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63)
 
+/* Which HPM counters are supported (as a bit mask). Bits [2 .. 0] are ignored. */
+val sys_writable_hpm_counters = {c: "sys_writable_hpm_counters", ocaml: "Platform.writable_hpm_counters", _: "sys_writable_hpm_counters"} : unit -> bits(32)
+
 /* whether misa.v was enabled at boot */
 val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool
 
@@ -142,6 +145,10 @@ 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.
@@ -449,24 +456,26 @@ register mcounteren : Counteren
 register scounteren : Counteren
 
 function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
-  /* no HPM counters yet */
-  [c with IR = [v[2]], TM = [v[1]], CY = [v[0]]]
+  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 = {
-  /* no HPM counters yet */
-  [c with IR = [v[2]], TM = [v[1]], CY = [v[0]]]
+  let supported_counters = sys_writable_hpm_counters()[31 .. 3] @ 0b111;
+  Mk_Counteren(v[31 .. 0] & supported_counters)
 }
 
 bitfield Counterin : bits(32) = {
-  /* no HPM counters yet */
+  HPM  : 31 .. 3,
   IR : 2,
   CY : 0
 }
 register mcountinhibit : Counterin
 
 function legalize_mcountinhibit(c : Counterin, v : xlenbits) -> Counterin = {
-  [c with IR = [v[2]], CY = [v[0]]]
+  // Note the 0 in 0b101 is because the mtimer counter can't be paused.
+  let supported_counters = sys_writable_hpm_counters()[31 .. 3] @ 0b101;
+  Mk_Counterin(v[31 .. 0] & supported_counters)
 }
 
 register mcycle : bits(64)
@@ -492,6 +501,38 @@ 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, dec, 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, dec, 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][(sizeof(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][(sizeof(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
+
 /* informational registers */
 register mvendorid : bits(32)
 register mimpid : xlenbits
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index b9921a0c3..681dd2783 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -22,6 +22,7 @@ let config_pmp_grain                   = ref Big_int.zero
 
 let set_config_pmp_count x = config_pmp_count := Big_int.of_int x
 let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x
+let config_writable_hpm_counters       = ref (ones (Big_int.of_int 32))
 
 let platform_arch = ref P.RV64
 
@@ -102,6 +103,7 @@ let enable_zicboz ()                 = !config_enable_zicboz
 let enable_dirty_update ()           = !config_enable_dirty_update
 let enable_misaligned_access ()      = !config_enable_misaligned_access
 let mtval_has_illegal_inst_bits ()   = !config_mtval_has_illegal_inst_bits
+let writable_hpm_counters ()         = !config_writable_hpm_counters
 let enable_svinval ()                = !config_enable_svinval
 let enable_zcb ()                    = !config_enable_zcb
 let enable_zfinx ()                  = false