From 661228ad1751ec87bca390408d6003b91cd79cf3 Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Mon, 12 Feb 2024 10:40:02 +0000
Subject: [PATCH] Add support for HPM counters

Implements Hardware Performance Monitoring counters, but only by making the registers available. Their values only change if explicitly written to and all values are legal.

All 32 HPM counters are always implemented (the spec says this "should" be the case), and a platform callback `sys_writable_hpm_counters` is added to allow making any of them read-only. I haven't hooked `sys_writable_hpm_counters` up to CLI flags because Codasip does not use the CLI flags and it is quite tedious, and hopefully going to change when riscv-config is used.

Finally this adds `menvcfg` and `senvcfg` to the CSR name map which I forgot to do previously.
---
 c_emulator/riscv_platform.c      |   5 ++
 c_emulator/riscv_platform.h      |   1 +
 c_emulator/riscv_platform_impl.c |   1 +
 c_emulator/riscv_platform_impl.h |   1 +
 model/riscv_csr_map.sail         | 150 ++++++++++++++++++++++++++++++-
 model/riscv_insts_zicsr.sail     |  28 ++++++
 model/riscv_sys_control.sail     |  42 ++++++---
 model/riscv_sys_regs.sail        |  54 +++++++++--
 ocaml_emulator/platform.ml       |   2 +
 9 files changed, 262 insertions(+), 22 deletions(-)

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/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 9e3e8045b..ea9338c1f 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"
@@ -69,6 +128,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"
@@ -159,9 +248,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 ef9e73e11..7988ebe2f 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -41,6 +41,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,
@@ -61,6 +64,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),
@@ -96,6 +103,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(),
 
@@ -151,6 +162,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 ecc53ae85..27bb7e83e 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -48,12 +48,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 unsigned(index) >= 3 => haveZihpm() & p == Machine, // mhpmevent3..31
+
     0xB00 => p == Machine, // mcycle
     0xB02 => p == Machine, // minstret
 
+    0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3 => haveZihpm() & p == Machine, // mhpmcounter3..31
+
     0xB80 => p == Machine & (sizeof(xlen) == 32), // mcycleh
     0xB82 => p == Machine & (sizeof(xlen) == 32), // minstreth
 
+    0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3 => haveZihpm() & p == Machine & (sizeof(xlen) == 32), // mhpmcounterh3..31
+
     /* disabled trigger/debug module */
     0x7a0 => p == Machine,
 
@@ -81,10 +89,14 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0xC01 => haveUsrMode(),    // time
     0xC02 => haveUsrMode(),    // instret
 
+    0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3 => haveZihpm() & haveUsrMode(), // hpmcounter3..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 unsigned(index) >= 3 => haveZihpm() & haveUsrMode() & (sizeof(xlen) == 32), // hpmcounterh3..31
+
     /* user mode: Zkr */
     0x015 => haveZkr(),
 
@@ -100,22 +112,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 feature_enabled_for_priv(p : Privilege, machine_enable_bit : bit, supervisor_enable_bit : bit) -> bool = match p {
+  Machine => true,
+  Supervisor => machine_enable_bit == bitone,
+  User => machine_enable_bit == bitone & (not(haveSupMode()) | supervisor_enable_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 | 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 fc20e4af4..04ca60f67 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -98,6 +98,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
 
@@ -160,6 +163,9 @@ function haveZmmul()  -> bool = true
 /* Zicond extension support */
 function haveZicond() -> bool = true
 
+/* Hardware Performance Monitoring counters */
+function haveZihpm()  -> bool = true
+
 bitfield Mstatush : bits(32) = {
   MBE  : 5,
   SBE  : 4
@@ -461,24 +467,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)
@@ -504,6 +512,40 @@ 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);
+  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..cc87cc11e 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 (ones (Big_int.of_int 32))
 
 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