DocumentCode :
2640389
Title :
Boolean satisfiability and equivalence checking using general binary decision diagrams
Author :
Ashar, Pranav ; Ghosh, Abhijit ; Devadas, Srinivas
Author_Institution :
California Univ., Berkeley, CA, USA
fYear :
1991
fDate :
14-16 Oct 1991
Firstpage :
259
Lastpage :
264
Abstract :
It is shown how general binary decision diagrams (BDDs), i.e., BDDs where input variables are allowed to appear multiple times along any path in the BDD, can be used to check for Boolean satisfiability. This satisfiability checking strategy is based on an input smoothing operation on general BDDs. Various input smoothing strategies for general BDDs are developed. In order to verify the equivalence of two functions f1 and f2, f 1f2 is checked for satisfiability. Using general BDDs different implementations of a 16×16 multiplier, a modified Achilles´ heel function and a complex add-shift function were verified. It was not possible to construct OBDDs for any of the three functions
Keywords :
Boolean functions; logic design; multiplying circuits; Achilles´ heel function; Boolean satisfiability; add-shift function; equivalence checking; general binary decision diagrams; input smoothing operation; multiplier; Binary decision diagrams; Boolean functions; Circuit synthesis; Combinational circuits; Data structures; Input variables; Logic functions; Logic programming; Smoothing methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1991. ICCD '91. Proceedings, 1991 IEEE International Conference on
Conference_Location :
Cambridge, MA
Print_ISBN :
0-8186-2270-9
Type :
conf
DOI :
10.1109/ICCD.1991.139893
Filename :
139893
Link To Document :
بازگشت