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

> "/home/kc5tja/git/libre-soc/soc/src/soc/fu/shift_rot/formal/proof_main_stage.
> py", line 68, in elaborate
>     dut_sig = getattr(dut.o.ctx.op, name)

moo this should have been replaced, like when you found in trap formal proof
(or spr?) that muxid was not being checked.  i'd done ALU and a couple others.

> I tried changing all references of AluOp to SrOp, but I get the exact same
> errors.  I'm at a loss.  Can anyone provide guidance?  Thanks.

sorted, git pull, try again

commit 92d39595d144700306ce7ac5a37260cc918c93fc (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
Date:   Wed Jul 29 00:14:33 2020 +0100

    use ctx.op compare (and muxid) in shiftrot proof
    also use correct input record type and spec

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