[Libre-soc-bugs] [Bug 325] create POWER9 TRAP pipeline

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=325

--- Comment #125 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
@@ -239,24 +211,6 @@ class Driver(Elaboratable):
                 comb += [
                     Assert(msr_o.ok),
                     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
-
-                comb += [
-                    # spec: MSR[3] <- (MSR[3] & SRR1[3])
-                    Assert(field(msr_o, 3) == (field(srr1_i, 3) &
-                                               field(msr_i, 3))), # HV
                 ]

                 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then


revert that in the proof.

-- 
You are receiving this mail because:
You are on the CC list for the bug.