[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 #7 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Samuel A. Falvo II from comment #6)
> Committed some WIP code; I cannot get closure on the instructions:
> 
> rlwinm(.)
> rlwnm(.)
> rlwimi(.)
> 
> On my system, there appears to be a bug with mask generation.  Yosys
> generates an RLC-type instruction with MB=0x10 and ME=0x14, which should
> generate a mask of 0x0000F000.  However, the final mask that does get
> generated is 0x00000000 (since ml=0x00000000 while mr=0xFFFFFFFF.  I would
> *expect* that ml=0x0000FFFF and mr=0xFFFFF000, so that their bitwise-AND
> would give the desired mask.

ok suggestion there is to write some short program that actually prints out the
values.

i got horribly confused by one of the masks being subtracted from 63/64 and not
the other.


> But, when I calculate by hand how the masks are generated, the results are,
> indeed, exactly what I'd expect them to be.
> 
> I can't explain the discrepancy.
> 
> BTW, any reason why the mb and me signals are 7-bits wide in
> proof_main_stage.py?  Since GPRs are only 64-bits wide, wouldn't 6-bits be
> sufficient?

i believe this is because they are calculated as 64 bit and can be signed?  the
top bit allow expression of -64 which requires 7 bits not 6.

honestly though i am just guessing, there.

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