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
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 1⊕f2 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;
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
DOI :
10.1109/ICCD.1991.139893