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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Tue May 26 11:01:25 BST 2020


--- 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.

More information about the libre-riscv-dev mailing list