diff --git a/Makefile b/Makefile
index ea6244a43..246affcaa 100644
--- a/Makefile
+++ b/Makefile
@@ -28,6 +28,7 @@ SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail
 SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_cdext.sail
 
 SAIL_DEFAULT_INST += riscv_insts_svinval.sail
+SAIL_DEFAULT_INST += riscv_insts_ctr.sail
 
 SAIL_DEFAULT_INST += riscv_insts_zba.sail
 SAIL_DEFAULT_INST += riscv_insts_zbb.sail
@@ -68,6 +69,7 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 SAIL_SYS_SRCS =  riscv_csr_map.sail
 SAIL_SYS_SRCS += riscv_vext_control.sail    # helpers for the 'V' extension
 SAIL_SYS_SRCS += riscv_next_regs.sail
+SAIL_SYS_SRCS += riscv_ctr_regs.sail
 SAIL_SYS_SRCS += riscv_sys_exceptions.sail  # default basic helpers for exception handling
 SAIL_SYS_SRCS += riscv_sync_exception.sail  # define the exception structure used in the model
 SAIL_SYS_SRCS += riscv_next_control.sail    # helpers for the 'N' extension
diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c
index 2fdb63f92..aa321326e 100644
--- a/c_emulator/riscv_platform.c
+++ b/c_emulator/riscv_platform.c
@@ -71,7 +71,18 @@ bool sys_enable_writable_misa(unit u)
 {
   return rv_enable_writable_misa;
 }
-
+uint64_t sys_valid_ctr_depth(unit u)
+{
+  return rv_valid_ctr_depth;
+}
+bool sys_enable_ssctr(unit u)
+{
+  return rv_enable_ssctr;
+}
+bool sys_enable_smctr(unit u)
+{
+  return rv_enable_smctr;
+}
 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 341bd5964..df2591d11 100644
--- a/c_emulator/riscv_platform.h
+++ b/c_emulator/riscv_platform.h
@@ -11,6 +11,10 @@ bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(unit);
 bool sys_enable_vext(unit);
 
