[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 #14 from Samuel A. Falvo II <kc5tja at arrl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #13)
> so the detection for when the mask beginning is at the opposite end i.e.
> (greater or less?) than the mask end, is missing.
> 
> basically from the spec:
> 
>     "A mask is generated having 1-bits from bit MB+32 through
>      bit ME+32 and 0-bits elsewhere."
> 
> this mask actually *rotates* and hence the inversion thing above.
> 
> notice that the OR of mr and ml produces 0xffffffff? (MASK_FOR_RLC)
> 
> that should be 0x0000f800 because they are supposed to be ANDed
> 
> ml = 0xffffff800
> mr = 0x00000ffff

It looks like your test case is different from mine, as this is exactly not
what I'm seeing.  I'm literally seeing ml = 0 and mr = -1.  Further, I'm seeing
that MB < ME, so ml should not be equal to 0.

> however because the mask is ORed together (which it should not be)

The statement reads ml | mr because that was the final test I'd performed
before checking everything in and giving up.  The test fails also with ml & mr,
which as I'd documented previously, equals 0x00000000.

I'll add the MB > ME test and select & vs | based on its results.  If this
makes a significant difference, then I'd be shocked, as the failing case would
not at all indicate this was the problem.  I *should* be seeing ml and mr being
disjoint masks if that were the case, but I'm not.

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