TY - JOUR
T1 - Permutation and phase independent Boolean comparison
AU - Mohnke, Janett
AU - Malik, Sharad
N1 - Funding Information:
This work was done while Janett Mohnke was visitingP rincetonU niversity under a grant from IREX. Sharad Malik is supportedb y an NSF Research InitiationA wardand an IBM FacultyD evelopmenAtw ard.
PY - 1993/12
Y1 - 1993/12
N2 - This paper addresses the problem of checking the equivalence of two Boolean functions under arbitrary input permutations and/or input phase assignments. This problem has several applications in the synthesis and verification of combinational logic. It arises in the technology mapping stage of logic synthesis in finding a match from the cell library for parts of the technology independent circuit. In logic verification this is needed when the exact correspondence of inputs between the two circuits is not known. Exact solutions using exhaustive enumeration of the permutations and/or phase assignments are never a practical possibility, thus recourse is taken to heuristics that work well in practice. The approach presented in this paper computes a signature for each variable or phase of a variable that will help to establish correspondence of variables or phases of variables. The strength of the proposed approach depends on the ability to quickly derive a signature with minimum aliasing. Aliasing refers to two different variables or phases having the same signature, thus rendering this signature useless for the purpose of distinguishing between them. Experimental results on a large number of examples establish the efficacy of this approach.
AB - This paper addresses the problem of checking the equivalence of two Boolean functions under arbitrary input permutations and/or input phase assignments. This problem has several applications in the synthesis and verification of combinational logic. It arises in the technology mapping stage of logic synthesis in finding a match from the cell library for parts of the technology independent circuit. In logic verification this is needed when the exact correspondence of inputs between the two circuits is not known. Exact solutions using exhaustive enumeration of the permutations and/or phase assignments are never a practical possibility, thus recourse is taken to heuristics that work well in practice. The approach presented in this paper computes a signature for each variable or phase of a variable that will help to establish correspondence of variables or phases of variables. The strength of the proposed approach depends on the ability to quickly derive a signature with minimum aliasing. Aliasing refers to two different variables or phases having the same signature, thus rendering this signature useless for the purpose of distinguishing between them. Experimental results on a large number of examples establish the efficacy of this approach.
KW - High level design tools
KW - synthesis and verification
KW - synthesis of field-programmable gate arrays
UR - http://www.scopus.com/inward/record.url?scp=0027873364&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0027873364&partnerID=8YFLogxK
U2 - 10.1016/0167-9260(93)90041-A
DO - 10.1016/0167-9260(93)90041-A
M3 - Article
AN - SCOPUS:0027873364
SN - 0167-9260
VL - 16
SP - 109
EP - 129
JO - Integration, the VLSI Journal
JF - Integration, the VLSI Journal
IS - 2
ER -