+uint64_t sys_valid_ctr_depth(unit u);
+bool sys_enable_ssctr(unit u);
+bool sys_enable_smctr(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 077fc50dc..51b40c8fe 100644
--- a/c_emulator/riscv_platform_impl.c
+++ b/c_emulator/riscv_platform_impl.c
@@ -6,6 +6,10 @@
 uint64_t rv_pmp_count = 0;
 uint64_t rv_pmp_grain = 0;
 
+uint64_t rv_valid_ctr_depth = 0x1F;
+bool rv_enable_smctr = true;
+bool rv_enable_ssctr = true;
+
 bool rv_enable_svinval = false;
 bool rv_enable_zcb = false;
 bool rv_enable_zfinx = false;
diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h
index c4289e679..7d3450037 100644
--- a/c_emulator/riscv_platform_impl.h
+++ b/c_emulator/riscv_platform_impl.h
@@ -11,6 +11,10 @@
 extern uint64_t rv_pmp_count;
 extern uint64_t rv_pmp_grain;
 
+extern uint64_t rv_valid_ctr_depth;
+extern bool rv_enable_smctr;
+extern bool rv_enable_ssctr;
+
 extern bool rv_enable_svinval;
 extern bool rv_enable_zcb;
 extern bool rv_enable_zfinx;
diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c
index 3a9bfc08d..dd278951c 100644
--- a/c_emulator/riscv_sim.c
+++ b/c_emulator/riscv_sim.c
@@ -54,6 +54,9 @@ const char *RV32ISA = "RV32IMAC";
 #define OPT_PMP_COUNT 1002
 #define OPT_PMP_GRAIN 1003
 #define OPT_ENABLE_SVINVAL 1004
+#define OPT_ENABLE_SMCTR 1005
+#define OPT_ENABLE_SSCTR 1006
+#define OPT_VALID_CTR_DEPTH 1007
 #define OPT_ENABLE_ZCB 10014
 
 static bool do_dump_dts = false;
@@ -149,6 +152,9 @@ static struct option options[] = {
     {"enable-writable-fiom",        no_argument,       0, OPT_ENABLE_WRITABLE_FIOM},
     {"enable-svinval",              no_argument,       0, OPT_ENABLE_SVINVAL      },
     {"enable-zcb",                  no_argument,       0, OPT_ENABLE_ZCB          },
+    {"valid-ctr-depth",             required_argument, 0, OPT_VALID_CTR_DEPTH     },
+    {"enable-smctr",                no_argument,       0, OPT_ENABLE_SMCTR        },
+    {"enable-ssctr",                no_argument,       0, OPT_ENABLE_SSCTR        },
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },
 #endif
@@ -245,6 +251,8 @@ static int process_args(int argc, char **argv)
   uint64_t ram_size = 0;
   uint64_t pmp_count = 0;
   uint64_t pmp_grain = 0;
+  uint64_t valid_ctr_depth = 0;
+
   while (true) {
     c = getopt_long(argc, argv,
                     "a"
@@ -394,6 +402,22 @@ static int process_args(int argc, char **argv)
       fprintf(stderr, "enabling Zcb extension.\n");
       rv_enable_zcb = true;
       break;
+    case OPT_ENABLE_SMCTR:
+      fprintf(stderr, "enabling Smctr extension.\n");
+      rv_enable_smctr = true;
+      break;
+    case OPT_ENABLE_SSCTR:
+      fprintf(stderr, "enabling Ssctr extension.\n");
+      rv_enable_ssctr = true;
+      break;
+    case OPT_VALID_CTR_DEPTH:
+      rv_valid_ctr_depth = atol(optarg);
+      fprintf(stderr, "Valid CTR depth: %" PRIu64 "\n", rv_valid_ctr_depth);
+      if (rv_valid_ctr_depth > 0x1F) {
+        fprintf(stderr, "invalid CTR depth");
+        exit(1);
+      }
+      break;
     case 'x':
       fprintf(stderr, "enabling Zfinx support.\n");
       rv_enable_zfinx = true;
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index 22cffd5a6..cc9530d65 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -49,8 +49,22 @@ mapping clause csr_name_map = 0x141  <-> "sepc"
 mapping clause csr_name_map = 0x142  <-> "scause"
 mapping clause csr_name_map = 0x143  <-> "stval"
 mapping clause csr_name_map = 0x144  <-> "sip"
+/* Supervisor Control Transfer Records Control Register */
+mapping clause csr_name_map = 0x14E  <-> "sctrctl"
+/* Supervisor Control Transfer Records Status Register */
+mapping clause csr_name_map = 0x14F  <-> "sctrstatus"
 /* supervisor protection and translation */
 mapping clause csr_name_map = 0x180  <-> "satp"
+/* supervisor indirect register select and alias CSRs */
+mapping clause csr_name_map = 0x150  <-> "siselect"
+mapping clause csr_name_map = 0x151  <-> "sireg"
+mapping clause csr_name_map = 0x152  <-> "sireg2"
+mapping clause csr_name_map = 0x153  <-> "sireg3"
+mapping clause csr_name_map = 0x155  <-> "sireg4"
+mapping clause csr_name_map = 0x156  <-> "sireg5"
+mapping clause csr_name_map = 0x157  <-> "sireg6"
+/* Supervisor Control Transfer Records Depth Register */
+mapping clause csr_name_map = 0x15F  <-> "sctrdepth"
 /* supervisor envcfg */
 mapping clause csr_name_map = 0x10A  <-> "senvcfg"
 /* machine information registers */
@@ -70,12 +84,25 @@ mapping clause csr_name_map = 0x306  <-> "mcounteren"
 mapping clause csr_name_map = 0x320  <-> "mcountinhibit"
 /* machine envcfg */
 mapping clause csr_name_map = 0x30A  <-> "menvcfg"
+/* Smstateen csrs */
+mapping clause csr_name_map = 0x30C  <-> "mstateen0"
+mapping clause csr_name_map = 0x31C  <-> "mstateen0h"
 /* machine trap handling */
 mapping clause csr_name_map = 0x340  <-> "mscratch"
 mapping clause csr_name_map = 0x341  <-> "mepc"
 mapping clause csr_name_map = 0x342  <-> "mcause"
 mapping clause csr_name_map = 0x343  <-> "mtval"
 mapping clause csr_name_map = 0x344  <-> "mip"
+/* Machine Control Transfer Records Control Register */
+mapping clause csr_name_map = 0x34E  <-> "mctrctl"
+/* Machine indirect register select and alias CSRs */
+mapping clause csr_name_map = 0x350  <-> "miselect"
+mapping clause csr_name_map = 0x351  <-> "mireg"
+mapping clause csr_name_map = 0x352  <-> "mireg2"
+mapping clause csr_name_map = 0x353  <-> "mireg3"
+mapping clause csr_name_map = 0x355  <-> "mireg4"
+mapping clause csr_name_map = 0x356  <-> "mireg5"
+mapping clause csr_name_map = 0x357  <-> "mireg6"
 /* machine protection and translation */
 mapping clause csr_name_map = 0x3A0  <-> "pmpcfg0"
 mapping clause csr_name_map = 0x3A1  <-> "pmpcfg1"
diff --git a/model/riscv_ctr_regs.sail b/model/riscv_ctr_regs.sail
new file mode 100644
index 000000000..31d333caa
--- /dev/null
+++ b/model/riscv_ctr_regs.sail
@@ -0,0 +1,207 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* Support CTR depths - if bit n is set then CTR depth 2^n is supported */
+val sys_valid_ctr_depth = {c: "sys_valid_ctr_depth", ocaml: "Platform.valid_ctr_depth", _: "sys_valid_ctr_depth"} : unit -> bits(64)
+
+/* Architectural state for the Ssctr and Smctr standard extension. */
+bitfield Mctrctl : bits(64) = {
+  DIRLJMPINH : 47,
+  INDLJMPINH : 46,
+  RETINH     : 45,
+  CORSWAPINH : 44,
+  DIRJMPINH  : 43,
+  INDJMPINH  : 42,
+  DIRCALLINH : 41,
+  INDCALLINH : 40,
+  TKBRINH    : 37,
+  NTBREN     : 36,
+  TRETINH    : 35,
+  INTRINH    : 34,
+  EXCINH     : 33,
+
+  LCOFIFRZ   : 12,
+  BPFRZ      : 11,
+
+  MTE        : 9,
+  STE        : 8,
+
+  RASEMU     : 7,
+
+  M          : 2,
+  S          : 1,
+  U          : 0
+}
+bitfield Sctrctl : bits(64) = {
+  DIRLJMPINH : 47,
+  INDLJMPINH : 46,
+  RETINH     : 45,
+  CORSWAPINH : 44,
+  DIRJMPINH  : 43,
+  INDJMPINH  : 42,
+  DIRCALLINH : 41,
+  INDCALLINH : 40,
+  TKBRINH    : 37,
+  NTBREN     : 36,
+  TRETINH    : 35,
+  INTRINH    : 34,
+  EXCINH     : 33,
+
+  LCOFIFRZ   : 12,
+  BPFRZ      : 11,
+
+  STE        : 8,
+
+  RASEMU     : 7,
+
+  S          : 1,
+  U          : 0
+}
+bitfield Sctrdepth : bits(32) = {
+  DEPTH      : 2 .. 0
+}
+bitfield Sctrstatus : bits(32) = {
+  FROZEN     : 31,
+  WRPTR      : 7 .. 0
+}
+bitfield Ctrsource : xlenbits = {
+  PC         : xlen - 1 .. 1,
+  V          : 0
+}
+bitfield Ctrtarget : xlenbits = {
+  PC         : xlen - 1 .. 1,
+  MISP       : 0
+}
+bitfield Ctrdata : bits(64) = {
+  CCE        : 31 .. 28,
+  CCM        : 27 .. 16,
+  CCV        : 15,
+  TYPE       : 3 .. 0
+}
+
+register sctrstatus : Sctrstatus
+register sctrdepth  : Sctrdepth
+register mctrctl    : Mctrctl
+register ctrsource  : vector(256, dec, Ctrsource)
+register ctrtarget  : vector(256, dec, Ctrtarget)
+register ctrdata    : vector(256, dec, Ctrdata)
+/* Should parameterize the cycle counter to support wider counters */
+register ctr_cycle_counter : bits(13)
+register ctr_cycle_counter_valid : bool
+
+function legalize_mctrctl(o : Mctrctl, v : xlenbits) -> Mctrctl = {
+  let m : Mctrctl = Mk_Mctrctl(zero_extend(v));
+  m
+}
+
+function lower_sctrctl(m : Mctrctl) -> Sctrctl = {
+  let s = Mk_Sctrctl(m.bits);
+  s
+}
+
+function legalize_sctrctl(m : Mctrctl, v : xlenbits) -> Mctrctl = {
+  let o = Mk_Mctrctl(zero_extend(v));
+  let o = [o with M = m[M], MTE = m[MTE]];
+  o
+}
+
+
+function get_wrptr_mask(d : Sctrdepth) -> bits(8) =
+  match(d[DEPTH]) {
+    0b000 => 0b00001111,
+    0b001 => 0b00011111,
+    0b010 => 0b00111111,
+    0b011 => 0b01111111,
+    0b100 => 0b11111111,
+        _ => internal_error(__FILE__, __LINE__, "Unexpected DEPTH encoding")
+  }
+
+function legalize_sctrdepth(s : Sctrdepth, v : xlenbits) -> Sctrdepth = {
+  let valid_ctr_depth : bits(64) = sys_valid_ctr_depth();
+  let depth : bits(3) = match(v[2 .. 0]) {
+    0b000 => if bit_to_bool(valid_ctr_depth[0]) then v[2 .. 0] else s[DEPTH],
+    0b001 => if bit_to_bool(valid_ctr_depth[1]) then v[2 .. 0] else s[DEPTH],
+    0b010 => if bit_to_bool(valid_ctr_depth[2]) then v[2 .. 0] else s[DEPTH],
+    0b011 => if bit_to_bool(valid_ctr_depth[3]) then v[2 .. 0] else s[DEPTH],
+    0b100 => if bit_to_bool(valid_ctr_depth[4]) then v[2 .. 0] else s[DEPTH],
+        _ => s[DEPTH]
+  };
+  let o = Mk_Sctrdepth(zero_extend(depth));
+
+  /* On depth change WRPTR assumes an unspecified but legal value */
+  sctrstatus[WRPTR] = sctrstatus[WRPTR] & get_wrptr_mask(o);
+
+  o
+}
+function legalize_sctrstatus(s : Sctrstatus, v : xlenbits) -> Sctrstatus = {
+  let wrptr_mask : bits(8) = get_wrptr_mask(sctrdepth);
+  let o = Mk_Sctrstatus(zeros());
+  let o = [o with WRPTR = (v[7 .. 0] & wrptr_mask), FROZEN = v[31 .. 31]];
+  o
+}
+function number_of_ctr() -> int = {
+  let valid_ctr_depth : bits(64) = sys_valid_ctr_depth();
+  let num = if bit_to_bool(valid_ctr_depth[0]) then 16 else 0;
+  let num = if bit_to_bool(valid_ctr_depth[1]) then 32 else num;
+  let num = if bit_to_bool(valid_ctr_depth[2]) then 64 else num;
+  let num = if bit_to_bool(valid_ctr_depth[3]) then 128 else num;
+  let num = if bit_to_bool(valid_ctr_depth[4]) then 256 else num;
+  num
+}
+function isValidCtrMiselect() -> bool = {
+  let ctr_select = miselect.bits[7 .. 0];
+  haveSmctr() & (unsigned(ctr_select) < number_of_ctr())
+}
+function isValidCtrSiselect() -> bool = {
+  let ctr_select = siselect.bits[7 .. 0];
+  haveSsctr() & (unsigned(ctr_select) < number_of_ctr())
+}
+/* Logical entry N, selected by *iselect value of (0x200 | N), is
+ * physically at ((WRPTR - N - 1) % depth) where depth = 2^(DEPTH+4)
+ */
+function get_ctr_idx(iselect : SMiselect) -> bits(8) = {
+  let ctr_idx = sctrstatus[WRPTR] - iselect.bits[7 .. 0] - 1;
+  ctr_idx & get_wrptr_mask(sctrdepth);
+}
+
+function get_ctr_mireg() -> xlenbits =
+  ctrsource[unsigned(get_ctr_idx(miselect))].bits
+
+function get_ctr_mireg2() -> xlenbits =
+  ctrtarget[unsigned(get_ctr_idx(miselect))].bits
+
+function get_ctr_mireg3() -> xlenbits =
+  ctrdata[unsigned(get_ctr_idx(miselect))].bits
+
+function set_ctr_mireg(v: xlenbits) -> unit =
+  ctrsource[unsigned(get_ctr_idx(miselect))] = Mk_Ctrsource(v)
+
+function set_ctr_mireg2(v: xlenbits) -> unit =
+  ctrtarget[unsigned(get_ctr_idx(miselect))] = Mk_Ctrtarget(v)
+
+function set_ctr_mireg3(v: xlenbits) -> unit =
+  ctrdata[unsigned(get_ctr_idx(miselect))] = Mk_Ctrdata(v)
+
+
+function get_ctr_sireg() -> xlenbits =
+  ctrsource[unsigned(get_ctr_idx(siselect))].bits
+
+function get_ctr_sireg2() -> xlenbits =
+  ctrsource[unsigned(get_ctr_idx(siselect))].bits
+
+function get_ctr_sireg3() -> xlenbits =
+  ctrsource[unsigned(get_ctr_idx(siselect))].bits
+
+function set_ctr_sireg(v: xlenbits) -> unit =
+  ctrsource[unsigned(get_ctr_idx(siselect))] = Mk_Ctrsource(v)
+
+function set_ctr_sireg2(v: xlenbits) -> unit =
+  ctrtarget[unsigned(get_ctr_idx(siselect))] = Mk_Ctrtarget(v)
+
+function set_ctr_sireg3(v: xlenbits) -> unit =
+  ctrdata[unsigned(get_ctr_idx(siselect))] = Mk_Ctrdata(v)
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 8d86804ed..bb7763149 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -57,6 +57,7 @@ match bv {
 but this is difficult
 */
 
+val update_ctr_jal : regidx -> unit
 function clause execute (RISCV_JAL(imm, rd)) = {
   let t : xlenbits = PC + sign_extend(imm);
   /* Extensions get the first checks on the prospective target address. */
@@ -74,6 +75,8 @@ function clause execute (RISCV_JAL(imm, rd)) = {
       } else {
         X(rd) = get_next_pc();
         set_next_pc(target);
+        /* update control transfer record if Ssctr/Smctr is active */
+        update_ctr_jal(rd);
         RETIRE_SUCCESS
       }
     }
@@ -111,6 +114,7 @@ mapping encdec_bop : bop <-> bits(3) = {
 mapping clause encdec = BTYPE(imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1 @ 0b0, rs2, rs1, op)
   <-> imm7_6 : bits(1) @ imm7_5_0 : bits(6) @ rs2 @ rs1 @ encdec_bop(op) @ imm5_4_1 : bits(4) @ imm5_0 : bits(1) @ 0b1100011
 
+val update_ctr_conditional: (bool) -> unit
 function clause execute (BTYPE(imm, rs2, rs1, op)) = {
   let rs1_val = X(rs1);
   let rs2_val = X(rs2);
@@ -136,11 +140,17 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
           RETIRE_FAIL;
         } else {
           set_next_pc(target);
+          /* Update control transfer record if Smctr/Ssctr is active */
+          update_ctr_conditional(true);
           RETIRE_SUCCESS
         }
       }
     }
-  } else RETIRE_SUCCESS
+  } else {
+    /* Update control transfer record if Smctr/Ssctr is active */
+    update_ctr_conditional(false);
+    RETIRE_SUCCESS
+  }
 }
 
 mapping btype_mnemonic : bop <-> string = {
diff --git a/model/riscv_insts_ctr.sail b/model/riscv_insts_ctr.sail
new file mode 100644
index 000000000..f1d63b50a
--- /dev/null
+++ b/model/riscv_insts_ctr.sail
@@ -0,0 +1,202 @@
+/*=======================================================================================*/
+/*  This Sail RISC-V architecture model, comprising all files and                        */
+/*  directories except where otherwise noted is subject the BSD                          */
+/*  two-clause license in the LICENSE file.                                              */
+/*                                                                                       */
+/*  SPDX-License-Identifier: BSD-2-Clause                                                */
+/*=======================================================================================*/
+
+/* ***************************************************************************/
+/* This file specifies the instruction added by the 'Smctr/Ssctr' extension. */
+
+union clause ast = SCTRCLR : unit
+
+mapping clause encdec = SCTRCLR()
+  <-> 0b000100000100 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
+
+function clause execute SCTRCLR() = {
+  let sctrclr_illegal : bool = match cur_privilege {
+    User       => true,
+    Supervisor => not(haveSsctr()) | mstateen0[CTR] == 0b0,
+    Machine    => not(haveSmctr())
+  };
+  if   sctrclr_illegal
+  then { handle_illegal(); RETIRE_FAIL }
+  else {
+    foreach (i from 0 to 255) {
+      ctrsource[i] = Mk_Ctrsource(zeros());
+      ctrtarget[i] = Mk_Ctrtarget(zeros());
+      ctrdata[i] = Mk_Ctrdata(zeros());
+    };
+    ctr_cycle_counter = zeros();
+    ctr_cycle_counter_valid = false;
+    RETIRE_SUCCESS
+  }
+}
+
+mapping clause assembly = SCTRCLR() <-> "sctrclr"
+
+
+
+/* The following functions are extensions to JAL/JALR instructions to
+ * update control transfer records
+ */
+enum ctr_xfer_type  = {
+  EXCEPTION,
+  INTERRUPT,
+  TRAP_RETURN,
+  NOT_TAKEN_BRANCH,
+  TAKEN_BRANCH,
+  INDIRECT_CALL,
+  DIRECT_CALL,
+  INDIRECT_JUMP_NO_LINKAGE,
+  DIRECT_JUMP_NO_LINKAGE,
+  COROUTINE_SWAP,
+  FUNCTION_RETURN,
+  OTHER_INDIRECT_JUMP_WITH_LINKAGE,
+  OTHER_DIRECT_JUMP_WITH_LINKAGE
+  }
+mapping encdec_ctr_xfer_type : ctr_xfer_type <-> bits(4) = {
+  EXCEPTION                        <-> 0b0001,
+  INTERRUPT                        <-> 0b0010,
+  TRAP_RETURN                      <-> 0b0011,
+  NOT_TAKEN_BRANCH                 <-> 0b0100,
+  TAKEN_BRANCH                     <-> 0b0101,
+  INDIRECT_CALL                    <-> 0b1000,
+  DIRECT_CALL                      <-> 0b1001,
+  INDIRECT_JUMP_NO_LINKAGE         <-> 0b1010,
+  DIRECT_JUMP_NO_LINKAGE           <-> 0b1011,
+  COROUTINE_SWAP                   <-> 0b1100,
+  FUNCTION_RETURN                  <-> 0b1101,
+  OTHER_INDIRECT_JUMP_WITH_LINKAGE <-> 0b1110,
+  OTHER_DIRECT_JUMP_WITH_LINKAGE   <-> 0b1111
+}
+
+function is_ctr_active(priv : Privilege) -> bool =
+  match priv {
+    User       => isSsctrEnabled() & mctrctl[U] == 0b1 & sctrstatus[FROZEN] == 0b0,
+    Supervisor => isSsctrEnabled() & mctrctl[S] == 0b1 & sctrstatus[FROZEN] == 0b0,
+    Machine    => isSsctrEnabled() & mctrctl[M] == 0b1 & sctrstatus[FROZEN] == 0b0
+  }
+
+val get_wrptr_mask : Sctrdepth -> bits(8)
+
+function update_ctr(transfer_type : ctr_xfer_type, src_recorded : bool, dst_recorded : bool) -> unit = {
+  let src_pc  : xlenbits = if src_recorded then get_arch_pc() else zeros();
+  let tgt_pc  : xlenbits = if dst_recorded then get_next_pc() else zeros();
+  let ras_emu : bool     = mctrctl[RASEMU] == 0b1;
+  let cce     : bits(1)  = ctr_cycle_counter[12 .. 12];
+  let ccm     : bits(12) = ctr_cycle_counter[11 .. 0];
+  let ccv     : bits(1)  = if ctr_cycle_counter_valid & not(ras_emu) then 0b1 else 0b0;
+
+  /* Transfer type filtering */
+  let is_transfer_type_enabled : bool = match transfer_type {
+    EXCEPTION                        => mctrctl[EXCINH]     == 0b0 & not(ras_emu),
+    INTERRUPT                        => mctrctl[INTRINH]    == 0b0 & not(ras_emu),
+    TRAP_RETURN                      => mctrctl[TRETINH]    == 0b0 & not(ras_emu),
+    NOT_TAKEN_BRANCH                 => mctrctl[NTBREN]     == 0b1 & not(ras_emu),
+    TAKEN_BRANCH                     => mctrctl[TKBRINH]    == 0b0 & not(ras_emu),
+    INDIRECT_CALL                    => mctrctl[INDCALLINH] == 0b0 | ras_emu,
+    DIRECT_CALL                      => mctrctl[DIRCALLINH] == 0b0 | ras_emu,
+    INDIRECT_JUMP_NO_LINKAGE         => mctrctl[INDJMPINH]  == 0b0 & not(ras_emu),
+    DIRECT_JUMP_NO_LINKAGE           => mctrctl[DIRJMPINH]  == 0b0 & not(ras_emu),
+    COROUTINE_SWAP                   => mctrctl[CORSWAPINH] == 0b0 | not(ras_emu),
+    FUNCTION_RETURN                  => mctrctl[RETINH]     == 0b0 | ras_emu,
+    OTHER_INDIRECT_JUMP_WITH_LINKAGE => mctrctl[INDLJMPINH] == 0b0 & not(ras_emu),
+    OTHER_DIRECT_JUMP_WITH_LINKAGE   => mctrctl[DIRLJMPINH] == 0b0 & not(ras_emu),
+  };
+
+  /* In RAS emulation, function returns and corouting swaps pop and then push */
+  if ras_emu & (transfer_type == FUNCTION_RETURN | transfer_type == COROUTINE_SWAP) then {
+    sctrstatus[WRPTR] = (sctrstatus[WRPTR] - 1) & get_wrptr_mask(sctrdepth);
+    ctrsource[unsigned(sctrstatus[WRPTR])] = [ctrsource[unsigned(sctrstatus[WRPTR])] with V = 0b0];
+  };
+
+  /* When RAS emulation is enabled, returns only pop but coroutines push as well */
+  let do_push : bool = is_transfer_type_enabled & (not(ras_emu) | (ras_emu & transfer_type != FUNCTION_RETURN));
+
+  if do_push then {
+    cycle_counter_valid = false;
+    ctr_cycle_counter = zeros();
+    ctrsource[unsigned(sctrstatus[WRPTR])] = Mk_Ctrsource(src_pc[(sizeof(xlen) - 1) .. 1] @ 0b1);
+    ctrtarget[unsigned(sctrstatus[WRPTR])] = Mk_Ctrtarget(tgt_pc[(sizeof(xlen) - 1) .. 1] @ 0b0);
+    ctrdata[unsigned(sctrstatus[WRPTR])]   =
+      Mk_Ctrdata(zero_extend(cce @ ccm @ ccv @ 0b00000000000 @ encdec_ctr_xfer_type(transfer_type)));
+    sctrstatus[WRPTR]                      = (sctrstatus[WRPTR] + 1) & get_wrptr_mask(sctrdepth);
+  }
+}
+
+function update_ctr_jal(rd : regidx) -> unit = {
+  if   rd == 0b00000 & is_ctr_active(cur_privilege)
+  then update_ctr(DIRECT_JUMP_NO_LINKAGE, true, true)
+  else if (rd == 0b00001 | rd == 0b00101) & is_ctr_active(cur_privilege)
+  then update_ctr(DIRECT_CALL, true, true)
+  else if is_ctr_active(cur_privilege)
+  then update_ctr(OTHER_DIRECT_JUMP_WITH_LINKAGE, true, true);
+}
+
+function update_ctr_jalr(rs1 : regidx, rd : regidx) -> unit = {
+  if   ((rs1 != 0b00101 & rd == 0b00001) | (rs1 != 0b00001 & rd == 0b00101)) & is_ctr_active(cur_privilege)
+  then update_ctr(INDIRECT_CALL, true, true)
+  else if (rs1 != 0b00101 & rs1 != 0b00001 & rd == 0b00000) & is_ctr_active(cur_privilege)
+  then update_ctr(INDIRECT_JUMP_NO_LINKAGE, true, true)
+  else if ((rs1 == 0b00001 & rd == 0b00101) | (rs1 == 0b00101 & rd == 0b00001)) & is_ctr_active(cur_privilege)
+  then update_ctr(COROUTINE_SWAP, true, true)
+  else if is_ctr_active(cur_privilege)
+  then update_ctr(OTHER_INDIRECT_JUMP_WITH_LINKAGE, true, true);
+}
+
+function update_ctr_conditional(taken : bool) -> unit = {
+  if   taken & is_ctr_active(cur_privilege)
+  then update_ctr(TAKEN_BRANCH, true, true)
+  else if is_ctr_active(cur_privilege)
+  then update_ctr(NOT_TAKEN_BRANCH, true, true);
+}
+
+function update_ctr_traps(intr : bool, del_priv : Privilege) -> unit = {
+  let is_src_ctr_enabled : bool     = is_ctr_active(cur_privilege);
+  let is_dst_ctr_enabled : bool     = is_ctr_active(del_priv);
+  let transfer_type : ctr_xfer_type = if intr then INTERRUPT else EXCEPTION;
+
+  let effective_xte : bool = match  (cur_privilege, del_priv) {
+    (User,       Supervisor) => mctrctl[STE] == 0b1,
+    (User,       Machine)    => mctrctl[STE] == 0b1 & mctrctl[MTE] == 0b1,
+    (Supervisor, Machine)    => mctrctl[MTE] == 0b1,
+    (_, _)                   => false
+  };
+  /* Traps between enabled privilege modes are recorded as normal.
+   * Traps from a disabled privilege mode to an enabled privilege mode
+   * are partially recorded, such that the ctrsource.PC is 0. Traps from
+   * an enabled mode to a disabled mode, known as external traps, are
+   * recorded with ctrtarget.PC as 0 if the effective xTE bit is 1
+   */
+  if   is_src_ctr_enabled & is_dst_ctr_enabled
+  then update_ctr(transfer_type, true, true)
+  else if not(is_src_ctr_enabled) & is_dst_ctr_enabled
+  then update_ctr(transfer_type, false, true)
+  else if is_src_ctr_enabled & not(is_dst_ctr_enabled) & effective_xte
+  then update_ctr(transfer_type, true, false)
+}
+
+function update_ctr_trap_return(prev_priv : Privilege) -> unit = {
+  let is_src_ctr_enabled : bool     = is_ctr_active(prev_priv);
+  let is_dst_ctr_enabled : bool     = is_ctr_active(cur_privilege);
+
+  /* Trap returns between enabled privilege modes are recorded
+   * as normal. Trap returns from an enabled mode back to a disabled mode are
+   * partially recorded, such that ctrtarget.PC is 0. Trap returns from a
+   * disabled mode to an enabled mode are not recorded.
+   */
+  if   is_src_ctr_enabled & is_dst_ctr_enabled
+  then update_ctr(TRAP_RETURN, true, true)
+  else if is_src_ctr_enabled & not(is_dst_ctr_enabled)
+  then update_ctr(TRAP_RETURN, true, false)
+}
+/* model implements a 13-bit cycle counter */
+function count_ctr_cycles() -> unit = {
+  if is_ctr_active(cur_privilege) then {
+    if unsigned(ctr_cycle_counter) < 8191
+    then ctr_cycle_counter = ctr_cycle_counter + 1;
+    ctr_cycle_counter_valid = true;
+  }
+}
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index f2980fb9e..b44e39b06 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -38,8 +38,10 @@ function readCSR csr : csreg -> xlenbits = {
     (0x305,  _) => get_mtvec(),
     (0x306,  _) => zero_extend(mcounteren.bits),
     (0x30A,  _) => menvcfg.bits[sizeof(xlen) - 1 .. 0],
+    (0x30C,  _) => mstateen0.bits[sizeof(xlen) - 1 .. 0],
     (0x310, 32) => mstatush.bits,
     (0x31A, 32) => menvcfg.bits[63 .. 32],
+    (0x31C, 32) => mstateen0.bits[63 .. 32],
     (0x320,  _) => zero_extend(mcountinhibit.bits),
 
     (0x340,  _) => mscratch,
@@ -48,6 +50,16 @@ function readCSR csr : csreg -> xlenbits = {
     (0x343,  _) => mtval,
     (0x344,  _) => mip.bits,
 
+    (0x34E,  _) => mctrctl.bits,
+
+    (0x350,  _) => miselect.bits,
+    (0x351,  _) => get_mireg(),
+    (0x352,  _) => get_mireg2(),
+    (0x353,  _) => get_mireg3(),
+    (0x355,  _) => get_mireg4(),
+    (0x356,  _) => get_mireg5(),
+    (0x357,  _) => get_mireg6(),
+
     // pmpcfgN
     (0x3A @ idx : bits(4),  _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)),
     // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits.
@@ -87,6 +99,16 @@ function readCSR csr : csreg -> xlenbits = {
     (0x142,  _) => scause.bits,
     (0x143,  _) => stval,
     (0x144,  _) => lower_mip(mip, mideleg).bits,
+    (0x14E,  _) => lower_sctrctl(mctrctl).bits,
+    (0x14F,  _) => zero_extend(sctrstatus.bits),
+    (0x150,  _) => siselect.bits(),
+    (0x151,  _) => get_sireg(),
+    (0x152,  _) => get_sireg2(),
+    (0x153,  _) => get_sireg3(),
+    (0x155,  _) => get_sireg4(),
+    (0x156,  _) => get_sireg5(),
+    (0x157,  _) => get_sireg6(),
+    (0x15F,  _) => zero_extend(sctrdepth.bits),
     (0x180,  _) => satp,
 
     /* user mode counters */
@@ -125,8 +147,11 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x306,  _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits)) },
     (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) },
     (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits) },
