[circt-lec] Fixed equivalence check for multiple outputs

[fzi-hielscher]

Currently the solver of the equivalence check creates a separate not equal constraint for each output of the processed module(s). Consequently, the constraint system becomes unsatisfiable as soon as at least one of the outputs is equivalent, causing the equivalence check for the entire module to pass. This PR changes the constraints to make them unsatisfiable iff all outputs are equivalent, by solving for the disjunction of the not equal expressions.

This also adds a test case, checking that two non-equivalent circuits do not pass the comparison. This turned out to be more complicated than I was expecting. When checking the output of circt-opt for c1 != c2 the test will still fail, because it produces a non-zero exit code for non-equivalent circuits. The best thing I could come up with was checking for equivalence and marking the test as expected to fail.

[TaoBi22]

This is great, thanks a lot for catching that bug! I'll defer to someone else on whether the failing test is appropriate - it might be worth getting verify-diagnostics working on circt-lec, which may offer a slightly nicer way to handle tests checking for equivalence check failure, but in my opinion that's not really within the scope of this PR (I'm happy to do it in a separate PR so this can be rebased on top, as I'm about to do it in #4647 which is architecturally very similar to circt-lec).

[fzi-hielscher]

Thank you for checking.
The XFAIL certainly is not a great solution. I was thinking about adding a command line flag that just 'flips' the return code, but didn't want to clutter this PR. I have never used verify-diagnostics so I cannot really comment on that.

[TaoBi22]

I was thinking about adding a command line flag that just 'flips' the return code, but didn't want to clutter this PR.

This is an interesting idea - my main concern here (and with the current approach) would be that if circt-lec throws an error for a different reason, this won't be flagged by failing tests. With verify-diagnostics, we can ensure that the error being thrown is the expected one, so I think that would probably be the best way to handle this - I can try and get a PR up soon to add support!

[dtzSiFive]

The "not" utility can be used for expected error exit codes, like "not circt-opt ....", if that helps? Haven't looked at what's going on in this PR (verify-diagnostics interaction might not be quite what we want? Can look tomorrow if unsure) but anyway just FYI that's useful tool for this sort of thing.

[TaoBi22]

The "not" utility can be used for expected error exit codes, like "not circt-opt ....", if that helps? Haven't looked at what's going on in this PR (verify-diagnostics interaction might not be quite what we want? Can look tomorrow if unsure) but anyway just FYI that's useful tool for this sort of thing.

Thanks! My thinking re: verify-diagnostics is that we want to be able to distinguish between a non-zero return code as a result of non-equivalence (which doesn't currently emit an error, but obviously an easy change), and as a result of some other error being emitted if a breaking change is made (although there might be a nicer way to handle this I'm not aware of?). However, just using not seems like a good fix for now, can always adjust later!

[fzi-hielscher]

Thanks. The not is just what I've been looking for but could not find in the docs. I think a flag indicating that we are actually checking for non-equivalence may still have its use for scripting purposes. Something along the lines of grep -v. But this should do the trick for now.

[darthscsi]

LGTM.