[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 #2 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
samuel the code is fine as there are a number of unit tests that already pass. 
we just need the mask/clear proofs added.  i had made a start on it already
however the different options was doing my head in.

here we definitely, definitely need to stick with the field decoders.  there
are odd things in the pseudocode that swap the MSB to the LSB.

example:

    b <- mb[5] || mb[0:4]

however please especially note: the 3.0B spec pseudocode is **WRONG** for the
field named "sh".  it is the shift amount AS-IS, it must NOT be Cat(sh[5],
sh[0:5]) or somesuch.

i have raised this as a bugreport on openpowerhdl-cores.

https://libre-soc.org/openpower/isa/fixedshift/

so, again: shl, extswsli, these are all done.  it is just the "mask" versions
rl* that need doing.

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