+    (0x30C, 32) => { mstateen0 = legalize_mstateen0(mstateen0, mstateen0.bits[63 .. 32] @ value); Some(mstateen0.bits[31 .. 0]) },
+    (0x30C, 64) => { mstateen0 = legalize_mstateen0(mstateen0, value); Some(mstateen0.bits) },
     (0x310, 32) => { Some(mstatush.bits) }, // ignore writes for now
     (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) },
+    (0x31C, 32) => { mstateen0 = legalize_mstateen0(mstateen0, value @ mstateen0.bits[31 .. 0]); Some(mstateen0.bits[63 .. 32]) },
     (0x320,  _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits)) },
     (0x340,  _) => { mscratch = value; Some(mscratch) },
     (0x341,  _) => { Some(set_xret_target(Machine, value)) },
@@ -134,6 +159,16 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x343,  _) => { mtval = value; Some(mtval) },
     (0x344,  _) => { mip = legalize_mip(mip, value); Some(mip.bits) },
 
+    (0x34E,  _) => { mctrctl = legalize_mctrctl(mctrctl, value); Some(mctrctl.bits) },
+
+    (0x350,  _) => { miselect = legalize_iselect(miselect, value); Some(miselect.bits) },
+    (0x351,  _) => { set_mireg(value);  Some(get_mireg())  },
+    (0x352,  _) => { set_mireg2(value); Some(get_mireg2()) },
+    (0x353,  _) => { set_mireg3(value); Some(get_mireg3()) },
+    (0x355,  _) => { set_mireg4(value); Some(get_mireg4()) },
+    (0x356,  _) => { set_mireg5(value); Some(get_mireg5()) },
+    (0x357,  _) => { set_mireg6(value); Some(get_mireg6()) },
+
     // pmpcfgN
     (0x3A @ idx : bits(4),  _) if idx[0] == bitzero | sizeof(xlen) == 32 => {
       let idx = unsigned(idx);
@@ -168,6 +203,20 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x142,  _) => { scause.bits = value; Some(scause.bits) },
     (0x143,  _) => { stval = value; Some(stval) },
     (0x144,  _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) },
