[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 #6 from Samuel A. Falvo II <kc5tja at arrl.net> ---
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.

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?

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