[libre-riscv-dev] [Bug 336] ALU CompUnit needs to recognise that RA (src1) can be zero

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=336

--- Comment #36 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #35)
> it will be fascinating to compare against the formal proof

I saw src/soc/fu/compunits/formal/proof_fu.py. Very interesting.

How about a formal proof of the ALU interface?

Also, maybe DummyALU could be truly dummy (doesn't drive its signals), and let
Assume drive them, in the CompUnit formal proof.

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