[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 17:29:34 BST 2020


--- Comment #38 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #37)
> (In reply to Cesar Strauss from comment #36)
> > How about a formal proof of the ALU interface?
> the interaction with it will be needed, yes, because of the signalling
> ready/valid.
> in particular the ALU may *not* necessarily be ready to proceed at the time
> operands are available.

Feel free to put this on my queue, if you wish (formal proof of the
CompUnit-ALU interface).

While I have no practical experience on formal proofs, I've been reading about
it for some time, with the goal of applying it to my own designs. I like to
think I've reached a good understanding.

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

More information about the libre-riscv-dev mailing list