[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 #21 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #20)

> 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?

no, i get boolean logic wrong :)

> > 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)).

ahh this explains why right_mask (in rotator.py) is one different from
left_mask.

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