format code

[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 a955011d2fca1b54fad1690e4ae02795f3c62de6..c00a3fbff4a199b21be6ff5a82da9e754af2c7eb 100644 (file)
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -19,9 +19,9 @@ from nmigen.cli import rtlil
 from nmutil.extend import exts
 from nmutil.formaltest import FHDLTestCase
 
-from soc.consts import MSR, MSRb, PI, TT, field
+from openpower.consts import MSR, MSRb, PI, TT, field
 
-from soc.decoder.power_enums import MicrOp
+from openpower.decoder.power_enums import MicrOp
 
 from soc.fu.trap.main_stage import TrapMainStage
 from soc.fu.trap.pipe_data import TrapPipeSpec
@@ -64,7 +64,8 @@ class Driver(Elaboratable):
         # This alias exists because some of our assertions exceed PEP8
         # width constraints.  Avoid using this alias in the general
         # case; ONLY use it when you're simultaneously trying to preserve
-        # line-oriented readibility while preserving PEP8 compliance.
+        # line-oriented readability (to make the code easy to compare with
+        # the v3.0B spec) while simultaneously preserving PEP8 compliance.
         F = field
 
         # start of properties
@@ -120,6 +121,10 @@ class Driver(Elaboratable):
                 with m.If(take_trap):
                     comb += exp_msr.eq(op.msr)
 
+                    # these are all set depending on the trap address (type)
+                    # see V3.0B p1063 however as noted in main_stage.py
+                    # the types of interrupts supported all need the same
+                    # values (for now)
                     comb += field(exp_msr, MSRb.IR).eq(0)
                     comb += field(exp_msr, MSRb.DR).eq(0)
                     comb += field(exp_msr, MSRb.FE0).eq(0)
@@ -134,20 +139,6 @@ class Driver(Elaboratable):
                     comb += field(exp_msr, MSRb.FP).eq(0)
                     comb += field(exp_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(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
 
                     comb += field(exp_msr, MSRb.UND).eq(0)
@@ -185,22 +176,22 @@ class Driver(Elaboratable):
 
                 with m.If(L == 0):
                     comb += [
-                        field(exp_msr, 48).eq(F(rs, 48) | F(rs, 49)),
-                        field(exp_msr, 58).eq(F(rs, 58) | F(rs, 49)),
-                        field(exp_msr, 59).eq(F(rs, 59) | F(rs, 49)),
+                        field(exp_msr, 48).eq(field(rs, 48) | field(rs, 49)),
+                        field(exp_msr, 58).eq(field(rs, 58) | field(rs, 49)),
+                        field(exp_msr, 59).eq(field(rs, 59) | field(rs, 49)),
                         field(exp_msr, 32, 47).eq(field(rs, 32, 47)),
                         field(exp_msr, 49, 50).eq(field(rs, 49, 50)),
                         field(exp_msr, 52, 57).eq(field(rs, 52, 57)),
                         field(exp_msr, 60, 62).eq(field(rs, 60, 62)),
                     ]
                 with m.Else():
+                    # L=1 only checks 48 and 62
                     comb += [
                         field(exp_msr, 48).eq(field(rs, 48)),
                         field(exp_msr, 62).eq(field(rs, 62)),
                     ]
 
                 comb += [
-                    # L=1 only checks 48 and 62
                     Assert(msr_o.data == exp_msr),
                     Assert(msr_o.ok),
                 ]
@@ -211,7 +202,7 @@ class Driver(Elaboratable):
             ###################
 
             with m.Case(MicrOp.OP_MTMSRD):
-                msr_od = msr_o.data
+                msr_od = msr_o.data  # another "shortener"
 
                 with m.If(L == 0):
                     # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
@@ -225,15 +216,15 @@ class Driver(Elaboratable):
                     # MSR[48] <- (RS)[48] | (RS)[49]
                     # MSR[58] <- (RS)[58] | (RS)[49]
                     # MSR[59] <- (RS)[59] | (RS)[49]
-                    PR = field(rs, 49) # alias/copy of SRR1 PR field
+                    PR = field(rs, 49)  # alias/copy of SRR1 PR field
                     comb += [
-                        Assert(field(msr_od, 48) == F(rs, 48) | PR),
-                        Assert(field(msr_od, 58) == F(rs, 58) | PR),
-                        Assert(field(msr_od, 59) == F(rs, 59) | PR),
+                        Assert(field(msr_od, 48) == field(rs, 48) | PR),
+                        Assert(field(msr_od, 58) == field(rs, 58) | PR),
+                        Assert(field(msr_od, 59) == field(rs, 59) | PR),
                     ]
 
                     comb += [
-                        # XXX Ambiguity in specification on page 978 of V3.0B:
+                        # Ambiguity in specification on page 978 of V3.0B:
                         #   MSR[4:28] <- RS[4 6:28].
                         #
                         # I've decided to follow the prose in the programmer
@@ -250,7 +241,7 @@ class Driver(Elaboratable):
                         Assert(field(msr_od, 60, 62) == field(rs, 60, 62)),
                     ]
                 with m.Else():
-                    # L=1 only checks 48 and 62
+                    # L=1 only checks 48 and 62 (MSR.EE, MSR.RI)
                     comb += [
                         Assert(field(msr_od, 48) == field(rs, 48)),
                         Assert(field(msr_od, 62) == field(rs, 62)),
@@ -272,7 +263,7 @@ class Driver(Elaboratable):
             # RFID.  v3.0B p955
             ###################
             with m.Case(MicrOp.OP_RFID):
-                msr_od = msr_o.data
+                msr_od = msr_o.data  # another "shortener"
                 comb += [
                     Assert(msr_o.ok),
                     Assert(nia_o.ok),
@@ -289,7 +280,7 @@ class Driver(Elaboratable):
 
                 # 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) |
+                with m.If((field(msr_i, 29, 31) != 0b010) |
                           (field(srr1_i, 29, 31) != 0b000)):
                     comb += Assert(F(msr_od, 29, 31) == F(srr1_i, 29, 31))
                 with m.Else():
@@ -299,7 +290,7 @@ class Driver(Elaboratable):
                 # MSR[48] <- (RS)[48] | (RS)[49]
                 # MSR[58] <- (RS)[58] | (RS)[49]
                 # MSR[59] <- (RS)[59] | (RS)[49]
-                PR = field(srr1_i, 49) # alias/copy of SRR1 PR field
+                PR = field(srr1_i, 49)  # alias/copy of SRR1 PR field
                 comb += [
                     Assert(field(msr_od, 48) == field(srr1_i, 48) | PR),
                     Assert(field(msr_od, 58) == field(srr1_i, 58) | PR),
@@ -382,4 +373,3 @@ class TrapMainStageTestCase(FHDLTestCase):
 
 if __name__ == '__main__':
     unittest.main()
-