[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 #20 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #19)
> (rot & ~(mr | ml)) | (ra & ~(mr & ml)))
> 
> see how they're the bit-opposite?

This doesn't satisfy DeMorgan's Theorem identities:

x AND y = ~(~x OR ~y)

It looks like you'll also need to invert mr and ml on the left-hand
transformation as well.  Am I missing something?

> ahh now that is clear.  oh ah are you sure about 4,3? should that be
> 4,3=0b11011111?

I did some searching, and it seems that this StackOverflow response supports my
understanding of how the mask is constructed:

https://stackoverflow.com/questions/30896622/understanding-powerpc-rlwinm-instruction

It looks like IBM uses inclusive bit numbering for the mask on both ends.  So,
if MB and ME are 3-bit fields (implying an 8-bit mask, as in the previous
example), then a mask of (0,7) == (8,7) == all bits set.  So, for a 32-bit wide
mask, the only way to produce all bits set is if ((MB AND 31) == ((ME+1) AND
31)).

> ok give it a rest, we can try mul and come back to this one.

I'll keep toying with it from time to time.  I despise defeat.

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