[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 #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.