DRET clarification (#1045)

replacement for #1044 which got messed up on a rebase
@JanMatCodasip can you review this one please instead? let's work from
here.

fix #1043

---------

Signed-off-by: Tariq Kurd <tariq.kurd@codasip.com>
Co-authored-by: Jan Matyas <50193733+JanMatCodasip@users.noreply.github.com>

Author: tariqkurd-repo

src/cheri/debug-integration.adoc

@@ -138,7 +138,8 @@ The <<dpc>> register is extended to hold a capability.
 include::img/dpccreg.edn[]
 
 Upon entry to debug mode, the _RISC-V Debug Specification_, does not specify how to
-update the PC, and says PC-relative instructions may be illegal. This concept
+When the hart is in debug mode, the _RISC-V Debug Specification_ does not specify
+how the PC is updated, and says that PC-relative instructions may be illegal. This concept
 is extended to include any instruction which reads or updates <<pcc>>, which refers to
 all jumps, conditional branches and <<AUIPC_CHERI>>. The exceptions are <<MODESW_CAP>> and <<MODESW_INT>>,
 which _are_ supported if {cheri_default_ext_name} is implemented, see <<drootc>>
@@ -151,13 +152,21 @@ instruction execution.
 
 On debug mode entry, <<dpc_y>> is updated with the
 capability in <<pcc>> whose address field is set to the address of the next
+On debug mode entry, <<dpc_y>> is updated with the
+capability in <<pcc>>, whose address field equals to the address of the next
 instruction to be executed upon debug mode exit as described in the _RISC-V Debug Specification_.
 
-When leaving debug mode, an unsealed capability value is copied from the value in <<dpc_y>> and written into <<pcc>>.
-A debugger may write <<dpc_y>> to change where the hart resumes and its mode, permissions, sealing or bounds.
+When leaving debug mode, the value in <<dpc_y>> is unsealed if it is a <<sentry_cap>> and is written to <<pcc>>.
+
+NOTE: A debugger may write <<dpc_y>> to change where the hart resumes and its mode, permissions, sealing or bounds.
+ The value saved from the <<pcc>> on debug mode entry cannot be sealed.
 
 The legalization of <<dpc_y>> follows the same rules described for <<mepc_y>>.
 
+One possible implementation choice for debug mode exit is DRET.
+
+include::insns/dret.adoc[leveloffset=+1]
+
 [#dscratch0_y,reftext="dscratch0 ({cheri_base_ext_name})"]
 ==== Debug Scratch Register 0 (dscratch0)
 
@@ -219,11 +228,6 @@ The <<p_bit>> of this capability is _only_ updated by executing <<MODESW_CAP>> o
 .Debug root capability register
 include::img/drootcreg.edn[]
 
-==== Modified Trap-Return Instruction Behavior
-The <<DRET_CHERI>> instruction reads the full YLEN bits of the <<mepc_y>>/<<sepc_y>> register and unseals it prior to exception return if it is a <<sentry_cap>>.
-
-include::insns/dret.adoc[leveloffset=+1]
-
 [#section_hybrid_debug_integration]
 === Integrating {cheri_default_ext_name} with Sdext
 

src/cheri/insns/dret.adoc

@@ -13,12 +13,13 @@ Encoding::
 include::wavedrom/dret.adoc[]
 
 Description::
-<<DRET_CHERI>> returns from debug mode. It unseals <<dpc_y>> and writes the result into
-<<pcc>>.
+<<DRET_CHERI>> returns from debug mode.
+It unseals <<dpc_y>> if it is sealed as a <<sentry_cap>> and writes the result into <<pcc>>.
+It also restores <<ddc>> from <<dddc>>.
 
 NOTE: The <<DRET_CHERI>> instruction is a documented method of exiting debug mode.
 However, it is a pseudoinstruction to return that technically does not execute
-from the program buffer or memory. It currently does not require the <<pcc>> to
+from the program buffer or memory. It does not require the <<pcc>> to
 grant <<asr_perm>> so it never raises an exception.
 
 NOTE: The definition of `DRET` is not part of Sdext, and is a suggested as an implementation choice in the _RISC-V Debug Specification_.