Linear Resolution Proofs of Combinatorial Equivalence of Logic Transformation
Publication Date: 2010-Sep-05
The IP.com Prior Art Database
A method for proving that logic optimization transformations are sound using standard resolution proofs is presented. A previous method suggests to use a series of extended resolutions in order to prove soundness of series of transformations, hence the equivalence of the original circuit and the final logically optimized one. Our method allows using regular resolution proofs instead of extended resolution proofs, hence helps facilitates the validation of the prove correctness.
There are scenarios in which one would like to keep a proof that a transformation / series of transformations ends up with logic that is
equivalent to the original logic. Such a scenario could appear both in the context of logic synthesis and in that of formal verification.
Logic optimization, clock re-timing and SAT sweeping are typical examples. Consider the case of Logic Optimization where a series of optimization steps are applied on a given model M0 yielding,
via a series of intermediate models, M1..Mn-1 an optimized model Mn. Event though the optimizer is assumed to be sound the
common practice is to verify the equivalence of M0 and Mn. Traditionally this is done via the use of a Combinatorial Equivalence Checker. (CEC).
It has been proposed in the past that the recording of the optimization steps can ease the verification process such as in .
A more sophisticated approach is described in
. The essence of this approach is as follows: since all optimization steps are sound
one could write proofs (P0,...Pn-1)
where Pi asserts that Mi and Mi+1
composition of P0,...Pn-1 yields a proof P
that the M0 and Mn are combinatoricly equivalent. Thus instead of running a CEC for the verification of an equivalence (
which is a hard NP complete problem)
, one could
assert the validity of the proof P. In order to achive this goals it was previousley suggested to use both the resolution and extended resolution inference rules.
While tools exists to verify resolution proofs  the usage of extended resolution is problematic. This is do to the fact that extended resolutions do not
lend themselves naturally neither to the stage in which the proof is written nor to the stage that it is verified. We end by mentioning that one could write a simple resolution proofs that asserts the equivalence of both models, yet this proof might be exponential
with relation to the size of the original proofs.
 M. Mneimneh and K. Sakallah, "REVERSE: Efficient sequential verification for retiming", Proc. IWLS '03 , pp. 133-139.
 Satrajit Chatterjee,
Robert K. Brayton,
Resolution Proofs for Combinational Equivalence. DAC 2007: 600-605
Given a series of models M0,...Mn and a series of proofs P0,..Pn-1
to create an intermediate model MI and two resolution proofs P
asserts the equivalence of M0 and MI and P
equivalence of MI and Mn. We show a method in which the size of P
is linear to
the size of the original proofs and P
is linear with
the size of M and the number of nets added and removed from M...