|
|
|---|
|
|
|
|---|
Tools for equivalence checking the evaluations of two sets of svex expressions under different environments.
Typically when we want to equivalence check the evaluation of some SVEX expressions against something else, e.g. a spec for some operation, we just bitblast both sides into an AIG and use FRAIGing along with other AIG transformations, followed by SAT to finish the proof.
The FRAIGing step is important because it speeds up the common case where the two sides are equivalent because they have a lot of equivalent subterms. To find candidate equivalent subterms, the transformation does a bunch of random simulation of the AIG and puts nodes which have identical simulation signatures into equivalence classes. Then it starts sweeping over the nodes with SAT to prove the equivalences. When it disproves an equivalence, this gives a counterexample which is again simulated on the AIG to further refine the equivalence classes.
A weakness of this algorithm is that sometimes many non-equivalent nodes seem to have the same behavior under simulation because their differences are improbable to be covered by random simulation. When there are lots of these nodes that aren't closely related in terms of their equivalence counterexamples, then we spend a lot of useless time on SAT checking. Or sometimes perhaps there are equivalent nodes within one side of the equivalence to be checked, but this equivalence doesn't help us prove that side equivalent to the other.
In the particular case where we are equivalence checking an evaluation of SVEX expressions against another evaluation of the same expressions, we can improve on this. We tweak our FRAIGing operation to begin with equivalence classes consisting only of the corresponding nodes between the two designs. This cuts down a lot on useless SAT checks; not all of the corresponding nodes are necessarily equivalent, but typically we expect the overall evaluations to be equivalent because of relatively simple equivalences near the inputs, not because of deep properties that SAT is ill-equipped to check.
We do this using FGL's
This requires some hand-tuning by the user. The user must provide the list
of AIGNET transforms, of type aignet::m-assumption-n-output-comb-transform. To use the special support for
limited FRAIGING, one or more of these transforms should be a FRAIG transform
with
(aignet::make-fraig-config ... :output-types `((:evals-equivalent-equiv-classes . ,(aignet::fraig-output-type-initial-equiv-classes))) ...)
Explanation: Our focused equivalence checking utilities add a set of outputs
to the AIG to be simplified, and these outputs specify which nodes should
initially be candidate equivalences. These outputs are tagged with the keyword
(aignet::make-fraig-config ... :output-types `((:fraig-remaining-equiv-classes . ,(aignet::fraig-output-type-initial-equiv-classes))) ...)