[Libre-soc-bugs] [Bug 879] Formal proof of soc.experiment.compalu_multi.MultiCompUnit needed

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Wed Oct 12 19:57:14 BST 2022


--- Comment #1 from Cesar Strauss <cestrauss at gmail.com> ---
The work done on the formal proof of MultiCompUnit is here:

It did caught issues and subtle bugs, unseen so far, which managed to keep
hidden from our current unit tests.

The most serious bug is improper assertion of rel_o, for a masked operand, when
the previous instruction had zero_a or imm_ok. This is due to the src_l latch
currently not being reset, on issue.

This particular sequence was not present on the unit tests. In fact, there were
already tests, which tested each of zero_a, imm_ok, and masked operands. They
were just not adjacent to each other... Sure enough, I moved the tests to be
next to each other, and it did reproduce the bug!

I guess the unexpected operand read (which was thrown away) did not affect
results, so far.

Another bug found is the req_l latch not being clear on system reset. Even if
the holding register of SRLatch is really reset-less, it is still reset at
startup, because the latch reset port has reset=1
But, this only works if the latch reset port is driven by the sync domain. In
case of req_l, it's driven by the comb domain, so the latch is not reset on
system reset.

A minor issue is, on handshakes, to assume the other end only sends pulses when
requested/allowed. For instance, MultiCompUnit is not resilient to:
1) Receiving a new issue pulse when busy is already high
2) Receiving a go signal when rel is low

If desired, just replace the use of pulses with the appropriate AND of the
handshake signals.

All in all, I consider the formal verification work a success in catching
subtle bugs in MultiCompUnit.

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

More information about the libre-soc-bugs mailing list