Initial debug module support: regs, control.debugmod

4 files changed, 224 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index 2c8981a..72a6deb 100644
--- a/Makefile
+++ b/Makefile
@@ -33,6 +33,9 @@ SAIL_SYS_SRCS += riscv_next_control.sail    # helpers for the 'N' extension
 SAIL_SYS_SRCS += riscv_csr_ext.sail         # access to CSR extensions
 SAIL_SYS_SRCS += riscv_sys_control.sail     # general exception handling
 
+DBG_MODULE_SRCS = $(addprefix debug_module/,dm_regs.sail dm_control.sail riscv_debug_regs.sail)
+SAIL_SYS_SRCS += $(DBG_MODULE_SRCS)
+
 SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail
 SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail
 
diff --git a/model/debug_module/dm_control.sail b/model/debug_module/dm_control.sail
new file mode 100644
index 0000000..3ce07eb
--- /dev/null
+++ b/model/debug_module/dm_control.sail
@@ -0,0 +1,74 @@
+type dm_cmd_arg = bits(24)
+
+bitfield AccessRegisterArg : dm_cmd_arg = {
+  AARSize  : 22 .. 20,
+  PostExec : 18,
+  Transfer : 17,
+  Write    : 16,
+  Regno    : 15 .. 0
+}
+
+bitfield AccessMemoryArg : dm_cmd_arg = {
+  AAMVirtual       : 23,
+  AAMSize          : 22 .. 20,
+  AAMPostIncrement : 19,
+  Write            : 16,
+  TargetSpecific   : 15 .. 14
+}
+
+function dm_access_register(a : AccessRegisterArg) -> unit = {
+  // TODO: pg 11
+  ()
+}
+
+function dm_access_memory(a : AccessMemoryArg) -> unit = {
+  // TODO: pg 13
+  ()
+}
+
+function dm_exec_cmd (c : Command) -> unit = {
+  match c.CmdType() {
+    0x00 => dm_access_register(Mk_AccessRegisterArg(c.Control())),
+    0x01 => (), // Quick access not yet supported
+    0x02 => dm_access_memory(Mk_AccessMemoryArg(c.Control())),
+       _ => ()
+  }
+}
+
+val initDMRegs : bool -> unit   effect {wreg}
+val readDMReg  : dmiaddr -> dmlenbits effect {rreg}
+val writeDMReg : (dmiaddr, dmlenbits) -> unit effect {rreg, wreg}
+
+function initDMRegs (halted : bool) = {
+  data0    = zeros();
+  haltsum0 = EXTZ(if halted then 0b1 else 0b0);
+}
+
+function readDMReg (reg) = {
+  match reg {
+    0x04 => data0,
+    0x05 => data1,
+    0x06 => data2,
+    0x07 => data3,
+    0x10 => dmcontrol.bits(),
+    0x11 => dmstatus.bits(),
+    0x16 => abstractcs.bits(),
+    0x17 => command.bits(),
+    0x19 => devtreeaddr0,
+    0x40 => haltsum0,
+    _    => zeros()
+  }
+}
+
+function writeDMReg (reg, value) = {
+  match reg {
+    0x04 => { data0 = value },
+    0x05 => { data1 = value },
+    0x06 => { data2 = value },
+    0x07 => { data3 = value },
+    0x10 => { dmcontrol = legalize_dmcontrol(dmcontrol, Mk_DMControl(value)) },
+    0x16 => { abstractcs = legalize_abstractcs(abstractcs, Mk_AbstractCS(value)) },
+    0x17 => { command->bits() = value; dm_exec_cmd(command) },
+    _    => ()
+  }
+}
diff --git a/model/debug_module/dm_regs.sail b/model/debug_module/dm_regs.sail
new file mode 100644
index 0000000..ba20a7c
--- /dev/null
+++ b/model/debug_module/dm_regs.sail
@@ -0,0 +1,110 @@
+/* Debug module registers */
+
+/* The current implementation tries to rely on using the abstract
+ * command mechanism as far as possible (i.e. for accessing registers,
+ * and reading and writing memory).  It does not implement a program
+ * buffer or system bus access.
+ */
+
+type dmlenbits  = bits(32)
+
+/* DM register indices are specified as offsets from the base
+ * address of the DM module on the DMI bus.
+ */
+type dmiaddr = bits(8)
+
+bitfield DMStatus : dmlenbits = {
+  ImpEbreak      : 22,
+  AllHaveReset   : 19,
+  AnyHaveReset   : 18,
+  AllResumeAck   : 17,
+  AnyResumeAck   : 16,
+  AllNonExistent : 15,
+  AnyNonExistent : 14,
+  AllUnavail     : 13,
+  AnyUnavail     : 12,
+  AllRunning     : 11,
+  AnyRunning     : 10,
+  AllHalted      :  9,
+  AnyHalted      :  8,
+
+  Authenticated   : 7,
+  AuthBusy        : 6,
+  HasResetHaltReq : 5,
+  DevTreeValid    : 4,
+  Version         : 3 .. 0,
+}
+register dmstatus : DMStatus
+
+bitfield DMControl : dmlenbits = {
+  HaltReq         : 31,
+  ResumeReq       : 30,
+  HartReset       : 29,
+  AckHaveReset    : 28,
+  HaSel           : 26,
+  HartSelLo       : 16,  // HARTSELLEN = 1
+  SetResetHaltReq : 3,
+  ClrResetHaltReq : 2,
+  NDMReset        : 1,
+  DMActive        : 0
+}
+register dmcontrol : DMControl
+
+function legalize_dmcontrol(c : DMControl, v : DMControl) -> DMControl = {
+  // TODO: implement control actions
+  let c = update_HaltReq(c, v.HaltReq());
+  let c = update_ResumeReq(c, v.ResumeReq());
+  let c = update_HartReset(c, v.HartReset());
+  let c = update_AckHaveReset(c, v.AckHaveReset());
+  let c = update_HaSel(c, v.HaSel());
+  let c = update_HartSelLo(c, v.HartSelLo());
+  let c = update_SetResetHaltReq(c, v.SetResetHaltReq());
+  let c = update_ClrResetHaltReq(c, v.ClrResetHaltReq());
+  c
+}
+
+bitfield AbstractCS : dmlenbits = {
+  ProgBufSize : 28 .. 24,
+  Busy        : 12,
+  CmdErr      : 10 ..  8,
+  DataCount   :  3 ..  0
+}
+register abstractcs : AbstractCS
+
+function legalize_abstractcs(cs : AbstractCS, v : AbstractCS) -> AbstractCS = {
+  let cs = update_CmdErr(cs, cs.CmdErr() & (~ (v.CmdErr())));
+  cs
+}
+
+bitfield Command : dmlenbits = {
+  CmdType : 31 .. 24,
+  Control : 23 ..  0
+}
+register command : Command
+
+// TODO: Remove if not needed.
+bitfield SBCS : dmlenbits = {
+  SBVersion       : 31 .. 29,
+  SBBusyError     : 22,
+  SBBusy          : 21,
+  SBReadOnAddr    : 20,
+  SBAccess        : 19 .. 17,
+  SBAutoIncrement : 16,
+  SBReadOnData    : 15,
+  SBError         : 14,
+  SBASize         : 11 .. 5,
+  SBAccess128     :  4,
+  SBAccess64      :  3,
+  SBAccess32      :  2,
+  SBAccess16      :  1,
+  SBAccess8       :  0
+}
+register sbcs : SBCS
+
+register devtreeaddr0 : dmlenbits
+register haltsum0     : dmlenbits
+
+register data0 : dmlenbits
+register data1 : dmlenbits
+register data2 : dmlenbits
+register data3 : dmlenbits
diff --git a/model/debug_module/riscv_debug_regs.sail b/model/debug_module/riscv_debug_regs.sail
new file mode 100644
index 0000000..f84d66f
--- /dev/null
+++ b/model/debug_module/riscv_debug_regs.sail
@@ -0,0 +1,37 @@
+/* These are additional CSRs added to the CSR address space by the debug mode. */
+
+bitfield DCSR : dmlenbits = {
+  XDebugVer : 31 .. 28,
+  EBreakM   : 15,
+  EBreakS   : 13,
+  EBreakU   : 12,
+  StepIE    : 11,
+  StopCount : 10,
+  StopTime  : 9,
+  Cause     : 8 .. 6,
+  MPrvEn    : 4,
+  NMIP      : 3,
+  Step      : 2,
+  Prv       : 1 .. 0
+}
+register dcsr : DCSR
+
+function legalize_dcsr(d : DCSR, v : DCSR) -> DCSR = {
+  let d = update_EBreakM(d, v.EBreakM());
+  let d = if haveSupMode() then update_EBreakS(d, v.EBreakS()) else d;
+  let d = if haveUsrMode() then update_EBreakU(d, v.EBreakU()) else d;
+  let d = update_StepIE(d, v.StepIE());
+  let d = update_StopCount(d, v.StopCount());
+  let d = update_StopTime(d, v.StopTime());
+  let d = update_MPrvEn(d, v.MPrvEn());
+  let d = update_Step(d, v.Step());
+  let d : DCSR = match privLevel_of_bits(v.Prv()) {
+                   Machine    => update_Prv(d, v.Prv()),
+                   Supervisor => if haveSupMode() then update_Prv(d, v.Prv()) else d,
+                   User       => if haveUsrMode() then update_Prv(d, v.Prv()) else d
+                 };
+  d
+}
+
+register dpc : xlenbits
+