+
+    (0x14E,  _) => { mctrctl = legalize_sctrctl(mctrctl, value); Some(mctrctl.bits) },
+    (0x14F,  _) => { sctrstatus = legalize_sctrstatus(sctrstatus, value); Some(zero_extend(sctrstatus.bits)) },
+
+    (0x150,  _) => { siselect = legalize_iselect(siselect, value); Some(siselect.bits) },
+    (0x151,  _) => { set_sireg(value);  Some(get_sireg()) },
+    (0x152,  _) => { set_sireg2(value); Some(get_sireg2()) },
+    (0x153,  _) => { set_sireg3(value); Some(get_sireg3()) },
+    (0x155,  _) => { set_sireg4(value); Some(get_sireg4()) },
+    (0x156,  _) => { set_sireg5(value); Some(get_sireg5()) },
+    (0x157,  _) => { set_sireg6(value); Some(get_sireg6()) },
+
+    (0x15F,  _) => { sctrdepth = legalize_sctrdepth(sctrdepth, value); Some(zero_extend(sctrdepth.bits)) },
+
     (0x180,  _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) },
 
     /* user mode: seed (entropy source). writes are ignored */
diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail
index d628630af..0e7f5352f 100644
--- a/model/riscv_jalr_rmem.sail
+++ b/model/riscv_jalr_rmem.sail
@@ -8,11 +8,15 @@
 
 /* The definition for the memory model. */
 
