This paper presents new inference fules for conditional statements and looping constructs with pre and post evaluation side effects in their test expressions. These inference rules allow us to reason about the security properties of programs.

Much of the work on verifying software has been done on simple, often artificial, languages or subsets of existing languages to avoid difficult details. In trying to verify a secure application written in C, we have encountered and overcome some semantically complicated uses of the language. We present inference rules for assignment statements with pre and post evaulation side effects and while loops with arbitrary pre evaluation effects in the test expression.

As hardware designs grow in size and complexity, current design methods are proving less adequate. Current methods for specification, design, and test are typically empirical or informal, that is, they are based on experience and argument. Formal methods are solidly based on mathematical logic systems and precise rules of inference. Formal methods offer a discipline which complements current methods so designers can successfully meet the demand for high performance systems.

Formal methods covers a broad and diverse set of techniques aimed at improving computer correctness. This paper explains the role of specifications and implementation models in formal methods, and different approaches to proving their correspondence. We refer to excellent overview papers and cite some recent successful examples of using formal methods in hardware design.

This paper explores the tension between adding functionality to create resilient software and minimizing functionality to make it more feasible to formally verify software.

In goal-directed proofs, such as those used in HOL, tactics often must operate on one or more specific assumptions. But goals often have many assumptions. Currently there is no good way to select or denote assumptions in HOL88. Most mechanisms are sensitive to inconsequential changes or are difficult to use.

Denoting assumptions by filters (matching) makes it easier to maintain large proofs and reuse pieces. But writing the filter predicate can be time-consuming and distracting.

We describe an aid to proof building which synthesizes filter functions from terms. Given examples of terms which should and should not be matched, the function creates an ML predicate which can be used, for example, with filter or FILTER_ASM_REWRITE_TAC.

Recently there has been much research in verifying pipelined microprocessors. Even so, there has been little consensus on what form the correctness statement should take. Put another way, what should we be verifying about pipelined microprocessors? We believe that the correctness statement should show that the parallel machine represented by the pipeline behaves in the same manner as the sequential machine represented by the instruction set semantics. In this paper, we present such a model and examine four pipeline verifications to see how they compare.

This report discusses how the generic interpreter theory can be used inside HOL theorem proving system to specify and verify a microcoded microprocessor system. The theory provides a methodical way to specify and verify computer systems.

What does it mean for an instruction pipeline to be correct? We recently completed the specification and verification of a pipelined microprocessor called Uinta. Our proof makes no simplifying assumptions about data and control hazards. This paper presents the specification, describes the verification, and discusses the effect of pipelining on the correctness model.

Sawtooth is a processor with a 5-stage pipeline, interrupts, and supervisory mode. This thesis describes the results from verifying Sawtooth including the method used and what errors were found in the design.

This paper presents techniques for specifying microprocessor instruction set syntax and semantics in the HOL theorem proving system. The paper describes the use of abstract representations for operators and data, gives techniques for specifying instruction set syntax, outlines the use of records in specifying semantic domains, presents the creation of parameterized semantic frameworks, and shows how all of these can be used to create a semantics for a microprocessor instruction set. The verified microprocessor Uinta provides examples for each of these.

Microprocessor verification has become an area of much interest. The generic interpreter theory provides a model and methodology for the specification and verification of microprocessors. Prior to this model, most microprocessor correctness proofs were ad hoc, and the formalism for one proof would be of little use for another. Recently, we have updated the generic interpreter theory. This report is the verification of a simple microprocessor called Tamarack using this new model. Since Tamarack is simple, this should provide an excellent example of how to apply the generic interpreter theory.

This report details the specification and verification of Tamarack. Sections two through six will highlight the specification, and sections seven and eight will show how the verification was completed.

This report describes the generic interpreter theory in detail and documents its mathematical foundations.

