[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 #28 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #25)
> I'm running into a situation where computing ((1ULL << 63) << 0) == 0
> instead of ((1ULL << 63) << 0) == (1ULL << 63).  
> 
>         # main assertion of arithmetic operations
>         with m.Switch(itype):
> 
>             # left-shift: 64/32-bit
>             with m.Case(MicrOp.OP_SHL):
>                 comb += Assume(ra == 0)
>                 with m.If(rec.is_32bit):

i think we should have "comb += Assume(b[5] == 0) here, to match the
behaviour of slw (v3.0B spec, p107)

>                     comb += Assert(o[0:32] == (rs << b[0:6])[0:32])
>                     comb += Assert(o[32:64] == 0)
>                 with m.Else():

add "comb += Assume(b[6] == 0) here and i believe things will "work"

>                     comb += DESIRED_sig.eq((rs << b[0:7])[0:64])
>                     comb += Assert(o == DESIRED_sig)  #<--- assertion fails
> here.

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