Review Sentinel's Reset State

[cr1901]

Section 3.4 of the Privileged Spec, emphasis mine, states:

Upon reset, a hart’s privilege mode is set to M. The mstatus fields MIE and MPRV are reset to 0. If
little-endian memory accesses are supported, the mstatus/mstatush field MBE is reset to 0. The misa
register is reset to enable the maximal set of supported extensions, as described in Section 3.1.1. For
implementations with the "A" standard extension, there is no valid load reservation. The pc is set to an
implementation-defined reset vector. The mcause register is set to a value indicating the cause of the
reset. Writable PMP registers’ A and L fields are set to 0, unless the platform mandates a different reset
value for some PMP registers’ A and L fields. If the hypervisor extension is implemented, the
hgatp.MODE and vsatp.MODE fields are reset to 0. If the Smrnmi extension is implemented, the
mnstatus.NMIE field is reset to 0. No WARL field contains an illegal value. All other hart state is
UNSPECIFIED.

The mcause values after reset have implementation-specific interpretation, but the value 0 should be
returned on implementations that do not distinguish different reset conditions. Implementations that
distinguish different reset conditions should only use 0 to indicate the most complete reset.

TODO when I have more bandwidth to add the relevant support code to doit: Check that the bold is true using k-induction/BMC in light of ac8fa67 and c21bd62. It should be true, because:

1. Re: MIE, CSRs can only be written using the ALU output, and that the ALU output is 0 after reset (implies ALU output can't be reset-less). So only zero can be written to MIE if the stale microcode entry requests a CSR write (not to mention, MIE is already reset to zero by reset).
2. WARL handling is done independently of the microcode program, so any stale zero values to other registers will fall under UNSPECIFIED.
3. Our MCAUSE doesn't distinguish reset conditions.

But can't hurt to check that these conditions actually hold vs "what I intend".

Use this patch and files as a starting point:

Patch

index c080c23..1770992 100644
--- a/src/sentinel/alu.py
+++ b/src/sentinel/alu.py
@@ -3,7 +3,7 @@ from .csr import MCause
 from .ucodefields import OpType, ALUIMod, ALUOMod, ASrc, BSrc, MemSel, \
     MemExtend

-from amaranth import Elaboratable, Signal, Module, C, Cat
+from amaranth import Assert, Elaboratable, ResetSignal, Signal, Module, C, Cat, Cover
 from amaranth.lib.wiring import Component, Signature, In, Out


@@ -261,4 +261,13 @@ class ALU(Component):
         # TODO: LSBS_2_ZERO for JALR/JAL misaligned exceptions?
         m.d.comb += self.ctrl.zero.eq(self.o == 0)

+        reset_prev_prev = Signal(reset_less=True)
+        reset_prev = Signal(reset_less=True)
+
+        m.d.sync += [reset_prev.eq(ResetSignal()),
+                     reset_prev_prev.eq(reset_prev)]
+
+        with m.If(reset_prev_prev):
+            m.d.comb += Cover(self.o != 0)
+
         return m

formal.ys

read_verilog -formal sen-cov.v
prep -top sentinel -nordff
clk2fflogic; opt_clean
write_smt2 -wires sen.smt2

Command

yosys-smtbmc -s boolector -c -t 100 --presat --dump-vcd alu-nonzero.vcd sen.smt2