WIP: SC properties more closely match doc'd behavior

[soc.git] / src / soc / fu / trap / formal / proof_main_stage.py

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index 823a58f29891bf72b0a612b8488e29b78b459f5c..1816afacbcbcc9aae19dd94e066e9f1793aa729d 100644 (file)
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -120,20 +120,37 @@ class Driver(Elaboratable):
                     comb += field(expected_msr, MSRb.PR).eq(0)
                     comb += field(expected_msr, MSRb.FP).eq(0)
                     comb += field(expected_msr, MSRb.PMM).eq(0)
+
+                    # still wrong.
+                    # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
+                    #
+                    # saf2: no it's not.  Proof by substitution:
+                    #
+                    # field(R,MSRb.TEs,MSRb.TEe).eq(0)
+                    # == field(R,53,54).eq(0)
+                    # == R[field_slice(53,54)].eq(0)
+                    # == R[slice(63-54, (63-53)+1)].eq(0)
+                    # == R[slice(9, 11)].eq(0)
+                    # == R[9:11].eq(0)
+                    #
+                    # Also put proof in py-doc for field().
+
                     comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
+
                     comb += field(expected_msr, MSRb.UND).eq(0)
                     comb += field(expected_msr, MSRb.LE).eq(1)
 
                     expected_srr1 = Signal(len(srr1_o.data))
                     comb += expected_srr1.eq(op.msr)
 
-                    comb += expected_srr1[63-36:63-32].eq(0)
-                    comb += expected_srr1[PI.TRAP].eq(traptype == 0)
-                    comb += expected_srr1[PI.PRIV].eq(traptype[1])
-                    comb += expected_srr1[PI.FP].eq(traptype[0])
-                    comb += expected_srr1[PI.ADR].eq(traptype[3])
-                    comb += expected_srr1[PI.ILLEG].eq(traptype[4])
-                    comb += expected_srr1[PI.TM_BAD_THING].eq(0)
+                    # Per V3.0B, page 1075
+                    comb += field(expected_srr1, 33, 36).eq(0)
+                    comb += field(expected_srr1, 42).eq(0)  # TM_BAD_THING
+                    comb += field(expected_srr1, 43).eq(traptype[0])    # FP
+                    comb += field(expected_srr1, 44).eq(traptype[4])    # ILLEG
+                    comb += field(expected_srr1, 45).eq(traptype[1])    # PRIV
+                    comb += field(expected_srr1, 46).eq(traptype == 0)  # TRAP
+                    comb += field(expected_srr1, 47).eq(traptype[3])    # ADDR
 
                     comb += [
                         Assert(msr_o.ok),
@@ -197,6 +214,18 @@ class Driver(Elaboratable):
                     Assert(nia_o.ok),
                 ]
 
+                # Note: going through the spec pseudo-code, line-by-line,
+                # in order, with these assertions.  idea is: compare
+                # *directly* against the pseudo-code.  therefore, leave
+                # numbering in (from pseudo-code) and add *comments* about
+                # which field it is (3 == HV etc.)
+
+                # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
+                with m.If(field(msr_i, 3)): # HV
+                    comb += Assert(field(msr_o, 51) == field(srr1_i, 51)) # ME
+                with m.Else():
+                    comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME
+
                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
                 #     MSR[29:31] <- SRR1[29:31]
                 with m.If((field(msr_i , 29, 31) != 0b010) |
@@ -208,11 +237,20 @@ class Driver(Elaboratable):
                                    field(msr_i, 29, 31))
 
                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
-                for bit in [48, 58, 59]:
-                    comb += Assert(
-                        field(msr_o, bit) ==
-                        (field(srr1_i, bit) | field(srr1_i, 49))
-                    )
+                comb += [
+                    Assert(
+                        field(msr_o, 48) ==
+                        field(srr1_i, 48) | field(srr1_i, 49)
+                    ),
+                    Assert(
+                        field(msr_o, 58) ==
+                        field(srr1_i, 58) | field(srr1_i, 49)
+                    ),
+                    Assert(
+                        field(msr_o, 59) ==
+                        field(srr1_i, 59) | field(srr1_i, 49)
+                    ),
+                ]
 
                 # remaining bits: straight copy.  don't know what these are:
                 # just trust the v3.0B spec is correct.