[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:15:16 BST 2020


--- Comment #37 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #36)
> (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.

it is also very "clean".

> How about a formal proof of the ALU interface?

the interaction with it will be needed, yes, because of the signalling

in particular the ALU may *not* necessarily be ready to proceed at the time
operands are available.

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

i have no idea.  we do need some way to check that data actually gets passed

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

More information about the libre-riscv-dev mailing list