code review comments for trap and proof

diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py
index 823a58f29891bf72b0a612b8488e29b78b459f5c..52218efb613dfab2d89008a149d3437a91a89fa8 100644 (file)
--- a/src/soc/fu/trap/formal/proof_main_stage.py
+++ b/src/soc/fu/trap/formal/proof_main_stage.py
@@ -120,14 +120,29 @@ 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
                     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)
+                    # note here: 36 is ***LESS*** than 32  ***BUT***
+                    # ***63-36*** is less than 63-32
+                    # could do with using field_slice here however
+                    # *get the number order right*.
+
+                    # however before doing that: why are these bits
+                    # initialised to zero then every single one of them
+                    # is over-ridden?  5 bits, 32-36 (36-32, haha)
+                    # are set to zero, then 5 bits are set to expressions.
+
+                    # redundant 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])
@@ -169,6 +184,10 @@ 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)
+                # XXX no.  slice quantity still inverted producing an empty list
+                # https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
+                # also add a comment explaining this very non-obvious
+                # behaviour
                 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)
@@ -197,6 +216,13 @@ class Driver(Elaboratable):
                     Assert(nia_o.ok),
                 ]
 
+                # XXX code comment has been removed, which explains
+                # why the code is written the way it is written
+                # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c127
+
+                # XXX restore HV check
+                # https://bugs.libre-soc.org/show_bug.cgi?id=325#c125
+
                 # 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,6 +234,9 @@ class Driver(Elaboratable):
                                    field(msr_i, 29, 31))
 
                 # check EE (48) IR (58), DR (59): PR (49) will over-ride
+
+                # XXX does not look as clear.  revert
+                # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c122
                 for bit in [48, 58, 59]:
                     comb += Assert(
                         field(msr_o, bit) ==

diff --git a/src/soc/fu/trap/main_stage.py b/src/soc/fu/trap/main_stage.py
index 1632bfb167b2ba1bdd3f59684f3208acdfdda2aa..43bc2c24cd287f82056c6b068c7237ec634a3f7b 100644 (file)
--- a/src/soc/fu/trap/main_stage.py
+++ b/src/soc/fu/trap/main_stage.py
@@ -103,6 +103,10 @@ class TrapMainStage(PipeModBase):
         comb += msr_o.data[MSR.VEC].eq(0)
         comb += msr_o.data[MSR.FP].eq(0)
         comb += msr_o.data[MSR.PMM].eq(0)
+        # XXX no.  slice quantity still inverted producing an empty list
+        # https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
+        # also add a comment explaining this very non-obvious
+        # behaviour.
         comb += field(msr_o.data, MSRb.TEs, MSRb.TEe).eq(0)
         comb += msr_o.data[MSR.UND].eq(0)
         if msr_hv is not None:
@@ -218,11 +222,16 @@ class TrapMainStage(PipeModBase):
                         for stt, end in [(1,12), (13, 32)]:
                             comb += msr_o.data[stt:end].eq(a_i[stt:end])
                     msr_check_pr(m, msr_o.data)
+
+                    # XXX code removed, needs reverting.
+                    # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c124
+                    # XXX
+
                 comb += msr_o.ok.eq(1)
 
             # move from MSR
             with m.Case(MicrOp.OP_MFMSR):
-                # TODO: some of the bits need zeroing?  apparently not
+                # some of the bits need zeroing?  apparently not
                 comb += o.data.eq(msr_i)
                 comb += o.ok.eq(1)
 
@@ -242,6 +251,11 @@ class TrapMainStage(PipeModBase):
 
                 # don't understand but it's in the spec.  again: bits 32-34
                 # are copied from srr1_i and need *restoring* to msr_i
+
+                # XXX bug introduced here.  this needs to be field_slice(31, 29)
+                # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c126
+                # XXX
+
                 bits = field_slice(29, 31)  # bits 29, 30, 31 (Power notation)
                 with m.If((msr_i[bits] == Const(0b010, 3)) &
                           (srr1_i[bits] == Const(0b000, 3))):
@@ -257,16 +271,8 @@ class TrapMainStage(PipeModBase):
                 # According to V3.0B, Book II, section 3.3.1, the System Call
                 # instruction allows you to trap directly into the hypervisor
                 # if the opcode's LEV sub-field is equal to 1.
-
-                # XXX see https://bugs.libre-soc.org/show_bug.cgi?id=325#c104
-                # do not access op.insn bits directly: PowerISA requires
-                # that fields be REVERSED and that has not been done here,
-                # where self.fields.FormNNN has that handled.
-
-                # in addition, we are following *microwatt* - which has
-                # not implemented hypervisor.  therefore this is incorrect
-                # behaviour.  see execute1.vhdl
-                # https://github.com/antonblanchard/microwatt/
+                # however we are following *microwatt* - which has
+                # not implemented hypervisor.
 
                 # jump to the trap address, return at cia+4
                 self.trap(m, 0xc00, cia_i+4)