+val update_ctr_jalr : (regidx, regidx) -> unit
+
 function clause execute (RISCV_JALR(imm, rs1, rd)) = {
   /* FIXME: this does not check for a misaligned target address. See riscv_jalr_seq.sail. */
   /* write rd before anything else to prevent unintended strength */
   X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
   let newPC : xlenbits = X(rs1) + sign_extend(imm);
   nextPC = [newPC with 0 = bitzero];  /* Clear newPC[0] */
+  /* update control transfer record if Ssctr/Smctr is active */
+  update_ctr_jalr(rs1, rd);
   RETIRE_SUCCESS
 }
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index 497a44178..a99c0a829 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -8,6 +8,8 @@
 
 /* The definition for the sequential model. */
 
+val update_ctr_jalr : (regidx, regidx) -> unit
+
 function clause execute (RISCV_JALR(imm, rs1, rd)) = {
 /* For the sequential model, the memory-model definition doesn't work directly
  * if rs1 = rd.  We would effectively have to keep a regfile for reads and another for
@@ -30,6 +32,8 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
       } else {
         X(rd) = get_next_pc();
         set_next_pc(target);
+        /* update control transfer record if Ssctr/Smctr is active */
+        update_ctr_jalr(rs1, rd);
         RETIRE_SUCCESS
       }
     }
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 19e3d30ae..106ecaa01 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -250,11 +250,15 @@ function clint_store(addr, width, data) = {
   }
 }
 
