Formal property verification by abstraction refinement with formal, simulation and hybrid engines

ABSTRACT

We present RFN, a formal property verification tool based on abstraction refinement. Abstraction refinement is a strategy for property verification. It iteratively refines an abstract model to better approximate the behavior of the original design in the hope that the abstract model alone will provide enough evidence to prove or disprove the property.However, previous work on abstraction refinement was only demonstrated on designs with up to 500 registers. We developed RFN to verify real-world designs that may contain thousands of registers. RFN differs from the previous work in several ways. First, instead of relying on a single engine, RFN employs multiple formal verification engines, including a BDD-ATPG hybrid engine and a conventional BDD-based fixpoint engine, for finding error traces or proving properties on the abstract model. Second, RFN uses a novel two-phase process involving 3-valued simulation and sequential ATPG to determine how to refine the abstract model. Third, RFN avoids the weakness of other abstraction-refinement algorithms --- finding error traces on the original design, by utilizing the error trace of the abstract model to guide sequential ATPG to find an error trace on the original design.We implemented and applied a prototype of RFN to verify various properties of real-world RTL designs containing approximately 5,000 registers, which represents an order of magnitude improvement over previous results. On these designs, we successfully proved a few properties and discovered a design violation.

REFERENCES

• 1: M. Abramovici, M.A. Breuer and A.D. Friedman. Digital Systems Testing and Testable Design. Piscataway, NJ: IEEE Press, 1990.
• 2: Felice Balarin , Alberto L. Sangiovanni-Vincentelli, An Iterative Approach to Language Containment, Proceedings of the 5th International Conference on Computer Aided Verification, p.29-40, June 28-July 01, 1993
• 3: Vamsi Boppana , Sreeranga P. Rajan , Koichiro Takayama , Masahiro Fujita, Model Checking Based on Sequential ATPG, Proceedings of the 11th International Conference on Computer Aided Verification, p.418-430, July 06-10, 1999
• 4: J. Burch, E. Clarke, K. McMillan, D. Dill and L. Hwang. Symbolic Model Checking: 10 20 States and Beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990.
• 5: H. Cho, G. Hatchel, E. Macii, M. Poncino, and F. Somenzi. Automatic state space decomposition for approximate FSM traversal based on circuit analysis. IEEE TCAD, 15(12), pp. 1451-1464, 1996.
• 6: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 7: Shankar G. Govindaraju , David L. Dill, Counterexample-guided choice of projections in approximate symbolic model checking, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 8: Pei Hsin Ho , Thomas Shiple , Kevin Harer , James Kukula , Robert Damiano , Valeria Bertacco , Jerry Taylor , Jiang Long, Smart simulation using collaborative formal and simulation engines, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
• 9: Chung-Yang Huang , Kwang-Ting Cheng, Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques, Proceedings of the 37th conference on Design automation, p.118-123, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337333]
• 10: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 11: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 12: Abelardo Pardo , Gary D. Hachtel, Incremental CTL model checking using BDD subsetting, Proceedings of the 35th annual conference on Design automation, p.457-462, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277171]
• 13: Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
• 14: F. Somenzi. CUDD: CU Decision Diagram Package. ftp://vlsi.colorado.edu/pub/.
• 15: Sun Microsystems. picoJava technology. http://www.sun.com/microelectronics/communitysource/pic ojava.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Advanced technologies

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  J. Computer Applications
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

General Terms:
Algorithms, Design, Experimentation, Measurement, Performance, Reliability, Theory, Verification