Abstract
We present a deductive verification framework that combines deductive reasoning, general purpose decision procedures, and domain- specific reasoning. We address the integration of formal as well as informal domain-specific reasoning, which is encapsulated in the form of user-defined inference rules. To demonstrate our approach, we describe the verification of a SRT divider where a transistor-level implementation with timing is shown to be a refinement of its high-level specification.
This work was supported in part by NSERC research grant OGP-0138501, a NSERC graduate fellowship and a UBC graduate fellowship.
Chapter PDF
Similar content being viewed by others
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
Mark Aagaard and Carl-Johan H. Seger. The formal verification of a pipelined double-precision IEEE floating-point multiplier. In Int. Conf. on Computer-Aided Design, ICCAD’ 95, pages 7–10, November 1995.
Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253–284, May 1991.
Martín Abadi and Leslie Lamport. An old-fashioned recipe for real time. In J. W. de Bakker et al., editors, Proceedings of the REX Workshop, “Real-Time: Theory in Practice”. Springer, 1992. LNCS 600.
Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In 3rd Int. Symp. on Prog. Lang. Implement. and Logic Program., number 528 in Lect. Notes Comput. Sci., pages 1–13. Springer-Verlag, August 1991.
N. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H. B. Sipma, and T. E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In 8th Int. Conf. Computer-Aided Verification, CAV’ 96, number 1102 in Lect. Notes Comput. Sci., pages 415–418. Springer-Verlag, August 1996.
Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In 1st Int. Conf. on Theorem Provers in Circuit Design, TPCD’ 92, pages 129–156. North Holland, 1992.
Joseph J. F. Cavanagh. Digital computer arithmetic: design and implementation. McGraw-Hill, New York, 1984.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
Michael Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 153–177. Elsevier Science Publishers, 1985.
Michael J. C. Gordon. HOL: a proof generating system for higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 74–128. Kluwer Academic Publishers, 1988.
Cheryl Harkness and Elizabeth Wolf. Verifying the Summit bus converter protocols with symbolic model checking. Formal Meth. System Design, 4:83–97, 1994.
Scott Hazelhurst and Carl-Johan H. Seger. A simple theorem prover based on symbolic trajectory evaluation and BDDs. IEEE Trans. Comput. Aided Des. Integr. Circuits, 14(4):413–422, April 1995.
Leslie Lamport. win and sin: Predicate transformers for concurrency. ACM Trans. Program. Lang. Syst., 12(3):396–428, July 1990.
Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst., 1(2):245–257, October 1979.
Tarik Ono-Tesfaye, Christoph Kern, and Mark R. Greenstreet. Verifying a self-timed divider. In Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems. IEEE Computer Society Press, April 1998.
S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th Int. Conf. Automated Deduction (CADE’ 92), number 607 in Lect. Notes Comput. Sci., pages 748–752. Springer-Verlag, 1992.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lect. Notes Comput. Sci. Springer-Verlag, Berlin, 1994.
Amir Pnueli and Elad Shahar. A platform for combining deductive with algorithmic verificication. In 8th Int. Conf. Computer-Aided Verification, CAV’ 96, number 1102 in Lect. Notes Comput. Sci., pages 184–195. Springer-Verlag, August 1996.
F. Pong, A. Nowatzyk, G. Aybay, and M. Dubois. Verifying distributed directory-based cache coherence protocols: S3.mp, a case study. In Proc. EURO-Par’ 95 Parallel Processing, number 966 in Lect. Notes Comput. Sci., pages 287–300. Springer-Verlag, August 1995.
S. Rajan, N. Shankar, and M. K. Srivas. An integration of model-checking with automated proof checking. In 7th Int. Conf. Computer-Aided Verification, CAV’ 95, number 939 in Lect. Notes Comput. Sci., pages 84–97. Springer-Verlag, July 1995.
Charles L. Seitz. System timing. In Carver Mead and Lynn Conway, editors, Introduction to VLSI Systems, pages 218–262. Addison-Wesley, 1980.
Robert E. Shostak. Deciding combinations of theories. J. ACM, 31(1):1–12, January 1984.
Fabio Somenzi. CUDD: CU Decision Diagram Package. URL: http://bessie.colorado.edu/~fabio/CUDD/cuddIntro.html.
Mandayam K. Srivas and Steven P. Miller. Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Meth. System Design, 8(2):153–188, March 1996.
Jørgen Staunstrup. A formal approach to hardware design. Kluwer Academic Publishers, Boston, 1994.
Tom Verhoeff. Delay-insensitive codes-an overview. Distributed Computing, 3:1–8, 1988.
T. E. Williams, M. A. Horowitz, R. L. Alverson, and T. S. Yang. A self-timed chip for division. In Stanford Conference on Advanced Research in VLSI, pages 75–96, March 1987.
Ted E. Williams. Self-timed rings and their application to division. Technical Report CSL-TR-91-482, Computer Systems Lab, Dept. of EE, Stanford, May 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kern, C., Ono-Tesfaye, T., Greenstreet, M.R. (1999). A Light-Weight Framework for Hardware Verification. In: Cleaveland, W.R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1999. Lecture Notes in Computer Science, vol 1579. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49059-0_23
Download citation
DOI: https://doi.org/10.1007/3-540-49059-0_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65703-3
Online ISBN: 978-3-540-49059-3
eBook Packages: Springer Book Archive