Browse Prior Art Database

Linear Resolution Proofs of Combinatorial Equivalence of Logic Transformation

IP.com Disclosure Number: IPCOM000199456D
Publication Date: 2010-Sep-05
Document File: 7 page(s) / 93K

Publishing Venue

The IP.com Prior Art Database

Abstract

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.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 59% of the total text.

Page 1 of 7

Ȉ

Ȉ Ȉ

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 [1].

A more sophisticated approach is described in

                               [2]. 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

are equivalent.

A

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.

    [1] M. Mneimneh and K. Sakallah, "REVERSE: Efficient sequential verification for retiming", Proc. IWLS '03 , pp. 133-139.
[2] Satrajit Chatterjee,

Alan Mishchenko,

Robert K. Brayton,

Andreas Kuehlmann

: On

Resolution Proofs for Combinational Equivalence. DAC 2007: 600-605

Given a series of models M0,...Mn and a series of proofs P0,..Pn-1

we suggest

to create an intermediate model MI and two resolution proofs P

_M0=MI

, P

_MI=Mn

where P

_M0=MI

asserts the equivalence of M0 and MI and P

_MI=Mn

asserts the

equivalence of MI and Mn. We show a method in which the size of P

_M0=MI

is linear to

the size of the original proofs and P

_MI=Mn

                            is linear with
the size of M and the number of nets added and removed from M...