controlling the cheri mode to enter when entering debug mode

src/debug-integration.adoc

@@ -5,9 +5,6 @@ This section describes changes to integrate the Sdext ISA and
 {cheri_base_ext_name}. It must be implemented to make external debug compatible
 with {cheri_base_ext_name}. Modifications to Sdext are kept to a minimum.
 
-WARNING: This section is preliminary as no-one has yet built debug support
- for CHERI-RISC-V so change is likely.
-
 The following features, which are optional in Sdext, must be implemented for
 use with {cheri_base_ext_name}:
 
@@ -178,12 +175,18 @@ include::img/dscratch1creg.edn[]
 
 The <<dinfc>> register is a CLEN-bit plus tag bit CSR only accessible in debug mode.
 
-The reset value is the <<infinite-cap>> capability with the <<m_bit>> set to {CAP_MODE_VALUE},
-regardless of whether {cheri_default_ext_name} (see xref:section-cheri-execution-mode[xrefstyle=short])
-is implemented:
+The reset value is the <<infinite-cap>> capability.
+
+If {cheri_default_ext_name} is implemented:
+
+* The <<m_bit>> is reset to be {cheri_default_ext_name} ({INT_MODE_VALUE}).
+* The debugger can set the <<m_bit>> to {cheri_base_mode_ext} ({CAP_MODE_VALUE}) by executing <<MODESW>> from the program buffer
+** if <<MODESW>> is not supported in debug mode then the same can be done by reading the CSR, using <<SCMODE>> and then writing the CSR.
+** This only needs doing once after resetting the core.
+* The <<m_bit>> is used on debug mode entry to determine which CHERI execution mode to enter.
 
-<<dinfc>> is read/write but with no writeable fields, and so writes are
-ignored.
+The <<m_bit>> is the only writeable field in <<dinfc>>.
+Therefore if {cheri_default_ext_name} is not implemented then it is read-write with no writeable fields.
 
 NOTE: A future version of this specification may add writeable fields to allow creation
  of other capabilities, if, for example, a future extension requires multiple formats for

src/insns/modesw_16bit.adoc

@@ -9,7 +9,7 @@ NOTE: *CHERI v9 Note:* This instruction is *new*.
 endif::[]
 
 Synopsis::
-Capability/{cheri_int_mode_name} switching (C.MODESW), 16-bit encoding
+{cheri_cap_mode_name}/{cheri_int_mode_name} switching (C.MODESW), 16-bit encoding
 
 Mnemonic::
 `c.modesw`

src/insns/modesw_32bit.adoc

@@ -6,7 +6,7 @@
 include::new_encoding_note.adoc[]
 
 Synopsis::
-Switch CHERI execution mode
+{cheri_cap_mode_name}/{cheri_int_mode_name} switching (MODESW), 32-bit encoding
 
 Mnemonic::
 `modesw`

src/insns/modesw_common.adoc

@@ -5,10 +5,13 @@ Toggle the hart's current CHERI execution mode in <<pcc>>.
 * If the current mode in <<pcc>> is {cheri_int_mode_name} ({INT_MODE_VALUE}), then the <<m_bit>> in <<pcc>> is set to {cheri_cap_mode_name} ({CAP_MODE_VALUE}).
 * If the current mode is {cheri_cap_mode_name} ({CAP_MODE_VALUE}), then the <<m_bit>> in <<pcc>> is set to {cheri_int_mode_name} ({INT_MODE_VALUE}).
 
-NOTE: The effective CHERI exection mode is give by the value of some CSRs and
+NOTE: The effective CHERI execution mode is give by the value of some CSRs and
 the <<pcc>>'s <<m_bit>>, so executing <<MODESW>> does not necessarily change
 the machine's current mode. The current, effective CHERI execution mode can be
 observed as described in xref:m_bit_observe[xrefstyle=short].
 
-NOTE: Implementations may optionally support executing <<C_MODESW>> from the
-program buffer while in debug mode.
+NOTE: Implementations may optionally support executing <<MODESW>> from the
+program buffer while in debug mode. If supported them the <<m_bit>> in
+<<dinfc>> is toggled and used to control which mode to enter next time debug
+mode is entered. The CHERI execution mode is only controlled by the <<m_bit>>
+of <<dinfc>> in debug mode.

src/riscv-hybrid-integration.adoc

@@ -99,8 +99,8 @@ write {CAP_MODE_VALUE} for {cheri_cap_mode_name} and
 {INT_MODE_VALUE} for {cheri_int_mode_name} to `x1`:
 
 ```
-csrr  c1, dinfc
-gctag x1, c1
+csrr   c1, dinfc
+gcmode x1, c1
 ```
 
 In any other privilege mode, the following sequence will write {CAP_MODE_VALUE}
@@ -279,9 +279,12 @@ shown in xref:default-csrnames-added[xrefstyle=short].
 
 {cheri_default_ext_name} optionally allows <<MODESW>> to execute in debug mode.
 
-When entering debug mode, the core always enters {cheri_cap_mode_name}.
+When entering debug mode, whether the core enters {cheri_int_mode_name} or
+{cheri_cap_mode_name} is controlled by the <<m_bit>> in <<dinfc>>.
 Implementations may optionally support switching CHERI execution mode by
-executing the <<MODESW>> from the program buffer.
+executing <<MODESW>> from the program buffer.
+
+The current mode can be read from <<dinfc>>.
 
 ifdef::cheri_v9_annotations[]
 NOTE: *CHERI v9 Note:* The mode change instruction <<MODESW>> is new

src/trigger-integration.adoc

@@ -9,7 +9,7 @@ shown in xref:trigger-exception-priority[xrefstyle=short].
 .Synchronous exception priority (including triggers) in decreasing priority order. Entries added in {cheri_base_ext_name} are in *bold*
 [%autowidth,float="center",align="center",cols="<,>,<,<",options="header"]
 |===
-|Priority |Exc.Code |Description |Trigger
+|Priority |Exc. Code |Description |Trigger
 |_Highest_ |3 +
 3 +
 3 +