[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 #25 from Samuel A. Falvo II <kc5tja at arrl.net> ---
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):
                    comb += Assert(o[0:32] == (rs << b[0:6])[0:32])
                    comb += Assert(o[32:64] == 0)
                with m.Else():
                    comb += DESIRED_sig.eq((rs << b[0:7])[0:64])
                    comb += Assert(o == DESIRED_sig)  #<--- assertion fails
here.


>From what I can discover, based on GTKWave investigation, it looks like the
Rotator module is operating in mode 0, which applies both mr and ml masks to
the output.  The problem is, while ml = 0xFFFFFFFFFFFFFFFF, mr is
0x0000000000000000.  This means that (ml & mr) == 0, which means the actual
rotator output is also zero.

This begs the question, when invoking an OP_SHL type instruction, where
mb=me=0, should it be operating in mode 0?  Should the masks be generated
differently for these types of instructions?  Etc.

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