Advertisement

Correctness Properties of the Viper Block Model: The Second Level

  • Avra Cohn

Abstract

Viper [7,8,9,11,23] is a microprocessor designed by W. J. Cullyer, C. Pygott and J. Kershaw at the Royal Signals and Radar Establishment in Malvern, England (RSRE), and is now commercially available. Viper was intended for use in safety-critical applications such as civil aviation and nuclear power plant control. It is currently being evaluated (as part of the “VENOM” project [10]) for use as an input-output controller in the deployment of weapons from tactical aircraft. To satisfy requirements of safety-criticality, Viper has a particularly simple design about which it is relatively easy to reason using current techniques and models. The designers at RSRE, who deserve much credit for the promotion of formal methods, intended from the start that Viper be formally verified. The verification project has been carried out at the University of Cambridge. The University was and is not involved with any of the applications of Viper, civil or otherwise, and the whole verification project is and has been fully in the public domain. This report describes the partially completed correctness proof, in the HOL system, of the Viper ‘block model’ with respect to Viper’s top level functional specification. The (fully completed) correctness proof of the Viper ‘major state’ model has already been reported in [5]. This paper describes the analysis of the block model in some detail (in Sections 6 to 9), so is necessarily rather long. Section 2 is a discussion of the scope and limits of the word ‘verification’, and cautions against careless use of the term. The paper includes a very brief introduction to HOL (Section 4), but does not attempt a description or rationalization of Viper’s design.The possible uses of the paper are as follows:

• It includes enough detail to support an attempt to repeat the proof in HOL, or possibly in other theorem-proving systems;

• It serves as a guide for future analyses of Viper;

• It complements the existing Viper documentation;

• It covers some general issues in hardware verification;

• It illustrates some problems in managing large HOL proofs.

Keywords

Minor State Block Model Memory Source Major State Symbolic Execution 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    H. G. Barrow, VERIFY: A Program for Proving Correctness of Digital Hard¬ware Designs, Artificial Intelligence Vol. 24, 1984Google Scholar
  2. [2]
    A. Camilieri, M. Gordon and T. Melham, Hardware Verification using Higher- Order Logic, Proceedings of the IFIP WG 10.2 Working Conference: From H.D.L. Descriptions to Guaranteed Correct Circuit Designs, Grenoble, September 1986, ed. D. Borrione, North-Holland, Amsterdam, 1987Google Scholar
  3. [3]
    A. Church, A Formulation of the Simple Theory of Types, Journal of Symbolic Logic 5, 1940Google Scholar
  4. [4]
    A. Cohn and M. Gordon, A Mechanized Proof of Correctness of a Simple Counter, University of Cambridge, Computer Laboratory, Tech. Report No. 94, 1986Google Scholar
  5. [5]
    A. Cohn, A Proof of Correctness of the Viper Microprocessor: the First Level, VLSI Specification, Verification and Synthesis, eds. G. Birtwistle and P.A. Subrahmanyam, Kluwer, 1987; Also University of Cambridge, Computer Laboratory, Tech. Report No. 104Google Scholar
  6. [6]
    W. J. Cullyer and C. H. Pygott, Hardware Proofs using LCFXSM and ELLA, RSRE Memo. 3832, Sept. 1985Google Scholar
  7. [7]
    W. J. Cullyer, Viper Microprocessor: Formal Specification, RSRE Report 85013, Oct. 1985Google Scholar
  8. [8]
    W. J. Cullyer, Viper — Correspondence between the Specification and the “Major State Machine”, RSRE report No. 86004, Jan. 1986Google Scholar
  9. [9]
    W. J. Cullyer, Implementing Safety-Critical Systems: The Viper Microproces¬sor, VLSI Specification, Verification and Synthesis, eds. G. Birtwistle and P.A. Subrahmanyam, Kluwer, 1987Google Scholar
  10. [10]
    C. Gane (Computing Devices Company Ltd.), Computing Devices, Hastings’ VIPER-VENOM Project: VIPER in Weapons Stores Management, SafetyNet: Viper Microprocessors in High Integrity Systems, Enq. No. 021, Issue 2, July- August-September 1988, Viper Technologies Ltd., WorcesterGoogle Scholar
  11. [11]
    J. Cullyer et. al., forthcoming bookGoogle Scholar
  12. [12]
    M. Gordon, R. Milner and C. P. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science No. 78, Springer-Verlag, 1979Google Scholar
  13. [13]
    M. Gordon, Proving a Computer Correct, University of Cambridge, Computer Laboratory, Tech. Report , 1983Google Scholar
  14. [14]
    M. Gordon, HOL: A Machine Oriented Formulation of Higher-Order Logic, University of Cambridge, Computer Laboratory, Tech. Report No. 68, 1985Google Scholar
  15. [15]
    M. Gordon: A Proof Generating System for Higher-Order Logic, Univer¬sity of Cambridge, Computer Laboratory, Tech. Report No. 103, 1987; Revised version in VLSI Specification, Verification and Synthesis, eds. G. Birtwistle and P.A. Subrahmanyam, Kluwer, 1987Google Scholar
  16. [16]
    M. P. Halbert (Cambridge Consultants Ltd.), Selfchecking Computer Module Based on the ViperlA Microprocessor, SafetyNet: Viper Microprocessors in High Integrity Systems, Enq. No. 017, Issue 2, July-August-September 1988, Viper Technologies Ltd., WorcesterGoogle Scholar
  17. [17]
    W. A. Hunt Jr., FM8501: A Verified Microprocessor, University of Texas, Austin, Tech. Report 47, 1985Google Scholar
  18. [18]
    J.J. Joyce, Formal Verification and Implementation of a Microprocessor, VLSI Specification, Verification and Synthesis, eds. G. Birtwistle and P.A. Subrah¬manyam, Kluwer, 1987Google Scholar
  19. [19]
    J. J. Joyce, private communicationGoogle Scholar
  20. [20]
    J. Kershaw, Viper: A Microprocessor for Safety-Critical Applications, RSRE Memo. No. 3754, Dec. 1985Google Scholar
  21. [21]
    T. Melham, private communicationGoogle Scholar
  22. [22]
    L. Paulson, Interactive Theorem Proving with Cambridge LCF, Cambridge University Press, 1987Google Scholar
  23. [23]
    C. H. Pygott, Viper: The Electronic Block Model, RSRE Report. No. 86006, July 1986Google Scholar
  24. [24]
    Viper Microprocessor: Verifiable Integrated Processor for Enhanced Reliabil¬ity: Development Tools, Charter Technologies Ltd., Publication No. VDT1, Issue 1, Dec. 1987Google Scholar
  25. [25]
    Application for Admission and Registration Form, Second VIPER Symposium, RSRE, Malvern, 6-7 September, 1988Google Scholar

Copyright information

© Springer-Verlag New York Inc. 1989

Authors and Affiliations

  • Avra Cohn
    • 1
  1. 1.New Museums SiteUniversity of Cambridge Computer LaboratoryCambridgeEngland

Personalised recommendations