added hpm CSRs. compiles. but no significant functionality at this point

4 files changed, 541 insertions, 14 deletions

diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 31872d3..01e4609 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -163,6 +163,126 @@ 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"
+/* hpm counters and events */
+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"
+
+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"
+
+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"
 
 val csr_name : csreg -> string
 overload to_str = {csr_name}
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 08c7a19..d02fc39 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -99,6 +99,36 @@ function readCSR csr : csreg -> xlenbits = {
     (0x310, 32) => mstatush.bits(),
     (0x320,  _) => EXTZ(mcountinhibit.bits()),
 
+    (0x323,  _) => mhpmevents[0],
+    (0x324,  _) => mhpmevents[1],
+    (0x325,  _) => mhpmevents[2],
+    (0x326,  _) => mhpmevents[3],
+    (0x327,  _) => mhpmevents[4],
+    (0x328,  _) => mhpmevents[5],
+    (0x329,  _) => mhpmevents[6],
+    (0x32A,  _) => mhpmevents[7],
+    (0x32B,  _) => mhpmevents[8],
+    (0x32C,  _) => mhpmevents[9],
+    (0x32D,  _) => mhpmevents[10],
+    (0x32E,  _) => mhpmevents[11],
+    (0x32F,  _) => mhpmevents[12],
+    (0x330,  _) => mhpmevents[13],
+    (0x331,  _) => mhpmevents[14],
+    (0x332,  _) => mhpmevents[15],
+    (0x333,  _) => mhpmevents[16],
+    (0x334,  _) => mhpmevents[17],
+    (0x335,  _) => mhpmevents[18],
+    (0x336,  _) => mhpmevents[19],
+    (0x337,  _) => mhpmevents[20],
+    (0x338,  _) => mhpmevents[21],
+    (0x339,  _) => mhpmevents[22],
+    (0x33A,  _) => mhpmevents[23],
+    (0x33B,  _) => mhpmevents[24],
+    (0x33C,  _) => mhpmevents[25],
+    (0x33D,  _) => mhpmevents[26],
+    (0x33E,  _) => mhpmevents[27],
+    (0x33F,  _) => mhpmevents[28],
+
     (0x340,  _) => mscratch,
     (0x341,  _) => get_xret_target(Machine) & pc_alignment_mask(),
     (0x342,  _) => mcause.bits(),
@@ -130,8 +160,67 @@ function readCSR csr : csreg -> xlenbits = {
     /* machine mode counters */
     (0xB00,  _) => mcycle[(sizeof(xlen) - 1) .. 0],
     (0xB02,  _) => minstret[(sizeof(xlen) - 1) .. 0],
+    (0xB03,  _) => mhpmcounters[0][(sizeof(xlen) - 1) .. 0],
+    (0xB04,  _) => mhpmcounters[1][(sizeof(xlen) - 1) .. 0],
+    (0xB05,  _) => mhpmcounters[2][(sizeof(xlen) - 1) .. 0],
+    (0xB06,  _) => mhpmcounters[3][(sizeof(xlen) - 1) .. 0],
+    (0xB07,  _) => mhpmcounters[4][(sizeof(xlen) - 1) .. 0],
+    (0xB08,  _) => mhpmcounters[5][(sizeof(xlen) - 1) .. 0],
+    (0xB09,  _) => mhpmcounters[6][(sizeof(xlen) - 1) .. 0],
+    (0xB0A,  _) => mhpmcounters[7][(sizeof(xlen) - 1) .. 0],
+    (0xB0B,  _) => mhpmcounters[8][(sizeof(xlen) - 1) .. 0],
+    (0xB0C,  _) => mhpmcounters[9][(sizeof(xlen) - 1) .. 0],
+    (0xB0D,  _) => mhpmcounters[10][(sizeof(xlen) - 1) .. 0],
+    (0xB0E,  _) => mhpmcounters[11][(sizeof(xlen) - 1) .. 0],
+    (0xB0F,  _) => mhpmcounters[12][(sizeof(xlen) - 1) .. 0],
+    (0xB10,  _) => mhpmcounters[13][(sizeof(xlen) - 1) .. 0],
+    (0xB11,  _) => mhpmcounters[14][(sizeof(xlen) - 1) .. 0],
+    (0xB12,  _) => mhpmcounters[15][(sizeof(xlen) - 1) .. 0],
+    (0xB13,  _) => mhpmcounters[16][(sizeof(xlen) - 1) .. 0],
+    (0xB14,  _) => mhpmcounters[17][(sizeof(xlen) - 1) .. 0],
+    (0xB15,  _) => mhpmcounters[18][(sizeof(xlen) - 1) .. 0],
+    (0xB16,  _) => mhpmcounters[19][(sizeof(xlen) - 1) .. 0],
+    (0xB17,  _) => mhpmcounters[20][(sizeof(xlen) - 1) .. 0],
+    (0xB18,  _) => mhpmcounters[21][(sizeof(xlen) - 1) .. 0],
+    (0xB19,  _) => mhpmcounters[22][(sizeof(xlen) - 1) .. 0],
+    (0xB1A,  _) => mhpmcounters[23][(sizeof(xlen) - 1) .. 0],
+    (0xB1B,  _) => mhpmcounters[24][(sizeof(xlen) - 1) .. 0],
+    (0xB1C,  _) => mhpmcounters[25][(sizeof(xlen) - 1) .. 0],
+    (0xB1D,  _) => mhpmcounters[26][(sizeof(xlen) - 1) .. 0],
+    (0xB1E,  _) => mhpmcounters[27][(sizeof(xlen) - 1) .. 0],
+    (0xB1F,  _) => mhpmcounters[28][(sizeof(xlen) - 1) .. 0],
+
     (0xB80, 32) => mcycle[63 .. 32],
     (0xB82, 32) => minstret[63 .. 32],
+    (0xB83, 32) => mhpmcounters[0][63 .. 32],
+    (0xB84, 32) => mhpmcounters[1][63 .. 32],
+    (0xB85, 32) => mhpmcounters[2][63 .. 32],
+    (0xB86, 32) => mhpmcounters[3][63 .. 32],
+    (0xB87, 32) => mhpmcounters[4][63 .. 32],
+    (0xB88, 32) => mhpmcounters[5][63 .. 32],
+    (0xB89, 32) => mhpmcounters[6][63 .. 32],
+    (0xB8A, 32) => mhpmcounters[7][63 .. 32],
+    (0xB8B, 32) => mhpmcounters[8][63 .. 32],
+    (0xB8C, 32) => mhpmcounters[9][63 .. 32],
+    (0xB8D, 32) => mhpmcounters[10][63 .. 32],
+    (0xB8E, 32) => mhpmcounters[11][63 .. 32],
+    (0xB8F, 32) => mhpmcounters[12][63 .. 32],
+    (0xB90, 32) => mhpmcounters[13][63 .. 32],
+    (0xB91, 32) => mhpmcounters[14][63 .. 32],
+    (0xB92, 32) => mhpmcounters[15][63 .. 32],
+    (0xB93, 32) => mhpmcounters[16][63 .. 32],
+    (0xB94, 32) => mhpmcounters[17][63 .. 32],
+    (0xB95, 32) => mhpmcounters[18][63 .. 32],
+    (0xB96, 32) => mhpmcounters[19][63 .. 32],
+    (0xB97, 32) => mhpmcounters[20][63 .. 32],
+    (0xB98, 32) => mhpmcounters[21][63 .. 32],
+    (0xB99, 32) => mhpmcounters[22][63 .. 32],
+    (0xB9A, 32) => mhpmcounters[23][63 .. 32],
+    (0xB9B, 32) => mhpmcounters[24][63 .. 32],
+    (0xB9C, 32) => mhpmcounters[25][63 .. 32],
+    (0xB9D, 32) => mhpmcounters[26][63 .. 32],
+    (0xB9E, 32) => mhpmcounters[27][63 .. 32],
+    (0xB9F, 32) => mhpmcounters[28][63 .. 32],
 
     /* trigger/debug */
     (0x7a0,  _) => ~(tselect),  /* this indicates we don't have any trigger support */
@@ -154,6 +243,36 @@ function readCSR csr : csreg -> xlenbits = {
     (0xC00,  _) => mcycle[(sizeof(xlen) - 1) .. 0],
     (0xC01,  _) => mtime[(sizeof(xlen) - 1) .. 0],
     (0xC02,  _) => minstret[(sizeof(xlen) - 1) .. 0],
+    (0xC03,  _) => mhpmcounters[0][(sizeof(xlen) - 1) .. 0],
+    (0xC04,  _) => mhpmcounters[1][(sizeof(xlen) - 1) .. 0],
+    (0xC05,  _) => mhpmcounters[2][(sizeof(xlen) - 1) .. 0],
+    (0xC06,  _) => mhpmcounters[3][(sizeof(xlen) - 1) .. 0],
+    (0xC07,  _) => mhpmcounters[4][(sizeof(xlen) - 1) .. 0],
+    (0xC08,  _) => mhpmcounters[5][(sizeof(xlen) - 1) .. 0],
+    (0xC09,  _) => mhpmcounters[6][(sizeof(xlen) - 1) .. 0],
+    (0xC0A,  _) => mhpmcounters[7][(sizeof(xlen) - 1) .. 0],
+    (0xC0B,  _) => mhpmcounters[8][(sizeof(xlen) - 1) .. 0],
+    (0xC0C,  _) => mhpmcounters[9][(sizeof(xlen) - 1) .. 0],
+    (0xC0D,  _) => mhpmcounters[10][(sizeof(xlen) - 1) .. 0],
+    (0xC0E,  _) => mhpmcounters[11][(sizeof(xlen) - 1) .. 0],
+    (0xC0F,  _) => mhpmcounters[12][(sizeof(xlen) - 1) .. 0],
+    (0xC10,  _) => mhpmcounters[13][(sizeof(xlen) - 1) .. 0],
+    (0xC11,  _) => mhpmcounters[14][(sizeof(xlen) - 1) .. 0],
+    (0xC12,  _) => mhpmcounters[15][(sizeof(xlen) - 1) .. 0],
+    (0xC13,  _) => mhpmcounters[16][(sizeof(xlen) - 1) .. 0],
+    (0xC14,  _) => mhpmcounters[17][(sizeof(xlen) - 1) .. 0],
+    (0xC15,  _) => mhpmcounters[18][(sizeof(xlen) - 1) .. 0],
+    (0xC16,  _) => mhpmcounters[19][(sizeof(xlen) - 1) .. 0],
+    (0xC17,  _) => mhpmcounters[20][(sizeof(xlen) - 1) .. 0],
+    (0xC18,  _) => mhpmcounters[21][(sizeof(xlen) - 1) .. 0],
+    (0xC19,  _) => mhpmcounters[22][(sizeof(xlen) - 1) .. 0],
+    (0xC1A,  _) => mhpmcounters[23][(sizeof(xlen) - 1) .. 0],
+    (0xC1B,  _) => mhpmcounters[24][(sizeof(xlen) - 1) .. 0],
+    (0xC1C,  _) => mhpmcounters[25][(sizeof(xlen) - 1) .. 0],
+    (0xC1D,  _) => mhpmcounters[26][(sizeof(xlen) - 1) .. 0],
+    (0xC1E,  _) => mhpmcounters[27][(sizeof(xlen) - 1) .. 0],
+    (0xC1F,  _) => mhpmcounters[28][(sizeof(xlen) - 1) .. 0],
+
     (0xC80, 32) => mcycle[63 .. 32],
     (0xC81, 32) => mtime[63 .. 32],
     (0xC82, 32) => minstret[63 .. 32],
@@ -173,6 +292,14 @@ function readCSR csr : csreg -> xlenbits = {
   res
 }
 
+//val plat_write_mhpmevent = {c: "riscv_write_mhpmevent", ocaml: "Platform.write_mhpmevent"} : (xlenbits, xlenbits, xlenbits) -> unit
+val plat_write_mhpmevent  : (xlenbits, xlenbits, xlenbits) -> unit
+function plat_write_mhpmevent (a : xlenbits, b : xlenbits, c : xlenbits) -> unit = {
+    let A = a;      // Cannot have an empty function.  Added this to get rid of compile error.
+    //TBD
+}
+
+
 function writeCSR (csr : csreg, value : xlenbits) -> unit = {
   let res : option(xlenbits) =
   match (csr, sizeof(xlen)) {
@@ -186,6 +313,36 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x306,  _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) },
     (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now
     (0x320,  _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(EXTZ(mcountinhibit.bits())) },
+    (0x323,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 0), value, mhpmevents[0]); mhpmevents[0] = value; Some(value) },
+    (0x324,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 1), value, mhpmevents[1]); mhpmevents[1] = value; Some(value) },
+    (0x325,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 2), value, mhpmevents[2]); mhpmevents[2] = value; Some(value) },
+    (0x326,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 3), value, mhpmevents[3]); mhpmevents[3] = value; Some(value) },
+    (0x327,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 4), value, mhpmevents[4]); mhpmevents[4] = value; Some(value) },
+    (0x328,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 5), value, mhpmevents[5]); mhpmevents[5] = value; Some(value) },
+    (0x329,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 6), value, mhpmevents[6]); mhpmevents[6] = value; Some(value) },
+    (0x32A,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 7), value, mhpmevents[7]); mhpmevents[7] = value; Some(value) },
+    (0x32B,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 8), value, mhpmevents[8]); mhpmevents[8] = value; Some(value) },
+    (0x32C,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 9), value, mhpmevents[9]); mhpmevents[9] = value; Some(value) },
+    (0x32D,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 10), value, mhpmevents[10]); mhpmevents[10] = value; Some(value) },
+    (0x32E,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 11), value, mhpmevents[11]); mhpmevents[11] = value; Some(value) },
+    (0x32F,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 12), value, mhpmevents[12]); mhpmevents[12] = value; Some(value) },
+    (0x330,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 13), value, mhpmevents[13]); mhpmevents[13] = value; Some(value) },
+    (0x331,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 14), value, mhpmevents[14]); mhpmevents[14] = value; Some(value) },
+    (0x332,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 15), value, mhpmevents[15]); mhpmevents[15] = value; Some(value) },
+    (0x333,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 16), value, mhpmevents[16]); mhpmevents[16] = value; Some(value) },
+    (0x334,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 17), value, mhpmevents[17]); mhpmevents[17] = value; Some(value) },
+    (0x335,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 18), value, mhpmevents[18]); mhpmevents[18] = value; Some(value) },
+    (0x336,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 19), value, mhpmevents[19]); mhpmevents[19] = value; Some(value) },
+    (0x337,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 20), value, mhpmevents[10]); mhpmevents[20] = value; Some(value) },
+    (0x338,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 21), value, mhpmevents[21]); mhpmevents[21] = value; Some(value) },
+    (0x339,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 22), value, mhpmevents[22]); mhpmevents[22] = value; Some(value) },
+    (0x33A,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 23), value, mhpmevents[23]); mhpmevents[23] = value; Some(value) },
+    (0x33B,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 24), value, mhpmevents[24]); mhpmevents[24] = value; Some(value) },
+    (0x33C,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 25), value, mhpmevents[25]); mhpmevents[25] = value; Some(value) },
+    (0x33D,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 26), value, mhpmevents[26]); mhpmevents[26] = value; Some(value) },
+    (0x33E,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 27), value, mhpmevents[27]); mhpmevents[27] = value; Some(value) },
+    (0x33F,  _) => { plat_write_mhpmevent(to_bits(sizeof(xlen), 28), value, mhpmevents[28]); mhpmevents[28] = value; Some(value) },
+
     (0x340,  _) => { mscratch = value; Some(mscratch) },
     (0x341,  _) => { Some(set_xret_target(Machine, value)) },
     (0x342,  _) => { mcause->bits() = value; Some(mcause.bits()) },
