A hybrid verification approach: getting deep into the design

ABSTRACT

One method of handling the computational complexity of the verification process is to combine the strengths of different approaches. We propose a hybrid verification technology combining symbolic trajectory evaluation with either symbolic model checking or SAT-based model checking. This reduces significantly the cost (both human and computing) of verifying circuits with complex initialisation, as well as simplifying proof development by enhancing verification productivity. The approach has been tested on current Intel designs.

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: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 3: Roderick Bloem , Kavita Ravi , Fabio Somenzi, Symbolic guided search for CTL model checking, Proceedings of the 37th conference on Design automation, p.29-34, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337306]
• 4: E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.427-432, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217565]
• 5: Fady Copty , Limor Fix , Ranan Fraer , Enrico Giunchiglia , Gila Kamhi , Armando Tacchella , Moshe Y. Vardi, Benefits of Bounded Model Checking at an Industrial Setting, Proceedings of the 13th International Conference on Computer Aided Verification, p.436-453, July 18-22, 2001
• 6: Fady Copty , Amitai Irron , Osnat Weissberg , Nathan P. Kropp , Gila Kamhi, Efficient Debugging in a Formal Verification Environment, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.275-292, September 04-07, 2001
• 7: Scott Hazelhurst , Carl-Johan H. Seger, Symbolic Trajectory Evaluation, Formal Hardware Verification - Methods and Systems in Comparison, p.3-78, January 1997
• 8: S. Hazelhurst. On Parametric and Characteristic Representations of State Spaces. Technical Report 2002-1, School of Computer Science, University of the Witwatersrand, March 2002. Available as ftp://ftp.cs.wits.ac.za/pub/research/reports/TR-Wits-CS-2002-1.ps.gz.
• 9: 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
• 10: P. Jain and G. Gopalakrishnan. Efficient symbolic simulation-based verification using the parametric form of boolean expressions. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 13(8):1005--1015, August 1994.
• 11: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 12: C. Pixley , S.-W. Jeong , G. D. Hachtel, Exact calculation of synchronization sequences based on binary decision diagrams, Proceedings of the 29th ACM/IEEE conference on Design automation, p.620-623, June 08-12, 1992, Anaheim, California, United States
• 13: Dong Wang , Pei-Hsin Jiang , James Kukula , Yunshan Zhu , Tony Ma , Robert Damiano, Formal property verification by abstraction refinement with formal, simulation and hybrid engines, Proceedings of the 38th conference on Design automation, p.35-40, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378260]
• 14: J. Yang and C.-J.H. Seger. Introduction to generalized symbolic trajectory evaluation. In Proc. of ICCD, September 2001.
• 15: Jun Yuan , Jian Shen , Jacob A. Abraham , Adnan Aziz, On Combining Formal and Informal Verification, Proceedings of the 9th International Conference on Computer Aided Verification, p.376-387, June 22-25, 1997

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Theory, Verification

Keywords:
hybrid verification, symbolic model checking, symbolic trajectory evaluation