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

> This begs the question, when invoking an OP_SHL type instruction, where
> mb=me=0, should it be operating in mode 0?  Should the masks be generated
> differently for these types of instructions?  Etc.

ok looking at p109 v3.0B spec, "sld" and "srd", the pseudocode has,
for sld, a MASK(0, 63-n) where n=RB.

and for slw (p107) it is MASK(32, 63-n)


so there is only one mask (mb?), the other one should be "Assume(me? == 0)".
or something.  maybe 0xffffffffffffffff, i don't know.

for OP_SHR it will be the other mask.

looking at the Rotator class, "input mode=0b0000" means:

* right_rhift=0,
* arith=0
* clear_left=0
* clear_right=0

this results in "output mode" (line 160) == 0b00 which yes, gives
us rot & (mr & ml)

wherrrrre.... how do we get me and mb both equal to zero?

oh hang on, look at the pseudocode again.

r = ROTL64((RS), n)
if (RB)57 = 0 then
     m = MASK(0, 63-n)

that means: if RB is between 64 and 127, the output is zero, simple as that.

i'll add a unit test for that, see how it goes.

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