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

hmm i was expecting symbiyosys to be deterministic.

if it is, you needed to have tested exactly the same code otherwise it woukd be
different.

of course, the other way is to explicitly set the same input values in the
proof itself.

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

ok so here's what i did:

* examined the proof debug assert failure logs
* associated each failure with the signal it came from
* back-reverse-engineer the instruction that would create the required MB, ME,
abd OP_RLC
* create a unit test with those values
* get confidence that the unit tests succeeds (which tells us that the proof is
wrong)
* compare the gtkwave files and look fir discrepancies.

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

the problem with doing that is that the engine simply finds different inputs
that cause *that* to fail instead.

so ml and mr get different values.

> I'll add the MB > ME test and select & vs | based on its results.

remember that you also need, when doing &, to invert it.

check rotator.py closely, again.


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

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.

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