diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index 253da353f..f4f35a09b 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -62,6 +62,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 38fac2f07..aec32426f 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -8,6 +8,7 @@ bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(unit);
 bool sys_enable_vext(unit);
+mach_bits sys_writable_hpm_counters(unit u);
 
 uint64_t sys_pmp_count(unit);
 uint64_t sys_pmp_grain(unit);
diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c
index c2ae256ef..e0b511e20 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -12,6 +12,7 @@ bool rv_enable_next = false;
 bool rv_enable_writable_misa = true;
 bool rv_enable_fdext = true;
 bool rv_enable_vext = true;
+uint64_t rv_writable_hpm_counters = 0xFFFFFFFF;
 
 bool rv_enable_dirty_update = false;
 bool rv_enable_misaligned = false;
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index e3e4a9678..2d68a1ad6 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -16,6 +16,7 @@ extern bool rv_enable_rvc;
 extern bool rv_enable_next;
 extern bool rv_enable_fdext;
 extern bool rv_enable_vext;
+extern uint64_t rv_writable_hpm_counters;
 extern bool rv_enable_writable_misa;
 extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
diff --git a/model/prelude.sail b/model/prelude.sail
index 3edec051d..d3b414497 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -178,22 +178,31 @@ val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
 function to_bits (l, n) = get_slice_int(l, n, 0)
 
 infix 4 <_s
+infix 4 >_s
+infix 4 <=_s
 infix 4 >=_s
 infix 4 <_u
-infix 4 >=_u
+infix 4 >_u
 infix 4 <=_u
+infix 4 >=_u
 
 val operator <_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator >_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator <=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
 val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
 val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
-val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
+val operator >_u  : forall 'n. (bits('n), bits('n)) -> bool
 val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
 
 function operator <_s  (x, y) = signed(x) < signed(y)
+function operator >_s  (x, y) = signed(x) > signed(y)
+function operator <=_s (x, y) = signed(x) <= signed(y)
 function operator >=_s (x, y) = signed(x) >= signed(y)
 function operator <_u  (x, y) = unsigned(x) < unsigned(y)
-function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
+function operator >_u  (x, y) = unsigned(x) > unsigned(y)
 function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
+function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
 
 infix 7 >>
 infix 7 <<
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index dcc865117..71d630a27 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -94,10 +94,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"
@@ -113,6 +172,8 @@ 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"
@@ -127,6 +188,37 @@ 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"
+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 envcfg */
+mapping clause csr_name_map = 0x30A  <-> "menvcfg"
 /* machine trap handling */
 mapping clause csr_name_map = 0x340  <-> "mscratch"
 mapping clause csr_name_map = 0x341  <-> "mepc"
@@ -217,9 +309,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 6aa512ea2..9c5198de9 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -103,6 +103,9 @@ function readCSR csr : csreg -> xlenbits = {
     (0x31A, 32) => menvcfg.bits[63 .. 32],
     (0x320,  _) => zero_extend(mcountinhibit.bits),
 
+    /* High Performance Monitoring event selection */
+    (0b0011001 /* 0x320 */ @ index : bits(5), _) if index >_u 0b00010 => read_mhpmevent(hpmidx_from_bits(index)),
+
     (0x340,  _) => mscratch,
     (0x341,  _) => get_xret_target(Machine) & pc_alignment_mask(),
     (0x342,  _) => mcause.bits,
@@ -123,6 +126,10 @@ function readCSR csr : csreg -> xlenbits = {
     (0xB80, 32) => mcycle[63 .. 32],
     (0xB82, 32) => minstret[63 .. 32],
 
+    /* High Performance Monitoring machine mode counters */
+    (0b1011000 /* 0xB00 */ @ index : bits(5), _) if index >_u 0b00010 => read_mhpmcounter(hpmidx_from_bits(index)),
+    (0b1011100 /* 0xB80 */ @ index : bits(5), 32) if index >_u 0b00010 => read_mhpmcounterh(hpmidx_from_bits(index)),
+
     /* vector */
     (0x008, _) => zero_extend(vstart),
     (0x009, _) => zero_extend(vxsat),
@@ -158,6 +165,10 @@ function readCSR csr : csreg -> xlenbits = {
     (0xC81, 32) => mtime[63 .. 32],
     (0xC82, 32) => minstret[63 .. 32],
 
+    /* High Performance Monitoring user mode counters */
+    (0b1100000 /* 0xC00 */ @ index : bits(5), _) if index >_u 0b00010 => read_mhpmcounter(hpmidx_from_bits(index)),
+    (0b1100100 /* 0xC80 */ @ index : bits(5), 32) if index >_u 0b00010 => read_mhpmcounterh(hpmidx_from_bits(index)),
+
     /* user mode: Zkr */
     (0x015,  _) => read_seed_csr(),
 
@@ -213,6 +224,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) },
 
+    /* High Performance Monitoring machine mode counters */
+    (0b0011001 /* 0x320 */ @ index : bits(5), _) if index >_u 0b00010 => {
+      let index = hpmidx_from_bits(index);
+      write_mhpmevent(index, value);
+      Some(read_mhpmevent(index))
+    },
+    (0b1011000 /* 0xB00 */ @ index : bits(5), _) if index >_u 0b00010 => {
+      let index = hpmidx_from_bits(index);
+      write_mhpmcounter(index, value);
+      Some(read_mhpmcounter(index))
+    },
+    (0b1011100 /* 0xB80 */ @ index : bits(5), 32) if index >_u 0b00010 => {
+      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 4dfe36539..5f3755f5b 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -110,12 +110,20 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x3C @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b01 @ idx),
     0x3D @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b10 @ idx),
     0x3E @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(0b11 @ idx),
+
+    /* counters */
+    0b0011001 /* 0x320 */ @ index : bits(5) if index >_u 0b00010 => p == Machine, // mhpmevent3..31
+
     0xB00 => p == Machine, // mcycle
     0xB02 => p == Machine, // minstret
 
+    0b1011000 /* 0xB00 */ @ index : bits(5) if index >_u 0b00010 => p == Machine, // mhpmcounter3..31
+
     0xB80 => p == Machine & (sizeof(xlen) == 32), // mcycleh
     0xB82 => p == Machine & (sizeof(xlen) == 32), // minstreth
 
+    0b1011100 /* 0xB80 */ @ index : bits(5) if index >_u 0b00010 => p == Machine & (sizeof(xlen) == 32), // mhpmcounterh3..31
+
     /* disabled trigger/debug module */
     0x7a0 => p == Machine,
 
@@ -143,10 +151,14 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0xC01 => haveUsrMode(),    // time
     0xC02 => haveUsrMode(),    // instret
 
+    0b1100000 /* 0xC00 */ @ index : bits(5) if index >_u 0b00010 => haveUsrMode(), // mhpmcounter3..31
+
     0xC80 => haveUsrMode() & (sizeof(xlen) == 32),     // cycleh
     0xC81 => haveUsrMode() & (sizeof(xlen) == 32),     // timeh
     0xC82 => haveUsrMode() & (sizeof(xlen) == 32),     // instreth
 
+    0b1100100 /* 0xC80 */ @ index : bits(5) if index >_u 0b00010 => haveUsrMode() & (sizeof(xlen) == 32), // mhpmcounterh3..31
+
     /* user mode: Zkr */
     0x015 => haveZkr(),
 
@@ -162,22 +174,24 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) =
 function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
   not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1)
 
