[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 #40 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #38)
> I split up the formal proof into a per-instruction proof, allowing the
> proofs to be run in parallel, greatly speeding up the tests (if run with
> `pytest -n auto` or similar).

nice.

> The code is mid-rewrite and very WIP, but it at least implements everything
> that was there before (except checking Data.ok, which I forgot). The new
> code also implements CA[32]. All non-rotate tests pass.

briilliant.  this one kicked all our asses, there's some combinations
of the inputs to the Rotate module which are possible to set (imagine
a wire that is floating, and can randomly set 1 or 0) that *never*
get set by the main_stage.py pipeline... but Formal Correctness Engines
don't know that, and, in the absence of any Asserts/Assumes, will
detect and advise you of every single corner-case and permutation
that is "floating":

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/shift_rot/rotator.py;h=7c3d811c8fa0402a70d5a3e1551e8ecb83873280;hb=20ffa8ec223be44fc37df5184ca09d648e85a844#l49

basically there are combinations of those inputs that are never under any
legitimate circumstances in the Power ISA going to be set, and they need 
locking down.

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