[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 #18 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #17)
> remember that you also need, when doing &, to invert it.
> 
> check rotator.py closely, again.

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

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.

> MASK() which is the function back in the soec, very early on, is really
> unclear to me, unfortunately.  you might be able to make sense of it.

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

---

I apologize for taking so long on this.  This is a real mind-bender for me. 
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.

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