Combinational equivalence checking through function transformation

ABSTRACT

Circuits can be simplified for combinational equivalence checking by transforming internal functions, while preserving their ranges. In this paper, we investigate how to effiectively apply the idea to improve equivalence checking. We propose new heuristics to identify groups of nets in a cut, and elaborate detailed aspects of the new equivalence checking method. With a given miter, we identify a group of nets in a cut and transform the function of each net into a more compact representation with less variables. These new compact parametric representations preserve the range of nets as well as of the cut. This transformation significantly reduces the size of intermediate BDDs and enables the verification to be conclusive for many designs which state-of-the-art equivalence checkers fail to verify. Iterative groupings and transformations are performed until no grouping is possible for a cut. Then we proceed to the next cut and continue until the compare point is reached. Our experimental results show the effiectiveness of our strategy and new grouping heuristics on the new method.

REFERENCES

• 1: Mark D. Aagaard , Robert B. Jones , Carl-Johan H. Serger, Formal verification using parametric representations of Boolean constraints, Proceedings of the 36th ACM/IEEE conference on Design automation, p.402-407, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309968]
• 2: Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
• 3: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 4: Andrew E. Caldwell , Andrew B. Kahng , Igor L. Markov, Improved algorithms for hypergraph bipartitioning, Proceedings of the 2000 conference on Asia South Pacific design automation, p.661-666, January 2000, Yokohama, Japan [doi>10.1145/368434.368864]
• 5: E. Cerny and C. Mauras. Tautology checking using cross-controllability and cross-observability relations. In Proceedings of the International Conference on Computer-Aided Design, pages 34--37, Santa Clara, CA, Nov. 1990.
• 6: O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using Boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111--128, Leuven, Belgium, Nov. 1989.
• 7: E. Goldberg , M. Prasad , R. Brayton, Using SAT for combinational equivalence checking, Proceedings of the conference on Design, automation and test in Europe, p.114-121, March 2001, Munich, Germany
• 8: Andreas Kuehlmann , Florian Krohm, Equivalence checking using cuts and heaps, Proceedings of the 34th annual conference on Design automation, p.263-268, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266090]
• 9: James H. Kukula , Thomas R. Shiple, Building Circuits from Relations, Proceedings of the 12th International Conference on Computer Aided Verification, p.113-123, July 15-19, 2000
• 10: James H. Kukula , Thomas R. Shiple, Building Circuits from Relations, Proceedings of the 12th International Conference on Computer Aided Verification, p.113-123, July 15-19, 2000
• 11: João Marques-Silva , Thomas Glass, Combinational equivalence checking using satisfiability and recursive learning, Proceedings of the conference on Design, automation and test in Europe, p.33-es, January 1999, Munich, Germany [doi>10.1145/307418.307477]
• 12: In-Ho Moon , Gary D. Hachtel , Fabio Somenzi, Border-Block Triangular Form and Conjunction Schedule in Image Computation, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.73-90, November 01-03, 2000
• 13: In-Ho Moon , James H. Kukula , Kavita Ravi , Fabio Somenzi, To split or to conjoin: the question in image computation, Proceedings of the 37th conference on Design automation, p.23-28, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337305]
• 14: In-Ho Moon , Hee-Hwan Kwak , James H. Kukula , Thomas R. Shiple , Carl Pixley, Simplifying Circuits for Formal Verification Using Parametric Representation, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.52-69, November 06-08, 2002
• 15: John Moondanos , Carl-Johan H. Seger , Ziyad Hanna , Daher Kaiss, CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination, Proceedings of the 13th International Conference on Computer Aided Verification, p.131-143, July 18-22, 2001
• 16: Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation, Proceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors, p.459, September 17-20, 2000

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING

General Terms:
Algorithms, Experimentation, Verification

Keywords:
combinational verification, equivalence checking