[Libre-soc-bugs] [Bug 340] formal proof of POWER9 SHIFTROT pipeline needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #13 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
samuel i added this to the unit test: it passes.

--- a/src/soc/fu/shift_rot/test/test_pipe_caller.py
+++ b/src/soc/fu/shift_rot/test/test_pipe_caller.py
@@ -77,6 +77,14 @@ def set_alu_inputs(alu, dec2, sim):

 class ShiftRotTestCase(TestAccumulatorBase):

+    def case_0_proof_regression_rlwnm(self):
+        lst = ["rlwnm 3, 1, 2, 16, 20"]
+        initial_regs = [0] * 32
+        initial_regs[1] = 0x7ffdbffb91b906b9
+        initial_regs[2] = 31
+        print(initial_regs[1], initial_regs[2])
+        self.add_case(Program(lst, bigendian), initial_regs)
+

ah i think i know why.

look in rotator.py:

            with m.Case(0b00):
                comb += self.result_o.eq((rot & (mr & ml)) | (ra & ~(mr & ml)))
            with m.Case(0b01):
                comb += self.result_o.eq((rot & (mr | ml)) | (ra & ~(mr | ml)))


and the only (corresponding) case in the proof is:

                comb += exp_ol.eq(field((exp_rot & mrl) | (ainp & ~mrl),


so the detection for when the mask beginning is at the opposite end i.e.
(greater or less?) than the mask end, is missing.

basically from the spec:

    "A mask is generated having 1-bits from bit MB+32 through
     bit ME+32 and 0-bits elsewhere."

this mask actually *rotates* and hence the inversion thing above.

notice that the OR of mr and ml produces 0xffffffff? (MASK_FOR_RLC)

that should be 0x0000f800 because they are supposed to be ANDed

ml = 0xffffff800
mr = 0x00000ffff

and when 0x0000f800 is ANDed with the input it produces the correct
answer which is 0x00008000

however because the mask is ORed together (which it should not be)

                comb += mrl.eq(ml | mr)

the proof *incorrectly* asserts the correct output as being untrue.

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