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

> I did check this file, but I don't see where the mask is inverted.  The
> closest thing I can find to an inversion is this:
> 
>             with m.Case(0b00):
>                 comb += self.result_o.eq((rot & (mr & ml)) | (ra & ~(mr &
> ml)))
>             with m.Case(0b01):
>                 comb += self.result_o.eq((rot & (mr | ml)) | (ra & ~(mr |
> ml)))

yes that's it.  and using boolean remapping one of those could be done as,
let's pick the 1st one

(rot & ~(mr | ml)) | (ra & ~(mr & ml)))

see how they're the bit-opposite?

> where bits from the un-rotated RA value are mixed into the final output via
> the negated mask.  I'm already doing that in the proof.  Inverting mask bits
> when MB > ME also contradicts the definition of the MASK() operation,
> documented on page 6 of Book I.

it's confusing as hell because all four possible combinations of and or not of
ml and mr are involved in those 2 lines in rotator.py


> Based on my understanding of how rwlinm, et. al. seem to work (per the
> specs), MASK() takes a start and end position, in IBM bit position notation.
> Starting at bit x (start), the mask contains 1 bits.  It ends (optionally
> wrapping) at bit y (end).  All other bits are 0.  So, let's pretend I'm
> using an 8-bit mask; then,
> 
>   MASK(1,7) = 0b01111111
>   MASK(7,1) = 0b11000001
>   MASK(3,4) = 0b00011000
>   MASK(4,3) = 0b11111111

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


> I apologize for taking so long on this.  This is a real mind-bender for me. 

likewise :)

> I'm increasingly inclined to put this task aside and work on something else;
> it seems intractable for my skill level.  I'm frustrated that I've been
> going on a week, and nothing to really show for it.

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

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