+val count_ctr_cycles : unit -> unit
 val tick_clock : unit -> unit
 function tick_clock() = {
   if   mcountinhibit[CY] == 0b0
   then mcycle = mcycle + 1;
 
+  /* Smctr/Ssctr - update CTR cycles */
+  count_ctr_cycles();
+
   mtime  = mtime  + 1;
   clint_dispatch()
 }
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index 1baa33701..5010f4c38 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -31,8 +31,10 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x305 => p == Machine, // mtvec
     0x306 => p == Machine & haveUsrMode(), // mcounteren
     0x30A => p == Machine & haveUsrMode(), // menvcfg
+    0x30C => p == Machine & haveSupMode() & haveSmstateen(), // mstateen0
     0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush
     0x31A => p == Machine & haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh
+    0x31C => p == Machine & haveSupMode() & (sizeof(xlen) == 32) & haveSmstateen(), // mstateen0h
     0x320 => p == Machine, // mcountinhibit
     /* machine mode: trap handling */
     0x340 => p == Machine, // mscratch
@@ -40,6 +42,16 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x342 => p == Machine, // mcause
     0x343 => p == Machine, // mtval
     0x344 => p == Machine, // mip
+    /* machine mode: Machine Control Transfer Records Control Register */
+    0x34E => p == Machine & haveSmctr(), // mctrctl
+    /* machine mode: indirect register select and alias CSRs */
+    0x350 => p == Machine & haveSmcsrind(), // miselect
+    0x351 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg
+    0x352 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg2
+    0x353 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg3
+    0x355 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg4
+    0x356 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg5
+    0x357 => p == Machine & haveSmcsrind() & isValidMiselect(), // mireg6
 
     // pmpcfgN
     0x3A @ idx : bits(4) => p == Machine & sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32),
@@ -74,6 +86,30 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x143 => haveSupMode() & (p == Machine | p == Supervisor), // stval
     0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip
 
