clarify writes to dinfc (#417)

#416

---------

Signed-off-by: Tariq Kurd <[email protected]>

src/csv/CHERI_ISA.csv

@@ -52,8 +52,8 @@
 "GCTYPE","✔","✔","","","","✔","✔","Both","","","","","","","","","","","","","","","","","OP","1-src 1-dst","","","Get capability type","","","","","","","",""
 "SCMODE","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","1-src 1-dst","","","Set the mode bit of a capability, no permissions required","","","","","","","",""
 "GCMODE","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","1-src 1-dst","","","Get the mode bit of a capability, no permissions required","","","","","","","",""
-"MODESW.CAP","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","no operands","","","Directly switch mode into {cheri_cap_mode_name}","mode==D (optional)","","","","","","",""
-"MODESW.INT","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","no operands","","","Directly switch mode into {cheri_int_mode_name}","mode==D (optional)","","","","","","",""
+"MODESW.CAP","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","no operands","","","Directly switch mode into {cheri_cap_mode_name}","","","","","","","",""
+"MODESW.INT","✔","✔","","","","✔","","Both","","","","","","","","","","","","","","","","","OP","no operands","","","Directly switch mode into {cheri_int_mode_name}","","","","","","","",""
 "C.ADDI16SP","✔","✔","","","","✔","✔","Both","","","","✔","","","","","","","","","","","","","C0","","","","ADD immediate to stack pointer, CADD in Capability Mode","","","","","","","",""
 "C.ADDI4SPN","✔","✔","","","","✔","✔","Both","","","","✔","","","","","","","","","","","","","C0","","","","ADD immediate to stack pointer, CADDI in Capability Mode","","","","","","","",""
 "C.MV","✔","✔","","","","✔","✔","Both","","","","✔","","","","","","","","","","","","","C2","","","","Register Move, cap reg move in Capability Mode","","","","","","","",""

src/debug-integration.adoc

@@ -180,13 +180,12 @@ The reset value is the <<infinite-cap>> capability.
 If {cheri_default_ext_name} is implemented:
 
 * The <<m_bit>> is reset to {cheri_int_mode_name} ({INT_MODE_VALUE}).
-* The debugger can set the <<m_bit>> to {cheri_cap_mode_name} ({CAP_MODE_VALUE}) by executing <<MODESW_CAP>> from the program buffer
-** if <<MODESW_CAP>> 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.
+* The debugger can set the <<m_bit>> to {cheri_cap_mode_name} ({CAP_MODE_VALUE}) by executing <<MODESW_CAP>> from the program buffer.
+** Executing <<MODESW_CAP>> causes the next instruction from the program buffer to be executed in {cheri_cap_mode_name}, and also sets the CHERI execution mode to {cheri_cap_mode_name} on future entry into debug mode.
+** Therefore to enable use of a CHERI debugger, a single <<MODESW_CAP>> only needs to be executed once from the program buffer after resetting the core.
+** The debugger can also execute <<MODESW_INT>> to change the mode back to {cheri_int_mode_name}, which also affects the execution of the next instruction in the program buffer, updates the <<m_bit>> of <<dinfc>> and controls which CHERI execution mode to enter on the next entry into debug mode.
 
-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.
+The <<m_bit>> of <<dinfc>> is _only_ updated by executing <<MODESW_CAP>> or <<MODESW_INT>> from the program buffer.
 
 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_32bit.adoc

@@ -23,11 +23,9 @@ Set the hart's current CHERI execution mode in <<pcc>>.
 * MODESW.CAP: 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}). Otherwise no effect.
 * MODESW.INT: If the current mode in <<pcc>> is {cheri_cap_mode_name} ({CAP_MODE_VALUE}), then the <<m_bit>> in <<pcc>> is set to {cheri_int_mode_name} ({INT_MODE_VALUE}). Otherwise no effect.
 
-NOTE: Implementations may optionally support executing <<MODESW_CAP>> and <<MODESW_INT>> from the
-program buffer while in debug mode. If supported then the <<m_bit>> in
-<<dinfc>> is set accordingly 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.
+NOTE: Executing <<MODESW_CAP>> or <<MODESW_INT>> from the program buffer in debug mode updates the <<m_bit>> of <<dinfc>>.
+ The <<m_bit>> of <<dinfc>> sets the CHERI execution mode for the execution of the next instruction from the program buffer, and is used to control which CHERI execution 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.
 
 Exceptions::
 include::require_cre.adoc[]

src/riscv-hybrid-integration.adoc

@@ -278,18 +278,16 @@ All CSR instructions cause CHERI exceptions if the <<pcc>> does not grant
 A new debug default data capability (<<dddc>>) CSR is added at the CSR number
 shown in xref:default-csrnames-added[xrefstyle=short].
 
-{cheri_default_ext_name} optionally allows <<MODESW_CAP>> and <<MODESW_INT>> to execute in debug mode.
+{cheri_default_ext_name} allows <<MODESW_CAP>> and <<MODESW_INT>> to execute in debug mode.
 
 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 <<MODESW_CAP>> or <<MODESW_INT>> from the program buffer.
 
 The current mode can be read from <<dinfc>>.
 
 ifdef::cheri_v9_annotations[]
 NOTE: *CHERI v9 Note:* The mode change instructions <<MODESW_CAP>> and <<MODESW_INT>> are new
-and the requirement to optionally support it in debug mode is also new.
+and the requirement to support them in debug mode is also new.
 endif::[]
 
 [#dddc,reftext="dddc"]