Sdtrig support

.gitignore

@@ -7,3 +7,8 @@ _sbuild/
 *.o
 *.a
 /z3_problems
+c_emulator/riscv_sim_RV32
+c_emulator/riscv_sim_RV64
+c_emulator/riscv_rvfi_RV64
+ocaml_emulator/riscv_ocaml_sim_RV64
+ocaml_emulator/riscv_ocaml_sim_RV32

c_emulator/riscv_platform.c

@@ -47,6 +47,11 @@ bool sys_enable_zfinx(unit u)
   return rv_enable_zfinx;
 }
 
+bool sys_enable_sdtrig(unit u)
+{
+  return rv_enable_sdtrig;
+}
+
 bool sys_enable_writable_fiom(unit u)
 {
   return rv_enable_writable_fiom;

c_emulator/riscv_platform.h

@@ -4,6 +4,7 @@
 bool sys_enable_rvc(unit);
 bool sys_enable_next(unit);
 bool sys_enable_fdext(unit);
+bool sys_enable_sdtrig(unit);
 bool sys_enable_svinval(unit);
 bool sys_enable_zcb(unit);
 bool sys_enable_zfinx(unit);

c_emulator/riscv_platform_impl.c

@@ -9,6 +9,7 @@ uint64_t rv_pmp_grain = 0;
 bool rv_enable_svinval = false;
 bool rv_enable_zcb = false;
 bool rv_enable_zfinx = false;
+bool rv_enable_sdtrig = false;
 bool rv_enable_rvc = true;
 bool rv_enable_next = false;
 bool rv_enable_writable_misa = true;

c_emulator/riscv_platform_impl.h

@@ -17,6 +17,7 @@ extern bool rv_enable_zfinx;
 extern bool rv_enable_rvc;
 extern bool rv_enable_next;
 extern bool rv_enable_fdext;
+extern bool rv_enable_sdtrig;
 extern bool rv_enable_vext;
 extern bool rv_enable_writable_misa;
 extern bool rv_enable_dirty_update;

c_emulator/riscv_sim.c

@@ -54,6 +54,7 @@ const char *RV32ISA = "RV32IMAC";
 #define OPT_PMP_COUNT 1002
 #define OPT_PMP_GRAIN 1003
 #define OPT_ENABLE_SVINVAL 1004
+#define OPT_ENABLE_SDTRIG 1005
 #define OPT_ENABLE_ZCB 10014
 
 static bool do_dump_dts = false;
@@ -149,6 +150,7 @@ 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          },
+    {"enable-sdtrig",               no_argument,       0, OPT_ENABLE_SDTRIG       },
 #ifdef SAILCOV
     {"sailcov-file",                required_argument, 0, 'c'                     },
 #endif
@@ -394,6 +396,10 @@ static int process_args(int argc, char **argv)
       fprintf(stderr, "enabling Zcb extension.\n");
       rv_enable_zcb = true;
       break;
+    case OPT_ENABLE_SDTRIG:
+      fprintf(stderr, "enabling sdtrig extension.\n");
+      rv_enable_sdtrig = true;
+      break;
     case 'x':
       fprintf(stderr, "enabling Zfinx support.\n");
       rv_enable_zfinx = true;

handwritten_support/riscv_extras.lem

@@ -161,6 +161,10 @@ val sys_enable_zfinx : unit -> bool
 let sys_enable_zfinx () = false
 declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
 
+val sys_enable_sdtrig : unit -> bool
+let sys_enable_sdtrig () = false
+declare ocaml target_rep function sys_enable_sdtrig = `Platform.enable_sdtrig`
+
 val sys_enable_vext : unit -> bool
 let sys_enable_vext () = true
 declare ocaml target_rep function sys_enable_vext = `Platform.enable_vext`

handwritten_support/riscv_extras.v

@@ -200,6 +200,7 @@ Axiom sys_enable_rvc : unit -> bool.
 Axiom sys_enable_fdext : unit -> bool.
 Axiom sys_enable_next : unit -> bool.
 Axiom sys_enable_zfinx : unit -> bool.
+Axiom sys_enable_sdtrig : unit -> bool.
 Axiom sys_enable_writable_fiom : unit -> bool.
 
 (* The constraint solver can do this itself, but a Coq bug puts

handwritten_support/riscv_extras_sequential.lem

@@ -149,6 +149,10 @@ val sys_enable_zfinx : unit -> bool
 let sys_enable_zfinx () = false
 declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
 
+val sys_enable_sdtrig : unit -> bool
+let sys_enable_sdtrig () = false
+declare ocaml target_rep function sys_enable_sdtrig = `Platform.enable_sdtrig`
+
 val sys_enable_next : unit -> bool
 let sys_enable_next () = true
 declare ocaml target_rep function sys_enable_next = `Platform.enable_next`

model/riscv_csr_map.sail

@@ -168,6 +168,8 @@ 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"
+mapping clause csr_name_map = 0x7a4  <-> "tinfo"
+mapping clause csr_name_map = 0x7a5  <-> "tcontrol"
 /* vector csrs */
 mapping clause csr_name_map = 0x008  <-> "vstart"
 mapping clause csr_name_map = 0x009  <-> "vxsat"

model/riscv_insts_zicsr.sail

@@ -72,7 +72,12 @@ function readCSR csr : csreg -> xlenbits = {
     (0xC22, _) => vlenb,
 
     /* trigger/debug */
-    (0x7a0,  _) => ~(tselect),  /* this indicates we don't have any trigger support */
+    (0x7a0,  _) => tselect.bits,
+    (0x7a1,  _) => tdata1.bits,
+    (0x7a2,  _) => tdata2,
+    (0x7a3,  _) => tdata3,
+    (0x7a4,  _) => legalize_tinfo(tinfo),
+    (0x7a5,  _) => tcontrol.bits,
 
     /* supervisor mode */
     (0x100,  _) => lower_mstatus(mstatus).bits,
@@ -153,7 +158,12 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0xB82, 32) => { minstret[63 .. 32] = value; minstret_increment = false; Some(value) },
 
     /* trigger/debug */
-    (0x7a0,  _) => { tselect = value; Some(tselect) },
+    (0x7a0,  _) => { tselect = legalize_tselect(tselect, value); Some(tselect.bits) },
+    (0x7a1, _) => { tdata1 = legalize_tdata1(tdata1, value); Some(tdata1.bits) },
+    // (0x7a2,  _) => { tdata2[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    // (0x7a3,  _) => { tdata3[(sizeof(xlen) - 1) .. 0] = value; Some(value) },
+    (0x7a4, _) => { Some(tinfo.bits) },       // ignoring Writes to Tinfo
+    (0x7a5, _) => { tcontrol = legalize_tcontrol(tcontrol, value); Some(tcontrol.bits) },
 
     /* supervisor mode */
     (0x100,  _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits) },

model/riscv_sys_control.sail

@@ -57,6 +57,11 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
 
     /* disabled trigger/debug module */
     0x7a0 => p == Machine,
+    0x7a1 => p == Machine,
+    0x7a2 => p == Machine,
+    0x7a3 => p == Machine,
+    0x7a4 => p == Machine,
+    0x7a5 => p == Machine,
 
     /* supervisor mode: trap setup */
     0x100 => haveSupMode() & (p == Machine | p == Supervisor), // sstatus