Early formal verification of conditional coverage points to identify intrinsically hard-to-verify logic

ABSTRACT

Design verification of complex digital circuits typically starts only after the register-transfer level (RTL) description is complete. This frequently makes verification more difficult than necessary because logic that is intrinsically hard to verify, such as memories, counters and deep first-in, first-out (FIFO) structures, becomes immutable in the design. This paper proposes a new approach that exploits formal verification of conditional coverage points with the goal of early identification of hard-to-verify logic. We use the difficulty of formal verification problems as an early estimator of the verification complexity of a design. While traditional verification methods consider conditional coverage only in the design verification phase, we describe an approach that uses conditional coverage at a much earlier stage---the design phase, during which changes to the RTL code are still possible. The method is illustrated using real examples from the verification of an ASIC designed for a specialized supercomputer.

REFERENCES

• 1: Richard C. Ho , C. Han Yang , Mark A. Horowitz , David L. Dill, Architecture validation for processors, Proceedings of the 22nd annual international symposium on Computer architecture, p.404-413, June 22-24, 1995, S. Margherita Ligure, Italy
• 2: Cunningham, G. D., et al., Expression Coverability Analysis: Improving Code Coverage with Model Checking, In Proc. of Design & Verif. Conf., 2004.
• 3: David L. Dill, What's between simulation and formal verification? (extended abstract), Proceedings of the 35th annual conference on Design automation, p.328-329, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277138]
• 4: Indradeep Ghosh , Mukul R. Prasad, A Technique for Estimating the Difficulty of a Formal Verification Problem, Proceedings of the 7th International Symposium on Quality Electronic Design, p.63-70, March 27-29, 2006 [doi>10.1109/ISQED.2006.17]
• 5: Daniel Große , Ulrich Kühne , Rolf Drechsler, Estimating functional coverage in bounded model checking, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
• 6: Ly, T. A. et al., Method for Automatically Generating Checkers for Finding Functional Defects in a Description of a Circuit, U.S. Patent 6,175,946, 2001.
• 7: David E. Shaw , Martin M. Deneroff , Ron O. Dror , Jeffrey S. Kuskin , Richard H. Larson , John K. Salmon , Cliff Young , Brannon Batson , Kevin J. Bowers , Jack C. Chao , Michael P. Eastwood , Joseph Gagliardo , J. P. Grossman , C. Richard Ho , Douglas J. Ierardi , István Kolossváry , John L. Klepeis , Timothy Layman , Christine McLeavey , Mark A. Moraes , Rolf Mueller , Edward C. Priest , Yibing Shan , Jochen Spengler , Michael Theobald , Brian Towles , Stanley C. Wang, Anton, a special-purpose machine for molecular dynamics simulation, Proceedings of the 34th annual international symposium on Computer architecture, June 09-13, 2007, San Diego, California, USA

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids

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

General Terms:
Algorithms, Design, Verification

Keywords:
code coverage, conditional coverage, coverage hole, formal verification, inconclusive results, verifiability