[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 #35 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
samuel it occurred to me that, just like in MUL, there may be some
spurious inputs being "wiggled" by the proof engine that should never
have been enabled in the first place.

examples of this include the "op.is_signed" flag - which should *definitely*
be False - for OP_SHL.

it may be worthwhile adding some Asserts on rotator itself

change this:

        # set up microwatt rotator module
        m.submodules.rotator = rotator = Rotator()

to this:

        # set up microwatt rotator module
        m.submodules.rotator = self.rotator = rotator = Rotator()

and that will allow you to get at it.

also:

        # instruction rotate type
        mode = Signal(4, reset_less=True)

change that to

        # instruction rotate type
        self.mode = mode = Signal(4, reset_less=True)

also it occurs to me that mb_extra - one of the key fields going in to
rotator - has not been set/asserted/assumed. 

therefore it could be adversely affecting the test.

the construction of mb and me *might* not be correct.  it's a little
more complicated (as you can see if you look in rotator.py) you have
to bring in a 6th bit... *sometimes*.

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