Towards Light-Weight Verification and Heavy-Weight Testing
Traditional, simulation-based validation methods have not kept up with the scale or pace of modern digital design, and, therefore, form a major impediment in the drive for evermore complex designs (Hardin et al.,1998). This is mainly due to the sheer number of possible test cases which makes it nearly impossible to perform exhaustive testing. Thus testing only demonstrates the existence but not the absence of flaws. Even worse, it is unlikely that testing alone would have caught errors like the famous bug in the lookup table of the Intel Pentium floating-point division unit, since it only occurred on table inputs that were thought to be beyond the region of interest (Pratt, 1995).
KeywordsTheorem Prove Formal Verification Symbolic Evaluation Abstract State Machine Common Lisp
Unable to display preview. Download preview PDF.
- E. Börger and S. Mazzanti (1996): A Correctness Proof for Pipelining in RISC Architectures. Technical Report DIMACS 96–22, Dipartimento di Informatica, University of Pisa, Corso Italia 40, 56125 Pisa, Italy.Google Scholar
- R.S. Boyer and J S. Moore (1996): Mechanized Formal Reasoning about Programs and Computing Machines. In Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. MIT Press.Google Scholar
- G. Dowek, A. Felty, H. Herbelin, G. Huet, Ch. Murthy, C. Parent, Chr. PaulinMohring, and B. Werner (1993): The Coq Proof Assistant User’s Guide (Version 5.8). INRIA-Rocquencourt - CNRS - ENS Lyon. Projet Formel.Google Scholar
- Y. Gurevich (1995): Evolving algebras 1993: Lipari guide. In E. Börger, editor, Current Trends in Theoretical Computer Science, pages 9–36. Computer Science Press.Google Scholar
- D. Hardin, M. Wilding, and D. Greve (1998): Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle. In CAV’98: Computer-Aided Verification, Lecture Notes in Computer Science. Springer Verlag.Google Scholar
- J S. Moore (1998): Symbolic Simulation: an ACL2 Approach. In Formal Methods in Computer-Aided Design (FMCAD ‘88), Lecture Notes in Computer Science. Springer Verlag. Accepted for publication.Google Scholar
- H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rueß (1996): Mechanized Semantics of Simple Imperative Programming Constructs. Ulmer Informatik-Berichte 96–11, Universität Ulm, Fakultät für Informatik.Google Scholar
- N. Shankar (1998): Personal communication.Google Scholar
- M.K. Srivas and S.P. Miller (1995): Formal Verification of the AAMP5 Microprocessor. In M.G. Hinchey and J.P. Bowen, editors, Applications of Formal Methods, International Series in Computer Science, chapter 7, pages 125–180. Prentice Hall, Hemel Hempstead, UK.Google Scholar
- M. Srivas, H. Rueß, and D. Cyrluk (1997) Hardware Verification using PVS. In Th. Kropf, editor, Formal Hardware Verification Methods and Systems in Comparison, volume 1287 of Lecture Notes in Computer Science, chapter 4, pages 156–205. Springer Verlag.Google Scholar
- F.W. von Henke, M. Luther, H. Pfeifer, H. Rueß, D. Schwier, M. Strecker, and M. Wagner (1996): The TYPELAB specification and verification environment. In M. Nivat M. Wirsing, editor, Proceedings AMAST’96, pages 604–607. Springer LNCS 1101.Google Scholar
- Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, and Harald Rueß (1998): Case Studies in Meta-Level Theorem Proving. In Jim Grundy and Malcolm Newey, editors, Proc. Intl. Conf. on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science. Springer-Verlag.Google Scholar