@@ -218,8 +375,67 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     /* machine mode counters */
     (0xB00,  _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
     (0xB02,  _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_written = true; Some(value) },
+    (0xB03,  _) => { mhpmcounters[0][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB04,  _) => { mhpmcounters[1][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB05,  _) => { mhpmcounters[2][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB06,  _) => { mhpmcounters[3][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB07,  _) => { mhpmcounters[4][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB08,  _) => { mhpmcounters[5][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB09,  _) => { mhpmcounters[6][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB0A,  _) => { mhpmcounters[7][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB0B,  _) => { mhpmcounters[8][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB0C,  _) => { mhpmcounters[9][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB0D,  _) => { mhpmcounters[10][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB0E,  _) => { mhpmcounters[11][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB0F,  _) => { mhpmcounters[12][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB10,  _) => { mhpmcounters[13][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB11,  _) => { mhpmcounters[14][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB12,  _) => { mhpmcounters[15][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB13,  _) => { mhpmcounters[16][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB14,  _) => { mhpmcounters[17][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB15,  _) => { mhpmcounters[18][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB16,  _) => { mhpmcounters[19][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB17,  _) => { mhpmcounters[20][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB18,  _) => { mhpmcounters[21][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB19,  _) => { mhpmcounters[22][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB1A,  _) => { mhpmcounters[23][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB1B,  _) => { mhpmcounters[24][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB1C,  _) => { mhpmcounters[25][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB1D,  _) => { mhpmcounters[26][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB1E,  _) => { mhpmcounters[27][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0xB1F,  _) => { mhpmcounters[28][(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+
     (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) },
     (0xB82, 32) => { minstret[63 .. 32] = value; minstret_written = true; Some(value) },
+    (0xB83, 32) => { mhpmcounters[0][63 .. 32] = value; Some(value) },
+    (0xB84, 32) => { mhpmcounters[1][63 .. 32] = value; Some(value) },
+    (0xB85, 32) => { mhpmcounters[2][63 .. 32] = value; Some(value) },
+    (0xB86, 32) => { mhpmcounters[3][63 .. 32] = value; Some(value) },
+    (0xB87, 32) => { mhpmcounters[4][63 .. 32] = value; Some(value) },
+    (0xB88, 32) => { mhpmcounters[5][63 .. 32] = value; Some(value) },
+    (0xB89, 32) => { mhpmcounters[6][63 .. 32] = value; Some(value) },
+    (0xB8A, 32) => { mhpmcounters[7][63 .. 32] = value; Some(value) },
+    (0xB8B, 32) => { mhpmcounters[8][63 .. 32] = value; Some(value) },
+    (0xB8C, 32) => { mhpmcounters[9][63 .. 32] = value; Some(value) },
+    (0xB8D, 32) => { mhpmcounters[10][63 .. 32] = value; Some(value) },
+    (0xB8E, 32) => { mhpmcounters[11][63 .. 32] = value; Some(value) },
+    (0xB8F, 32) => { mhpmcounters[12][63 .. 32] = value; Some(value) },
+    (0xB90, 32) => { mhpmcounters[13][63 .. 32] = value; Some(value) },
+    (0xB91, 32) => { mhpmcounters[14][63 .. 32] = value; Some(value) },
+    (0xB92, 32) => { mhpmcounters[15][63 .. 32] = value; Some(value) },
+    (0xB93, 32) => { mhpmcounters[16][63 .. 32] = value; Some(value) },
+    (0xB94, 32) => { mhpmcounters[17][63 .. 32] = value; Some(value) },
+    (0xB95, 32) => { mhpmcounters[18][63 .. 32] = value; Some(value) },
+    (0xB96, 32) => { mhpmcounters[19][63 .. 32] = value; Some(value) },
+    (0xB97, 32) => { mhpmcounters[20][63 .. 32] = value; Some(value) },
+    (0xB98, 32) => { mhpmcounters[21][63 .. 32] = value; Some(value) },
+    (0xB99, 32) => { mhpmcounters[22][63 .. 32] = value; Some(value) },
+    (0xB9A, 32) => { mhpmcounters[23][63 .. 32] = value; Some(value) },
+    (0xB9B, 32) => { mhpmcounters[24][63 .. 32] = value; Some(value) },
+    (0xB9C, 32) => { mhpmcounters[25][63 .. 32] = value; Some(value) },
+    (0xB9D, 32) => { mhpmcounters[26][63 .. 32] = value; Some(value) },
+    (0xB9E, 32) => { mhpmcounters[27][63 .. 32] = value; Some(value) },
+    (0xB9F, 32) => { mhpmcounters[28][63 .. 32] = value; Some(value) },
 
     /* trigger/debug */
     (0x7a0,  _) => { tselect = value; Some(tselect) },
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 6681367..25d672e 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -91,6 +91,38 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x306 => p == Machine & haveUsrMode(), // mcounteren
     0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush
     0x320 => p == Machine, // mcountinhibit
+
+    /* machine mode: event selectors */
+    0x323 => p == Machine, // mhpmevents[0]
+    0x324 => p == Machine, // mhpmevents[1]
+    0x325 => p == Machine, // mhpmevents[2]
+    0x326 => p == Machine, // mhpmevents[3]
+    0x327 => p == Machine, // mhpmevents[4]
+    0x328 => p == Machine, // mhpmevents[5]
+    0x329 => p == Machine, // mhpmevents[6]
+    0x32A => p == Machine, // mhpmevents[7]
+    0x32B => p == Machine, // mhpmevents[8]
+    0x32C => p == Machine, // mhpmevents[9]
+    0x32D => p == Machine, // mhpmevents[10]
+    0x32E => p == Machine, // mhpmevents[11]
+    0x32F => p == Machine, // mhpmevents[12]
+    0x330 => p == Machine, // mhpmevents[13]
+    0x331 => p == Machine, // mhpmevents[14]
+    0x332 => p == Machine, // mhpmevents[15]
+    0x333 => p == Machine, // mhpmevents[16]
+    0x334 => p == Machine, // mhpmevents[17]
+    0x335 => p == Machine, // mhpmevents[18]
+    0x336 => p == Machine, // mhpmevents[19]
+    0x337 => p == Machine, // mhpmevents[20]
+    0x338 => p == Machine, // mhpmevents[21]
+    0x339 => p == Machine, // mhpmevents[22]
+    0x33A => p == Machine, // mhpmevents[23]
+    0x33B => p == Machine, // mhpmevents[24]
+    0x33C => p == Machine, // mhpmevents[25]
+    0x33D => p == Machine, // mhpmevents[26]
+    0x33E => p == Machine, // mhpmevents[27]
+    0x33F => p == Machine, // mhpmevents[28]
+
     /* machine mode: trap handling */
     0x340 => p == Machine, // mscratch
     0x341 => p == Machine, // mepc
@@ -123,9 +155,67 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     /* counters */
     0xB00 => p == Machine, // mcycle
     0xB02 => p == Machine, // minstret
+    0xB03 => p == Machine, // mhpmcounters[0]
+    0xB04 => p == Machine, // mhpmcounters[1]
+    0xB05 => p == Machine, // mhpmcounters[2]
+    0xB06 => p == Machine, // mhpmcounters[3]
+    0xB07 => p == Machine, // mhpmcounters[4]
+    0xB08 => p == Machine, // mhpmcounters[5]
+    0xB09 => p == Machine, // mhpmcounters[6]
+    0xB0A => p == Machine, // mhpmcounters[7]
+    0xB0B => p == Machine, // mhpmcounters[8]
+    0xB0C => p == Machine, // mhpmcounters[9]
+    0xB0D => p == Machine, // mhpmcounters[10]
+    0xB0E => p == Machine, // mhpmcounters[11]
+    0xB0F => p == Machine, // mhpmcounters[12]
+    0xB10 => p == Machine, // mhpmcounters[13]
+    0xB11 => p == Machine, // mhpmcounters[14]
+    0xB12 => p == Machine, // mhpmcounters[15]
+    0xB13 => p == Machine, // mhpmcounters[16]
+    0xB14 => p == Machine, // mhpmcounters[17]
+    0xB15 => p == Machine, // mhpmcounters[18]
+    0xB16 => p == Machine, // mhpmcounters[19]
+    0xB17 => p == Machine, // mhpmcounters[20]
+    0xB18 => p == Machine, // mhpmcounters[21]
+    0xB19 => p == Machine, // mhpmcounters[22]
+    0xB1A => p == Machine, // mhpmcounters[23]
+    0xB1B => p == Machine, // mhpmcounters[24]
+    0xB1C => p == Machine, // mhpmcounters[25]
+    0xB1D => p == Machine, // mhpmcounters[26]
+    0xB1E => p == Machine, // mhpmcounters[27]
+    0xB1F => p == Machine, // mhpmcounters[28]
 
     0xB80 => p == Machine & (sizeof(xlen) == 32), // mcycleh
     0xB82 => p == Machine & (sizeof(xlen) == 32), // minstreth
+    0xB83 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[0]
+    0xB84 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[1]
+    0xB85 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[2]
+    0xB86 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[3]
+    0xB87 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[4]
+    0xB88 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[5]
+    0xB89 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[6]
+    0xB8A => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[7]
+    0xB8B => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[8]
+    0xB8C => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[9]
+    0xB8D => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[10]
+    0xB8E => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[11]
+    0xB8F => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[12]
+    0xB90 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[13]
+    0xB91 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[14]
+    0xB92 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[15]
+    0xB93 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[16]
+    0xB94 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[17]
+    0xB95 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[18]
+    0xB96 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[19]
+    0xB97 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[20]
+    0xB98 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[21]
+    0xB99 => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[22]
+    0xB9A => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[23]
+    0xB9B => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[24]
+    0xB9C => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[25]
+    0xB9D => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[26]
+    0xB9E => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[27]
+    0xB9F => p == Machine & (sizeof(xlen) == 32), // mhpmcounters[28]
 
     /* disabled trigger/debug module */
     0x7a0 => p == Machine,
@@ -152,6 +242,35 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0xC00 => haveUsrMode(),    // cycle
     0xC01 => haveUsrMode(),    // time
     0xC02 => haveUsrMode(),    // instret
+    0xC03 => haveUsrMode(),    // hpmcounters[0]
+    0xC04 => haveUsrMode(),    // hpmcounters[1]
+    0xC05 => haveUsrMode(),    // hpmcounters[2]
+    0xC06 => haveUsrMode(),    // hpmcounters[3]
+    0xC07 => haveUsrMode(),    // hpmcounters[4]
+    0xC08 => haveUsrMode(),    // hpmcounters[5]
+    0xC09 => haveUsrMode(),    // hpmcounters[6]
+    0xC0A => haveUsrMode(),    // hpmcounters[7]
+    0xC0B => haveUsrMode(),    // hpmcounters[8]
+    0xC0C => haveUsrMode(),    // hpmcounters[9]
+    0xC0D => haveUsrMode(),    // hpmcounters[10]
+    0xC0E => haveUsrMode(),    // hpmcounters[11]
+    0xC0F => haveUsrMode(),    // hpmcounters[12]
+    0xC10 => haveUsrMode(),    // hpmcounters[13]
+    0xC11 => haveUsrMode(),    // hpmcounters[14]
+    0xC12 => haveUsrMode(),    // hpmcounters[15]
+    0xC13 => haveUsrMode(),    // hpmcounters[16]
+    0xC14 => haveUsrMode(),    // hpmcounters[17]
+    0xC15 => haveUsrMode(),    // hpmcounters[18]
+    0xC16 => haveUsrMode(),    // hpmcounters[19]
+    0xC17 => haveUsrMode(),    // hpmcounters[20]
+    0xC18 => haveUsrMode(),    // hpmcounters[21]
+    0xC19 => haveUsrMode(),    // hpmcounters[22]
+    0xC1A => haveUsrMode(),    // hpmcounters[23]
+    0xC1B => haveUsrMode(),    // hpmcounters[24]
+    0xC1C => haveUsrMode(),    // hpmcounters[25]
+    0xC1D => haveUsrMode(),    // hpmcounters[26]
+    0xC1E => haveUsrMode(),    // hpmcounters[27]
+    0xC1F => haveUsrMode(),    // hpmcounters[28]
 
     0xC80 => haveUsrMode() & (sizeof(xlen) == 32),     // cycleh
     0xC81 => haveUsrMode() & (sizeof(xlen) == 32),     // timeh
@@ -177,15 +296,73 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool =
     (0xC00, Supervisor) => mcounteren.CY() == 0b1,
     (0xC01, Supervisor) => mcounteren.TM() == 0b1,
     (0xC02, Supervisor) => mcounteren.IR() == 0b1,
-
-    (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
+    (0xC03, Supervisor) => mcounteren.HPM()[0] == bitone,
+    (0xC04, Supervisor) => mcounteren.HPM()[1] == bitone,
+    (0xC05, Supervisor) => mcounteren.HPM()[2] == bitone,
+    (0xC06, Supervisor) => mcounteren.HPM()[3] == bitone,
+    (0xC07, Supervisor) => mcounteren.HPM()[4] == bitone,
+    (0xC08, Supervisor) => mcounteren.HPM()[5] == bitone,
+    (0xC09, Supervisor) => mcounteren.HPM()[6] == bitone,
+    (0xC0A, Supervisor) => mcounteren.HPM()[7] == bitone,
+    (0xC0B, Supervisor) => mcounteren.HPM()[8] == bitone,
+    (0xC0C, Supervisor) => mcounteren.HPM()[9] == bitone,
+    (0xC0D, Supervisor) => mcounteren.HPM()[10] == bitone,
+    (0xC0E, Supervisor) => mcounteren.HPM()[11] == bitone,
+    (0xC0F, Supervisor) => mcounteren.HPM()[12] == bitone,
+    (0xC10, Supervisor) => mcounteren.HPM()[13] == bitone,
+    (0xC11, Supervisor) => mcounteren.HPM()[14] == bitone,
+    (0xC12, Supervisor) => mcounteren.HPM()[15] == bitone,
+    (0xC13, Supervisor) => mcounteren.HPM()[16] == bitone,
+    (0xC14, Supervisor) => mcounteren.HPM()[17] == bitone,
+    (0xC15, Supervisor) => mcounteren.HPM()[18] == bitone,
+    (0xC16, Supervisor) => mcounteren.HPM()[19] == bitone,
+    (0xC17, Supervisor) => mcounteren.HPM()[10] == bitone,
+    (0xC18, Supervisor) => mcounteren.HPM()[21] == bitone,
+    (0xC19, Supervisor) => mcounteren.HPM()[22] == bitone,
+    (0xC1A, Supervisor) => mcounteren.HPM()[23] == bitone,
+    (0xC1B, Supervisor) => mcounteren.HPM()[24] == bitone,
+    (0xC1C, Supervisor) => mcounteren.HPM()[25] == bitone,
+    (0xC1D, Supervisor) => mcounteren.HPM()[26] == bitone,
+    (0xC1E, Supervisor) => mcounteren.HPM()[27] == bitone,
+    (0xC1F, Supervisor) => mcounteren.HPM()[28] == 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),
+
+    (0xC80, User) => mcounteren.CY() == 0b1 & ((~ (haveSupMode())) | scounteren.CY() == 0b1),   // TODO: check address
+    (0xC81, User) => mcounteren.TM() == 0b1 & ((~ (haveSupMode())) | scounteren.TM() == 0b1),   // TODO: check address
+    (0xC82, User) => mcounteren.IR() == 0b1 & ((~ (haveSupMode())) | scounteren.IR() == 0b1),   // TODO: check address
+    (0xC83, User) => mcounteren.HPM()[0] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[0] == bitone),
+    (0xC84, User) => mcounteren.HPM()[1] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[1] == bitone),
+    (0xC85, User) => mcounteren.HPM()[2] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[2] == bitone),
+    (0xC86, User) => mcounteren.HPM()[3] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[3] == bitone),
+    (0xC87, User) => mcounteren.HPM()[4] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[4] == bitone),
+    (0xC88, User) => mcounteren.HPM()[5] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[5] == bitone),
+    (0xC89, User) => mcounteren.HPM()[6] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[6] == bitone),
+    (0xC8A, User) => mcounteren.HPM()[7] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[7] == bitone),
+    (0xC8B, User) => mcounteren.HPM()[8] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[8] == bitone),
+    (0xC8C, User) => mcounteren.HPM()[9] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[9] == bitone),
+    (0xC8D, User) => mcounteren.HPM()[10] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[10] == bitone),
+    (0xC8E, User) => mcounteren.HPM()[11] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[11] == bitone),
+    (0xC8F, User) => mcounteren.HPM()[12] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[12] == bitone),
+    (0xC90, User) => mcounteren.HPM()[13] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[13] == bitone),
+    (0xC91, User) => mcounteren.HPM()[14] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[14] == bitone),
+    (0xC92, User) => mcounteren.HPM()[15] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[15] == bitone),
+    (0xC93, User) => mcounteren.HPM()[16] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[16] == bitone),
+    (0xC94, User) => mcounteren.HPM()[17] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[17] == bitone),
+    (0xC95, User) => mcounteren.HPM()[18] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[18] == bitone),
+    (0xC96, User) => mcounteren.HPM()[19] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[19] == bitone),
+    (0xC97, User) => mcounteren.HPM()[20] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[20] == bitone),
+    (0xC98, User) => mcounteren.HPM()[21] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[21] == bitone),
+    (0xC99, User) => mcounteren.HPM()[22] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[22] == bitone),
+    (0xC9A, User) => mcounteren.HPM()[23] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[23] == bitone),
+    (0xC9B, User) => mcounteren.HPM()[24] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[24] == bitone),
+    (0xC9C, User) => mcounteren.HPM()[25] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[25] == bitone),
+    (0xC9D, User) => mcounteren.HPM()[26] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[26] == bitone),
+    (0xC9E, User) => mcounteren.HPM()[27] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[27] == bitone),
+    (0xC9F, User) => mcounteren.HPM()[28] == bitone & ((~ (haveSupMode())) | scounteren.HPM()[28] == bitone),
+    (_, _) => true
   }
 
 
@@ -596,6 +773,11 @@ function init_sys() -> unit = {
   minstret           = EXTZ(0b0);
   minstret_written   = false;
 
+  foreach (i from 0 to 28) {
+    mhpmevents[i]   = sail_zeros(sizeof(xlen));
+    mhpmcounters[i] = sail_zeros(64);
+  };
+
   init_pmp();
 
   // log compatibility with spike
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index e1576ed..ecd8eb8 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -515,7 +515,7 @@ register mcounteren : Counteren
 register scounteren : Counteren
 
 function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
-  /* no HPM counters yet */
+  let c = update_HPM(c, v[31 .. 3]);
   let c = update_IR(c, [v[2]]);
   let c = update_TM(c, [v[1]]);
   let c = update_CY(c, [v[0]]);
@@ -523,7 +523,7 @@ function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
 }
 
 function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
-  /* no HPM counters yet */
+  let c = update_HPM(c, v[31 .. 3]);
   let c = update_IR(c, [v[2]]);
   let c = update_TM(c, [v[1]]);
   let c = update_CY(c, [v[0]]);
@@ -531,13 +531,14 @@ function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
 }
 
 bitfield Counterin : bits(32) = {
-  /* no HPM counters yet */
-  IR : 2,
-  CY : 0
+  HPM : 31 .. 3,
+  IR  : 2,
+  CY  : 0
 }
 register mcountinhibit : Counterin
 
 function legalize_mcountinhibit(c : Counterin, v : xlenbits) -> Counterin = {
+  let c = update_HPM(c, v[31 .. 3]);
   let c = update_IR(c, [v[2]]);
   let c = update_CY(c, [v[0]]);
   c
@@ -546,6 +547,12 @@ function legalize_mcountinhibit(c : Counterin, v : xlenbits) -> Counterin = {
 register mcycle : bits(64)
 register mtime : bits(64)
 
+/* HPM counters */
+
+register mhpmevents   : vector(29, dec, xlenbits)
+register mhpmcounters : vector(29, dec, bits(64))
+
+
 /* minstret
  *
  * minstret is an architectural register, and can be written to.  The
@@ -559,8 +566,10 @@ register mtime : bits(64)
  */
 register minstret : bits(64)
 register minstret_written : bool
+register inst_retired : bool
 
 function retire_instruction() -> unit = {
+  inst_retired = true;
   if   minstret_written == true
   then minstret_written = false
   else if mcountinhibit.IR() == 0b0