[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 #38 from Jacob Lifshay <programmerjake at gmail.com> ---
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).

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.

https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=442546d5bffafb8571f50b1a4dc48e83ace1ce47

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