YAN Xiao-lang, ZHENG Fei-jun, GE Hai-tong, et al. Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking[J]. Acta Electronica Sinica, 2004, 32(8): 1233-1235.
YAN Xiao-lang, ZHENG Fei-jun, GE Hai-tong, et al. Combining Binary Decision Diagrams and Boolean Satisfiability for Equivalence Checking[J]. Acta Electronica Sinica, 2004, 32(8): 1233-1235.DOI：
A new combinational equivalence checking approach integrating Binary Decision Diagrams and Boolean Satisfiability is proposed.The algorithm works on the representation called And/Inverter Graph of the circuit.The BDD propogation and Circuit-based SAT Solver are applied in an intertwined manner to reduce the space of the miter circuit. If failed
CNF-based SAT Solver is used to solve the problem.The efficiency of the proposed approach is shown through its application on the LGsynth91 benchmark circuits.
京公网安备11010802024621