The research presented in this paper describes a parser for the BOLT hardware description language in the HOL theorem proving system. This provides a means of using the same language in the theorem proving system and the VLSI CAD tools used in our work. We have also built a semantic model in HOL for the signal values used in the simulator in our CAD tool suite. We show how this semantic model can be used for reasoning about the signal value data types that are used in the BOLT hardware description language and the VHDL Standard Logic Package.

Formal verification methods provide a way to prove that a circuit structure correctly implements its specification. Low level gate and transistor logic circuits can be verified using methods such as symbolic simulation. Higher level circuits can be verified using theorem--proving methods, providing a multi-leveled approach to complex device verification. Correct modeling of many VLSI circuits requires a signal value data type that includes some degree of strength indeterminacy. The VHDL Standard Logic Package includes such a signal value data type, t_wlogic, that includes 46 unique values. In this paper we provide a foundation for the t_wlogic values and their resolution function that provides a possible link between simulation and theorem-proving. A formalization of the low level signal values used by design tools also facilitates reasoning about CAD tools.

In the fall of 1992, we taught an introductory programming course to a class of non-Computer Science majors. We followed an approach based on formal specifications, with an informal translation to Pascal as an implementation language. This anecdotal paper reports on our experiences and ideas for future attempts.

Iterated structures occur frequently in hardware. This paper describes properties required of mathematical relations that can be implemented iteratively and demonstrates the use of these properties on a generalized class of adders. This work provides a theoretical basis for the correct synthesis of iterated arithmetic structures.

We present techniques for automating many of the tedious aspects of hardware verification in a higher-order logic theorem proving environment. We employ two complementary approaches. The first involves intelligent tactics which incorporate many of the smaller steps currently applied by the user. The second uses hardware combinators to partially automate inductive proofs for iterated hardware structures. We envision a system that captures most of this reasoning in one tactic, SuperDuperHWTac. ideally, users would use this tactic on a goal for proving that a hardware component meets its specification, and get back a proof documented at a level they would have written by hand. This paper presents preliminary work toward SuperDuperHWTac in both the HOL and Nuprl proof development systems.

Large proofs involve many theories which are usually built from separate files. This note describes how the standard UNIX make utility can be used to help manage large proofs. We provide a general Makefile that can be used with few changes and a program for automatically generating dependencies between HOL theories.

Abstract theories are widely used in mathematics because the provide a convenient way to reason about classes of structures. Abstract theories provide proofs about abstract structures which can then be used to reason about specific instances of those structures. Abstract theories are useful for specifying and verifying computer systems because they provide structure and guidance in the specification and verification processes and provide a convenient method of theorem reuse. This report describes and documents a package for using abstract theories in the HOL theorem proving system.

We present a state property called congruence and show how it can be used to demonstrate commutivity of instructions in a modern load--store architecture. Our analysis is particularly important in pipelined microprocessors where instructions are frequently reordered to avoid costly delays in execution caused by hazards. Our work has significant implications to safety and security critical applications since reordering can easily change the meaning and an instruction sequence and current techniques are largely ad hoc. Our work is done in a mechanical theorem prover and results in a set of trustworthy rules for instruction reordering. The mechanization makes it practical to analyze the entire instruction set.

This dissertation contains results that provide a methodological approach to microprocessor verification. We present a hierarchical decomposition strategy for specifying microprocessors. The decomposition follows traditional abstraction levels used by microprocessor designers. We show how the explicit representation of these abstraction levels in the specification can lead to an order of magnitude reduction in the number of long, difficult cases in a microprocessor verification.

AVM-1 is a microprocessor designed at the University of California, Davis to serve as a testbed for experiments in microprocessor verification. This report is intended to document the HOL code that verifies that the design of AVM-1 implements its specification. The report begins by briefly describing the architecture and organization of AVM-1. The organization of the proof is discussed and several technical details relating to the execution of the proof scripts in HOL are presented. The final section of the report contains all of the HOL code necessary to perform the verification.