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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Mon Sep 7 23:38:49 BST 2020


--- Comment #36 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #35)
> 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.

I added this to the test:

    comb += Assume(~rec.is_signed)
    comb += Assume(~dut.i.ctx.op.is_signed)

but this did not change the outcome.  :(

I'll report my results looking at the other things separately.

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

More information about the libre-soc-bugs mailing list