Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 31 Mar 1995 23:08:16 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA247495920; Fri, 31 Mar 1995 14:38:40 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from bobcat.cs.byu.edu by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA247455918; Fri, 31 Mar 1995 14:38:38 -0700 Received: from cs.byu.edu (localhost) by bobcat.cs.byu.edu (1.37.109.15/CS-Client) id AA074556008; Fri, 31 Mar 1995 14:40:08 -0700 Message-Id: <199503312140.AA074556008@bobcat.cs.byu.edu> To: info-hol@cs.byu.edu Subject: "new_theory `HOL`" book is available in HTML Date: Fri, 31 Mar 1995 14:40:08 -0700 From: Phil Windley The book, "new_theory `HOL`", by Graham Birtwistle, Shiu-Kai Chin, and Brian Graham is now available in HTML format. The book is available from the HOL documentation page http://lal.cs.byu.edu/lal/hol-documentation.html or directly from http://lal.cs.byu.edu/lal/holdoc/birtwhistle/all/all.html The book is over 600 pages in Postscript (also available). Thanks to Graham, Shiu-Kai, and Brian for making it available and to Rosina Bignall and Scott McCosh (in my lab) for translating it from LaTeX to HTML. Even with the help of a LaTeX to HTML translator, the task was formidable. I've attached a table of contents below for those who are interested. --phil-- __________________________________________________________________________ Phillip J. Windley, Asst. Professor | windley@cs.byu.edu Laboratory for Applied Logic | Dept. of Computer Science, TMCB 3370 | Brigham Young University | Phone: 801.378.3722 Provo UT 84602-6576 | Fax: 801.378.7775 ------------------------------------------------------------------------ If you use WWW, I can be found here. ============================================================================ Table of contents (chapters only) Chapter 1 Programming in ML 3 Chapter 2 Terms in HOL 43 Chapter 3 Theorems in HOL 55 Chapter 4 The HOL notation 77 Chapter 5 Verifying hardware 101 Chapter 6 Uses and limitations of verification 123 Chapter 7 A basic library of gates 133 Chapter 8 Bits, numbers, and words 147 Chapter 9 Comparators 171 Chapter 10 Step 1: ALU overview 209 Chapter 11 Step 2: The adder sub-system 219 Chapter 12 Step 3: ALU verification 253 Chapter 13 Subst, conv, and rewriting 291 Chapter 14 Tactics and tacticals 329 Chapter 15 Theorem continuations 349 Chapter 16 Basic techniques (clocked sequential circuits) 369 Chapter 17 Case study I: shifters 399 Chapter 18 Case studies II: counter 433 Chapter 19 Recursive data types 459 Chapter 20 pico compiler correctness 491 Chapter 21 Verification of FSMs 507 From the preface The book is based upon experiences with a graduate level Computer Science course in Hardware Verification given at the University of Calgary since 1985. It is aimed at graduate and senior undergraduate students in Computer Engineering and Computer Science and at mature readers requiring a self-study introduction to verifying hardware using HOL. The text assumes some prior knowledge of first order logic, functional programming and the lambda calculus, primitive recursion, and digital design. These topics are covered by most undergraduate curricula and in many excellent text books. On the other hand, we anticipate that the arts of hardware specification and verification and the HOL notation will be new to most readers. We aim to give you a good feel for these topics {\it before} you attempt your first session with the HOL system. This is deliberate. We feel that once you are at ease with the basic ideas and principles, you can focus much more sharply on becoming adept at using the HOL system. Chapters 1-3 introduce the most useful features of ML the language in which HOL is hosted, and uses them to write a simple proof checker for propositional logic. Chapter 1 introduces the basics of programming in ML using the built-in pair and list data types before moving on to the use of higher order functions, user-definable data types, and abstract data types. Chapters 2 and 3 implement a proof checker for the propositional logic subset of HOL. Chapter 2 reminds you of propositional logic, defines an abstract data type for terms (valid propositional logic expressions), and then describes a lexer and parser for terms. Chapter 3 gives an axiomatisation of propositional logic (a selected set of axioms and inference rules) and shows you how to carry out proofs in this system. We then implement this axiomatisation using an abstract data type for theorems and show it in action with several more proofs. At the end of these chapters, you should be competent in ML, have a basic understanding of how to implement a proof checker, and be able to carry out proofs in a formal manner. The extended example in chapters 2 and 3 serve as an introduction to mechanical proof checking and will give you a good feel for how the HOL system is implemented. Chapters 4-6 lay part of the foundation for formal work with the HOL proof assistant. Through examples, we teach you the HOL notation, how to specify hardware in HOL, how to conduct proofs in HOL, before giving you an understanding of the possibilities and limitations of the verification methodology. Having completed these chapters, you should be ready to get acquainted with the HOL proof assistant itself. Chapter 4 reminds you of the basic properties of first order logic before sketching the lambda calculus and some of the notation and intuition of higher order logic. It also serves to remind you of things we expect you to know, especially primitive recursion and induction which are used to specify and verify regular VLSI structures. In chapter 4 we also carry out two important forward proofs and introduce the notion of backward proof. In chapter 5, we show you how to specify some simple circuits and regular sub-systems using the HOL notation and stress the need for general solutions that can be applied to families of designs. We also show you how to define implementations of circuits and sub-systems. Finally, we do some paper and pencil verifications of hardware designs. In chapter 6 we show how verification fits into the world of VLSI CAD and point out some of its inherent limitations. By now you should feel comfortable with using the ML subcomponent of the HOL system, with paper and pencil descriptions of hardware in HOL, and with paper and pencil proof outlines. Now is the time to get you started with the HOL system, which is the purpose of chapters 7-9. The initial hurdle we face is this: you will not be able to complete non-trivial proofs with HOL until you know HOL well, and you will not know HOL well until you have completed several proofs. Our first session with the HOL system in chapter 7 merely shows you how to make suitable definitions of some hardware primitives and save them in a theory. We then verify a two input multiplexer built from two inverters and three nand gates. This example shows you how to bring down and use the results saved in a theory and how to extend a theory. We then ask you to verify a number of commonly used gates and save them in a library. The gates include two-, three-, four-, and five-input and and or gates, and the four-input multiplexer. We then devote chapter 8 to building three more useful libraries of facts about bits, numbers, and words which are required for our next hardware proofs. The examples in the text illustrate the value of standard forms, show you how to make primitive recursive definitions and carry out proofs by induction. In chapter 9 we specify and verify both a 1-bit comparator and a ripple comparator subsystem. We also show you how to develop, prove and apply your own mini-theorems on-the-fly whilst working on a larger proof. The proofs in these chapters are completed using the backward proof strategy. Using this strategy, one first sets up the goal to be proved, and then uses HOL tactics to split the goal into simpler parts. If any sub-goal is itself tricky, then we apply the same strategy repeatedly. Eventually we wind up with several small sub-goals each of which is trivial to prove. There will be many ways in which a particular verification can be carried out. In general we eschew tricks, and try to present a straightforward, general and robust style of theorem proving. Chapters 10-12 form a substantial case study which develops the specification and verification of an ALU from scratch. In these chapters, we stress specification and proof development and do not expound all the details of all the proofs. These proofs show you how to exploit hierarchy in proof development and thus take advantage of completed work instead of flattening every proof down to the most primitive level (a large network of inverters, nands, and nors). Since our development so far has been driven by examples, there are some holes in our knowledge of HOL. Chapters 13-15 systematically work through the whole catalogue of HOL tools and methods. We develop our presentation working upwards. In chapter 13, we start at the bottom of the hierarchy. We first explain how terms are represented and they may be constructed and taken apart. Then we define the mathematics of substitution on terms and present the HOL primitives for substitution. We then cover conversions, which take terms to theorems. A conversion only applies to a term at the top level. Some control structure is required to navigate through a term and apply a conversion to its sub-terms, once or repeatedly. HOL has several defined primitives which can be combined to produce these effects; analagous to tacticals, they are called conversionals. Finally we survey and catalogue the different styles of forward inferencing. In chapter 14 we survey and catalogue all the tactics we have used (and will use during the course of this text) and the common tacticals that can be used to weave them together. We also introduce theorem continuations which allow us to pick up and manipulate specified terms and/or theorems through several operations before letting them go. They are used by experts to good effect when they do not wish to clutter up the assumption list with assumptions that are used but once. Chapters 16-18 are concerned with the verification of sequential circuits. Correctness proofs for sequential devices are usually more difficult than those of combinational circuits because we have to match signals that vary with time, but we can make substantial strides with a few standard techniques. Examples include registers, stacks, counters, ... One of our reasons for choosing to work with HOL is its generality. It is good for reasoning about algorithms and software as well as hardware. In chapters 19-21 we introduce recursive data types in HOL and show them in action by proving a few meta theorems about lists and trees. As larger examples we specify and verify insert sort and the correctness of the translation schema for a very small language running on a very small machine. These should give you a feel for the possibilities for software verification in HOL. The inclusion of great numbers of interactive HOL scripts demanded careful attention to their accuracy and currency. This task was aided considerably by the use of the mweb proof script management utilities written by Wai Wong. These utilities, along with an extension written to aid the preparation of this document, are available in the contrib library of the hol88 distribution.