-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,
+// There are several features that are controlled by machine/supervisor enable
+// bits (m/senvcfg, m/scounteren, etc.). This abstracts that logic.
+function mode_bit_enabled(p : Privilege, machine_bit : bit, supervisor_bit : bit) -> bool = match p {
+  Machine => true,
+  Supervisor => machine_bit == bitone,
+  User => machine_bit == bitone & (not(haveSupMode()) | supervisor_bit == bitone),
+}
 
-    (0xC00, User) => mcounteren[CY] == 0b1 & (not(haveSupMode()) | scounteren[CY] == 0b1),
-    (0xC01, User) => mcounteren[TM] == 0b1 & (not(haveSupMode()) | scounteren[TM] == 0b1),
-    (0xC02, User) => mcounteren[IR] == 0b1 & (not(haveSupMode()) | 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 | csr >_u 0xC1F
+  then return true;
 
+  // Check the relevant bit in m/scounteren.
+  let index = unsigned(csr[4 .. 0]);
+  mode_bit_enabled(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 c98584bc0..406915301 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -160,6 +160,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
 
@@ -523,24 +526,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)
@@ -566,6 +571,40 @@ function retire_instruction() -> unit = {
   if minstret_increment then minstret = minstret + 1;
 }
 
+// HPM (High 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);
+  if index >= 3 then index else {
+    assert(false, "unreachable HPM index");
+    undefined
+  }
+}
+
+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 a8bde44d6..b804e71d6 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -17,6 +17,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 0xFFFFFFFF
 
 let platform_arch = ref P.RV64
 
@@ -85,6 +86,7 @@ let enable_rvc ()                    = !config_enable_rvc
 let enable_next ()                   = !config_enable_next
 let enable_fdext ()                  = false
 let enable_vext ()                   = !config_enable_vext
+let writable_hpm_counters ()         = !config_writable_hpm_counters
 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