+    /* supervisor mode: Machine Control Transfer Records Control Register */
+    0x14E => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrctl
+    /* supervisor mode: Machine Control Transfer Records Status Register */
+    0x14F => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrstatus
+
+    /* supervisor mode: indirect register select and alias CSRs */
+    0x150 => haveSupMode() & haveSscsrind() &
+             (p == Machine | (p == Supervisor & isSscsrindEnabled())), // siselect
+    0x151 => haveSupMode() & haveSscsrind() & isValidSiselect() &
+             (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg
+    0x152 => haveSupMode() & haveSscsrind() & isValidSiselect() &
+             (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg2
+    0x153 => haveSupMode() & haveSscsrind() & isValidSiselect() &
+             (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg3
+    0x155 => haveSupMode() & haveSscsrind() & isValidSiselect() &
+             (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg4
+    0x156 => haveSupMode() & haveSscsrind() & isValidSiselect() &
+             (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg5
+    0x157 => haveSupMode() & haveSscsrind() & isValidSiselect() &
+             (p == Machine | (p == Supervisor & isSscsrindEnabled())), // sireg6
+
+    /* supervisor mode: Machine Control Transfer Records Depth Register */
+    0x15F => haveSsctr() & (p == Machine | (p == Supervisor & isSsctrEnabled())), // sctrdepth
+
     /* supervisor mode: address translation */
     0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp
 
@@ -314,6 +350,7 @@ function rvfi_trap () = ()
 $endif
 
 /* handle exceptional ctl flow by updating nextPC and operating privilege */
+val update_ctr_traps : (bool, Privilege) -> unit
 
 function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception))
                      -> xlenbits = {
@@ -325,6 +362,9 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
   cancel_reservation();
 
+  /* Update control transfer records when Smctr/Ssctr is implemented */
+  update_ctr_traps(intr, del_priv);
+
   match (del_priv) {
     Machine => {
        mcause[IsInterrupt] = bool_to_bits(intr);
@@ -393,6 +433,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
   };
 }
 
+val update_ctr_trap_return : (Privilege) -> unit
 function exception_handler(cur_priv : Privilege, ctl : ctl_result,
                            pc: xlenbits) -> xlenbits = {
   match (cur_priv, ctl) {
@@ -418,6 +459,8 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
+      /* Update control transfer records when Smctr/Ssctr is implemented */
+      update_ctr_trap_return(prev_priv);
       prepare_xret_target(Machine) & pc_alignment_mask()
     },
     (_, CTL_SRET())  => {
@@ -436,6 +479,8 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
                           ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
+      /* Update control transfer records when Smctr/Ssctr is implemented */
+      update_ctr_trap_return(prev_priv);
       prepare_xret_target(Supervisor) & pc_alignment_mask()
     },
     (_, CTL_URET())  => {
@@ -528,6 +573,11 @@ function init_sys() -> unit = {
 
   menvcfg.bits = zero_extend(0b0);
   senvcfg.bits = zero_extend(0b0);
+  mstateen0.bits = zero_extend(0b0);
+
+  /* Smctr/Ssctr cycle counter */
+  ctr_cycle_counter_valid = false;
+
   /* initialize vector csrs */
   elen               = 0b1; /* ELEN=64 as the common case */
   vlen               = 0b0100; /* VLEN=512 as a default value */
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 6c66492b4..af5dc85c0 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -95,6 +95,10 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "
 /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
    supervisor mode is implemented and non-bare addressing modes are supported. */
 val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
+/* whether Ssctr is enabled */
+val sys_enable_ssctr = {c: "sys_enable_ssctr", ocaml: "Platform.enable_ssctr", _: "sys_enable_ssctr"} : unit -> bool
+/* whether Smctr is enabled */
+val sys_enable_smctr = {c: "sys_enable_smctr", ocaml: "Platform.enable_smctr", _: "sys_enable_smctr"} : unit -> bool
 
 /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */
 val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64)
@@ -164,6 +168,21 @@ function haveZmmul()  -> bool = true
 /* Zicond extension support */
 function haveZicond() -> bool = true
 
+/* Smstateen extension support */
+function haveSmstateen() -> bool = true
+
+/* Sscsrind extension support */
+function haveSscsrind() -> bool = true
+
+/* Smcsrind extension support */
+function haveSmcsrind() -> bool = true
+
+/* Smctr extension support - Smctr depends on S-mode, and Smcsrind */
+function haveSmctr() -> bool = haveSupMode() & sys_enable_smctr() & haveSmcsrind()
+
+/* Ssctr extension support - Ssctr depends on S-mode, Smctr, and Sscsrind */
+function haveSsctr() -> bool = haveSupMode() & sys_enable_ssctr() & haveSmctr() & haveSscsrind()
+
 bitfield Mstatush : bits(32) = {
   MBE  : 5,
   SBE  : 4
@@ -835,6 +854,50 @@ function is_fiom_active() -> bool = {
     User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1,
   }
 }
+
+/* Smstateen */
+bitfield Mstateen0 : bits(64) = {
+  SE0        : 63,               // Controls access to hstateen0/h and sstateen0
+  ENVCFG     : 62,               // Controls access to henvcfg/h and senvcfg
+  WPRI_1     : 61,
+  CSRIND     : 60,               // controls access to the siselect, sireg*, vsiselect,
+                                 // and the vsireg* CSRs provided by the Sscsrind extensions
+  AIA        : 59,               // Controls access to Ssaia state not
+                                 // controlled by CSRIND or IMSIC
+  IMSIC      : 58,               // Controls access IMSIC state - including
+                                 // stopei and vstopei
+  CONTEXT    : 57,               // Controls access to scontext and hcontext
+  PRIV_V1P13 : 56,               // Controls access to hedelegh
+  WPRI_1     : 55,
+  CTR        : 54,               // Controls Ssctr state
+  WPRI_0     : 53 .. 3,
+  JVT        : 2,                // Controls access to the jvt CSR
+  FCSR       : 1,                // Controls access to the fcsr
+  C          : 0                 // Controls access to any and all custom state
+}
+
+register mstateen0 : Mstateen0
+
+function isSscsrindEnabled() -> bool =
+  match(haveSmstateen(), mstateen0[CSRIND]) {
+    (false,  _) => true,
+    (true, 0b0) => false,
+    (true, 0b1) => true
+ }
+function isSsctrEnabled() -> bool =
+  match(haveSmstateen(), mstateen0[CTR]) {
+    (false,  _) => true,
+    (true, 0b0) => false,
+    (true, 0b1) => true
+ }
+
+function legalize_mstateen0(o : Mstateen0, v : bits(64)) -> Mstateen0 = {
+  let v = Mk_Mstateen0(v);
+  let o = [o with CSRIND = if haveSscsrind() then v[CSRIND] else 0b0];
+  // Other extensions are not implemented yet so all other fields are read only zero.
+  o
+}
+
 /* vector csrs */
 register vstart : bits(16) /* use the largest possible length of vstart */
 register vxsat  : bits(1)
@@ -919,3 +982,137 @@ function get_vtype_vma() = decode_agtype(vtype[vma])
 
 val get_vtype_vta : unit -> agtype
 function get_vtype_vta() = decode_agtype(vtype[vta])
+
+bitfield SMiselect : xlenbits = {
+  REG : 11 .. 0
+}
+
+register siselect : SMiselect
+register miselect : SMiselect
+
+function legalize_iselect(s : SMiselect, v: xlenbits) -> SMiselect = {
+  let s = Mk_SMiselect(v);
+  s
+}
+
+val isValidCtrMiselect: unit -> bool
+val isValidCtrSiselect: unit -> bool
+function isValidMiselect() -> bool = {
+  /* The behavior upon accessing mireg* from M-mode,
+   * while miselect holds a value that is not implemented,
+   * is UNSPECIFIED. It is expected that implementations
+   * will typically raise an illegal instruction exception
+   */
+  if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767
+  then isValidCtrMiselect() /* 0x200 - 0x2FF is designated for Smctr */
+  else false;
+}
+function isValidSiselect() -> bool = {
+  /* The behavior upon accessing sireg* from M/S-mode,
+   * while siselect holds a value that is not implemented,
+   * is UNSPECIFIED. It is expected that implementations
+   * will typically raise an illegal instruction exception
+   */
+  if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767
+  then isValidCtrSiselect() /* 0x200 - 0x2FF is designated for Ssctr */
+  else false;
+}
+val get_ctr_mireg  : unit -> xlenbits
+val get_ctr_mireg2 : unit -> xlenbits
+val get_ctr_mireg3 : unit -> xlenbits
+val set_ctr_mireg  : xlenbits -> unit
+val set_ctr_mireg2 : xlenbits -> unit
+val set_ctr_mireg3 : xlenbits -> unit
+function get_mireg() -> xlenbits = {
+  if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767
+  then get_ctr_mireg()
+  else zeros()
+}
+function get_mireg2() -> xlenbits = {
+  if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767
+  then get_ctr_mireg2()
+  else zeros()
+}
+function get_mireg3() -> xlenbits = {
+  if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767
+  then get_ctr_mireg3()
+  else zeros()
+}
+function get_mireg4() -> xlenbits = {
+  zeros()
+}
+function get_mireg5() -> xlenbits = {
+  zeros()
+}
+function get_mireg6() -> xlenbits = {
+  zeros()
+}
+
+function set_mireg(v: xlenbits) -> unit = {
+  let ctr_idx = miselect.bits[7 .. 0];
+  if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767
+  then set_ctr_mireg(v)
+}
+function set_mireg2(v: xlenbits) -> unit = {
+  let ctr_idx = miselect.bits[7 .. 0];
+  if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767
+  then set_ctr_mireg2(v)
+}
+function set_mireg3(v: xlenbits) -> unit = {
+  let ctr_idx = miselect.bits[7 .. 0];
+  if unsigned(miselect[REG]) >= 512 & unsigned(miselect[REG]) <= 767
+  then set_ctr_mireg3(v)
+}
+function set_mireg4(v: xlenbits) -> unit = ()
+function set_mireg5(v: xlenbits) -> unit = ()
+function set_mireg6(v: xlenbits) -> unit = ()
+
+val get_ctr_sireg  : unit -> xlenbits
+val get_ctr_sireg2 : unit -> xlenbits
+val get_ctr_sireg3 : unit -> xlenbits
+val set_ctr_sireg  : xlenbits -> unit
+val set_ctr_sireg2 : xlenbits -> unit
+val set_ctr_sireg3 : xlenbits -> unit
+function get_sireg() -> xlenbits = {
+  if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767
+  then get_ctr_sireg()
+  else zeros()
+}
+function get_sireg2() -> xlenbits = {
+  if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767
+  then get_ctr_sireg2()
+  else zeros()
+}
+function get_sireg3() -> xlenbits = {
+  if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767
+  then get_ctr_sireg3()
+  else zeros()
+}
+function get_sireg4() -> xlenbits = {
+  zeros()
+}
+function get_sireg5() -> xlenbits = {
+  zeros()
+}
+function get_sireg6() -> xlenbits = {
+  zeros()
+}
+
+function set_sireg(v: xlenbits) -> unit = {
+  let ctr_idx = siselect.bits[7 .. 0];
+  if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767
+  then set_ctr_sireg(v)
+}
+function set_sireg2(v: xlenbits) -> unit = {
+  let ctr_idx = siselect.bits[7 .. 0];
+  if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767
+  then set_ctr_sireg2(v)
+}
+function set_sireg3(v: xlenbits) -> unit = {
+  let ctr_idx = siselect.bits[7 .. 0];
+  if unsigned(siselect[REG]) >= 512 & unsigned(siselect[REG]) <= 767
+  then set_ctr_sireg3(v)
+}
+function set_sireg4(v: xlenbits) -> unit = ()
+function set_sireg5(v: xlenbits) -> unit = ()
+function set_sireg6(v: xlenbits) -> unit = ()
diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml
index 69f271496..50ddcd905 100644
--- a/ocaml_emulator/platform.ml
+++ b/ocaml_emulator/platform.ml
@@ -12,6 +12,9 @@ let config_enable_misaligned_access    = ref false
 let config_mtval_has_illegal_inst_bits = ref false
 let config_enable_svinval              = ref false
 let config_enable_zcb                  = ref false
+let config_enable_smctr                = ref false
+let config_enable_ssctr                = ref false
+let config_valid_ctr_depth             = ref Big_int.zero
 let config_enable_writable_fiom        = ref true
 let config_enable_vext                 = ref true
 let config_pmp_count                   = ref Big_int.zero
@@ -20,6 +23,8 @@ 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 set_valid_ctr_depth x = config_valid_ctr_depth := Big_int.of_int x
+
 let platform_arch = ref P.RV64
 
 (* logging *)
@@ -92,6 +97,9 @@ let enable_misaligned_access ()      = !config_enable_misaligned_access
 let mtval_has_illegal_inst_bits ()   = !config_mtval_has_illegal_inst_bits
 let enable_svinval ()                = !config_enable_svinval
 let enable_zcb ()                    = !config_enable_zcb
+let enable_smctr ()                  = !config_enable_smctr
+let enable_ssctr ()                  = !config_enable_ssctr
+let valid_ctr_depth ()               = !config_valid_ctr_depth
 let enable_zfinx ()                  = false
 let enable_writable_fiom ()          = !config_enable_writable_fiom
 let pmp_count ()                     = !config_pmp_count
diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml
index 56be8d8a8..5f7d4ca3d 100644
--- a/ocaml_emulator/riscv_ocaml_sim.ml
+++ b/ocaml_emulator/riscv_ocaml_sim.ml
@@ -89,6 +89,15 @@ let options = Arg.align ([("-dump-dts",
                           ("-with-dtc",
                            Arg.String PI.set_dtc,
                            " full path to dtc to use")
+                          ("-enable-smctr",
+                           Arg.Set P.config_enable_smctr,
+                           " enable Smctr extension");
+                          ("-enable-ssctr",
+                           Arg.Set P.config_enable_ssctr,
+                           " enable Ssctr extension");
+                          ("-valid-ctr-depth",
+                           Arg.Int P.set_config_valid_ctr_depth,
+                           " valid CTR depths");
                          ])
 
 let usage_msg = "RISC-V platform options:"