Mechanically checking a lemma used in an automatic verification tool

1. Jerry R. Burch and David L. Dill. Automatic verification of pipelined microprocessor control. In David L. Dill, editor, Conference on Computer-Aided Verification, volume 818 of Lecture Notes in Computer Science. Springer-Verlag, June 1994.

   Google Scholar 

2. Derek L. Beatty. A Methodology for Formal Hardware Verification, with Application to Microprocessors. PhD thesis, School of Computer Science, Carnegie Mellon University, August 1993.

   Google Scholar 

3. Jerry R. Burch. Techniques for verifying superscalar microprocessors. In Design Automation Conference, June 1996.

   Google Scholar 

4. Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier Scientific Publishers, 1987.

   Google Scholar 

5. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.

   Google Scholar 

6. A. J. Cohn. A proof of correctness of the Viper microprocessors: The first level. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 27–72. Kluwer, 1988.

   Google Scholar 

7. D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Conference on Theorem Provers in Circuit Design, September 1994.

   Google Scholar 

8. David Cyrluk. Inverting the abstraction mapping: A methodology for hardware verification. In Conference on Formal Methods in Computer-Aided Design, November 1996. (This volume).

   Google Scholar 

9. Michael J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwhistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer Academic Press, 1988.

   Google Scholar 

10. W. A. Hunt, Jr. FM8501: A verified microprocessor. Technical Report 47, University of Texas at Austin, Institute for Computing Science, December 1985.

    Google Scholar 

11. J. Joyce, G. Birtwistle, and M. Gordon. Proving a computer correct in higher order logic. Technical Report 100, Computer Lab., University of Cambridge, 1986.

    Google Scholar 

12. Robert B. Jones, David L. Dill, and Jerry R. Burch. Efficient validity checking for processor verification. In Intl. Conf. on Comp. Aided Design, 1995.

    Google Scholar 

13. Robert B. Jones, Carl-Johan H. Seger, and David L. Dill. Self-consistency checking. In Conference on Formal Methods in Computer-Aided Design, November 1996. (This volume).

    Google Scholar 

14. Jeffrey Kuskin et al. The Stanford FLASH multiprocessor. In Intl. Symp. on Comp. Arch., 1994.

    Google Scholar 

15. Mandayam Srivas and Mark Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52–64, September 1990.

    Google Scholar 

16. James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning. Using transformations and verification in circuit design. Technical Report 78, DEC Systems Research Center, September 1991.

    Google Scholar 

17. Mandayam Srivas and Steven P. Miller. Applying formal verification to a commercial microprocessor. In IFIP Conference on Hardware Description Languages (CHDL 95), Tokyo, Japan, August 1995.

    Google Scholar 

18. M. Srivas and S. P. Miller. Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Methods in System Design, 8(2): 153–88, March 1996.

    Google Scholar 

19. Phillip J. Windley and Michael Coe. The formal verification of instruction pipelines. In Ramayya Kumar and Thomas Kropf, editors, Conference on Theorem Provers in Circuit Design, Lecture Notes in Computer Science. Springer-Verlag, September 1994.

    Google Scholar 

20. Phillip J. Windley. A theory of generic interpreters. In George J. Milne and Laurence Pierre, editors, Correct Hardware Design and Verification Methods, volume 683 of Lecture Notes in Computer Science, pages 122–134. Springer-Verlag, June 1993.

    Google Scholar 

21. Phillip J. Windley. Formal modeling and verification of microprocessors. IEEE Transactions on Computers, 44(1), January 1995.

    Google Scholar 

22. Phillip J. Windley. Verifying pipelined microprocessors. In IFIP Conference on Hardware Description Languages (CHDL 95), Tokyo, Japan, August 1995.

    Google Scholar 

Download references