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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #1 from Cesar Strauss <cestrauss at gmail.com> ---
The work done on the formal proof of MultiCompUnit is here:
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/experiment/formal/proof_compalu_multi.py;h=2bab836ab8f2eda3778383ed0811303972250e3e;hb=099825f7d53fb64adb30e363fd359eda3d1f14cd

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
(https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/latch.py;h=e2d7541d396fa7468668f4bd903346abd504a94f;hb=8aa377705c96f365606950c0fa142e40546e566b#l69).
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.