Verification through the principle of least astonishment

ABSTRACT

Assessing the correctness of a digital design is a challenging task hampered by extremely large circuit netlists, counterintuitive property descriptions and ill-defined specifications. In this paper we propose a new verification methodology, inspired by the principle of least astonishment. The underlying idea is to provide an automatic assessment of what constitutes "common behavior" for a system, and use this to detect any anomaly in the design. Deviant behavior is presented to the verification engineer through intuitive, compact diagrams which lend themselves to quick inspection for correctness. To enable this methodology we introduce Inferno, a new tool which can analyze the results of a logic simulation trace and automatically extract high-level diagrams representing the design's transaction activity across any user-defined interface. In addition, Inferno can automatically generate a checker module corresponding to a given transaction, suitable for use in a wide range of verification methodologies. We envision the deployment of Inferno in a closed-loop constraint-random simulation methodology where any new transaction detected on the interface is presented to the user for analysis and, once deemed legal, it is merged into an "approved transactions" checker, which flags the detection of any new type of transactions. We provide a series of examples and experimental results to show the effectiveness of Inferno and some of its possible uses.

REFERENCES

• 1: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 2: Thomas Arts , Lars-Åke Fredlund, Trace analysis of Erlang programs, ACM SIGPLAN Notices, v.37 n.12, December 2002 [doi>10.1145/636517.636524]
• 3: Saddek Bensalem , Yassine Lakhnech , Hassen Saïdi, Powerful Techniques for the Automatic Generation of Invariants, Proceedings of the 8th International Conference on Computer Aided Verification, p.323-335, August 03, 1996
• 4: B. Bentley and R. Gray. Validating the Intel Pentium 4 Microprocessor. Intel Technology Journal, pages 1--8, 2001.
• 5: D. S. Brahme, S. Cox, J. Gallo, W. Grundmann, C. N. Ip, W. Paulsen, J. L. Pierce, J. Rose, D. Shea, and K. Whiting. The transaction-based verification methodology. Technical report, Cadence Design Systems, Inc., Aug. 2000. Technical Report No. CDNL-TR-2000-0825.
• 6: E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P. R. Stephan, R. K. Brayton and A. Sangiovanni-Vincentelli. SIS: A system for sequential circuit synthesis. Technical report, 1992.
• 7: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 8: M. D. Ernst. Verification for legacy programs. In Verified Tools: Theories, Tools, Experiments, Zürich, Switzerland, October 10--13, 2005.
• 9: Görschwin Fey , Rolf Drechsler, Improving simulation-based verification by means of formal methods, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, January 27-30, 2004, Yokohama, Japan
• 10: Sudheendra Hangal , Naveen Chandra , Sridhar Narayanan , Sandeep Chakravorty, IODINE: a tool to automatically infer dynamic invariants for hardware designs, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065786]
• 11: http://www.opencores.org.
• 12: Tom Schubert, High level formal verification of next-generation microprocessors, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775834]
• 13: Jinlin Yang , David Evans, Automatically Inferring Temporal Properties for Program Evolution, Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE'04), p.340-351, November 02-05, 2004 [doi>10.1109/ISSRE.2004.11]

INDEX TERMS

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

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification; Simulation
  B.8 Performance and Reliability
      B.8.1 Reliability, Testing, and Fault-Tolerance
      B.8.2 Performance Analysis and Design Aids

General Terms:
Design, Performance, Verification