Abstract
As digital designs grow evermore complex and design cycles become ever shorter, traditional informal methods of design verification are proving inadequate. Design teams are increasingly turning to formal techniques to address this “verification crunch”. The theorem prover, with its emphasis on establishing correctness, is arguably the dream design verification tool; however, theorem provers are rarely used in digital design. Much like automotive industry “concept cars”, theorem provers provide a compelling vision of the future, but in the real world of industrial design they have proven to be difficult to drive and expensive to maintain. We suggest ways that the theorem prover “concept cars” of today can be adapted to become the “off-road vehicles” necessary to negotiate the rough-and-tumble terrain of digital design in the 21st century.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
William R. Bevier, Warren A. Hunt Jr., J Strother Moore, and William D. Young.An approach to systems verification. Journal of Automated Reasoning, 5(4):411–428, December 1989.
Mark Bickford and Damir Jamsek. Formal specification and verification of VHDL. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design-FMCAD, volume 1166 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
Robert S. Boyer and J Strother Moore. Mechanized formal reasoning about programs and computing machines. In R. Veroff, editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. MIT Press, 1996.
Robert S. Boyer and Yuan Yu. Automated proofs of object code for a widely used microprocessor. Journal of the ACM, 43(1):166–192, January 1996.
Bishop Brock, Matt Kaufmann, and J Strother Moore. ACL2 theorems about commercial microprocessors. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design-FMCAD, volume 1166 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
Bishop C. Brock and Jr. Warren A. Hunt. The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor. Formal Methods in System Design, 11(1):71–104, July 1997.
David Greve, Matthew Wilding, and David Hardin. Efficient simulation using a simple formal processor model. Technical report, Rockwell Collins Advanced Technology Center, April 1998. (submitted for publication).
David A. Greve. Symbolic simulation of the JEM1 microprocessor. Technical report, Rockwell Collins, Inc., Cedar Rapids, IA, 1998. (submitted for publication).
David A. Greve and Matthew M. Wilding. Stack-based Java a back-to-future step. Electronic Engineering Times, page 92, January 12, 1998.
M. Kaufmann and J S. Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203–213, April 1997.
Steven P. Miller, David A. Greve, Matthew M. Wilding, and Mandayam Srivas. Formal verification of the AAMP-FV microcode. Technical report, Rockwell Collins, Inc., Cedar Rapids, IA, 1996.
Steven P. Miller and Mandayam Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT'95: Workshop on Industrial-Strength Formal specification Techniques, Boca Raton, FL, 1995. IEEE Computer Society.
J Strother Moore.Piton-A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.
S. Owre, N. Shankar, and J. M. Rushby. User Guide for the PVS Specification and Verification System (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.
David M. Russinoff. A mechanically checked proof of IEEE compliance of the floating point multiplication, division, and square root algorithms of the AMD-K7 processor. Available at www.onr.com/user/russ/david/, January 28 1998.
Matthew Wilding. A mechanically verified application for a mechanically verified environment. In Costas Courcoubetis, editor, Computer-Aided Verification-CAV '93, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
Matthew M. Wilding. Robust computer system proofs in PVS. In C. Michael Holloway and Kelly J. Hayhurst, editors, LFM97. Fourth NASA Langley Formal Methods Workshop. NASA Conference Publication, 1997. (http://atb-www.larc.nasa.gov/Lfm97/).
Alexander Wolfe. First Java-specific MPU rolls. Electronic Engineering Times, page 1, September 22, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hardin, D., Wilding, M., Greve, D. (1998). Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028729
Download citation
DOI: https://doi.org/10.1007/BFb0028729
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive