54 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44. NO. I.

JANUARY 1995

Formal Modeling and Verification of Microprocessors

Phillip J. Windley

Abstruct- Formal verification has long been promised as a Formal models of VLSI designs are usually called specijica-
means of reducing the amount of testing required to ensure cor- tions; specifications provide a concise description of the behav-
rect VLSI devices. Verification requires at least two mathematical ior of the device that can be used by design engineers, layout
models: one that describes the structure of a computer system
and another that models its intended behavior. These models technicians, production engineers, test engineers, technical
are called specijkations. Verification is a mathematical analysis writers, and users. The application of symbolic mathematical
showing that the behavior follows from the structure. Formal analysis to these models is usually called verification.
verification of microprocessor designs has been quite successful. Verification is largely an exercise in demonstrating that
Indeed, several verified microprocessors have been presented in a design has certain properties. The primary property that
the literature, and one microprocessor where formal modeling
has been applied is commercially available. These efforts were concems us is functional correctness; that is, showing
virtuoso performances-largely academic exercises carried out that a design has an intended behavior. This paper is
by experts in logic and specification. largely concemed with verifying functional correctness,
This paper presents a methodology for microprocessor verifica- but other work by the author has been aimed at using
tion that significantly reduces the learning curve for performing specifications to demonstrate, for example, the integrity
verification. The methodology is formalized in the HOL theorem-
proving system. The paper includes a description of a large case of supervisory mode in a RISC-like microprocessor [20]
study performed to evaluate the methodology. and the correctness of rules used in instruction stream
The novel aspects of this research include the use of abstract reordering [22].
theories to formalize hardware models. Because our model is Correctness verification uses at least two descriptions of
described using abstract theories, it provides a framework for a system: one that describes how the circuit is constructed,
both the specification and the verification. This framework re-
duces the number of ad hoc modeling decisions that must be called the structural specification, and one that describes
made to complete the verification. Another unique aspect of what the circuit is supposed to do, called the behavioral
our research is the use of hierarchical abstractions to reduce specijication. Correctness is shown by demonstrating through
the number of difficult lemmas in completing the verification. mathematical proof that the former implies the latter. Design
Our formalism frees the user from directly reasoning about the faults are discovered as part of demonstrating correctness and
difficult aspects of modeling the hierarchy, namely the temporal
and data abstractions. are corrected as the verification proceeds. Thus, verification
We believe that our formalism, coupled with case studies and can be viewed as part of the design process itself, not as an ex
tools, allows microprocessor verification to be done by engineers post facto process that gives a seal of approval. Typically, some
with relatively little experience in microprocessor specification sort of mechanical proof tool is used in conjunction with the
or logic. We are currently testing that hypothesis by using the verification to reduce the tedium associated with manipulating
methodology to teach graduate students formal microprocessor
modeling. large specifications.
Treating microprocessor design formally can be a difficult
task. Avra Cohn, in 161, describes her specification of VIPER’s
I. INTRODUCTION EBM from informal descriptions supplied by VIPER’s design-
ers as follows:
C OMPUTERS are being used with increasing frequency
in areas in which the correct implementation of the
computer hardware is critical. Testing has traditionally been
VIPER’s top-level specification and its major-state level
were both supplied in a logical language; but its block-
used to exclude faults in computers; however, the effectiveness level model was given partly formally and partly pictori-
of testing is limited by the combinatorial explosion inherent in ally (as was natural). Combining these two parts required
any testing technique. The limitations of testing, coupled with both ingenuity and some guesswork. The guesses were
the ever-increasing size of VLSI devices, have led to a search based on the coincidence of line names, on the names
for alternatives to testing, such as mathematical modeling and of bound variables in the functional detinitions, and
analysis. on the annotations in the text of the definitions. None
of these notational devices can be regarded as formal
Manuscript received July 29, 1991; revised December 2, 1992; July 28, specific ation.
1993. This work was supported by NASA under Space Engineering Research
Center Grant NAGW-I406 and under Boeing Contract NASI-18586, Task This statement not only describes the difficulties of developing
Assignment No. 3. with NASA-Langley Research Center. formal specifications from the kinds of informal descriptions
The author is with the Laboratory for Applied Logic, Department of commonly in use, but it also alludes to the inadequacies of
Computer Science. Brigham Young University, Provo, UT 84602-6576 USA;
E-mail: [email protected]. those descriptions. After the specification is complete, verify-
IEEE Log Number 9407556. ing that the implementation meets the behavioral specification
0018-9340/95$04.00 0 1995 IEEE

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 55

is equally arduous, sometimes requiring the proof of hundreds build on the five axioms that form the basis of higher
of multipage theorems. order logic to derive a large number of theorems that
Every microprocessor verification done to date has been a follow from them.
virtuoso performance, carried out by experts in logic, spec- Rules of inference for higher order logic. These rules
ification, and mechanical reasoning. In contrast to this, we contain not only the eight basic rules of inference from
are striving to make microprocessor verification a viable tool higher order logic, but also a large body of derived
for VLSI design engineers. To that end, this paper presents a inference rules that allow proofs to be done using larger
methodology for verifying microprocessors. This methodology steps. The HOL system has rules that implement the
is embodied in a formalism for the HOL theorem prover, standard introduction and elimination rules for Predicate
providing tool support for a step-by-step approach to system Calculus as well as specialized rules for rewriting terms.
verification. In addition, we have produced several case studies A large collection of tactics to support goal-directed
and are working on additional examples of verified systems proof. Included in HOL are tactics that rewrite a goal
for use in instructing engineers in microprocessor verification. according to some previously proven theorem or defini-
The latter part of this paper presents a case study of the tion, remove unnecessary universally quantified variables
specification and verification of a microprocessor using our from the front of a goal, and split equalities into two
methodology. implicative subgoals.
Organizcition of the Paper: This paper consists of two A proof management system that records the state of an
parts. In the first part, Section I1 presenrs a brief introduction interactive proof session.
to the HOL theorem proving system, Section 111 contains a A metalanguage, ML, for programming and extending
mathematical model of interpreters, and Section IV contains the theorem prover. Using the metalanguage, tactics can
a formalization of that model in the HOL theorem-proving be combined to form more powerful tactics, new tactics
system. can be written, and theorems can be aggregated to form
The second part of the paper demonstrates the use of new theories for later use. The metalanguage makes the
the model in a case study involving the specification and verification system extremely flexible.
verification of a microprocessor called AVM-1. Section 5 For the most part, the notation of HOL is that of standard
presents an introduction to AVM-1, Section VI contains the logic: V.3,A,V, etc. have their usual meanings. A few con-
hierarchical specification of AVM-I in HOL, Section VI1 structs deserve special attention because that are used in this
presents the verification of AVM-I , and Section VI11 presents paper.
our observations about the case study. HOL types are identified by a prefixed colon. Built-
in types include :boo1 and :num.Function types are
11. A BRIEFINTRODUCTION TO HOL constructed using -+. HOL is polymorphic; type variables
are indicated by a type names beginning with an asterisk.
To ensure the accuracy of our specifications and proofs, The HOL conditional statement, written a h I c,
we used a mechanical verification system to develop them. means “if a, then b, else c”.
The mechanical system performs syntax and type checking The HOL list containing elements a , b , c , and d is
of the specifications and prevents the proofs from containing represented as [ a ;b ;c ;d]. A list that contains elements
logical mistakes. The HOL system was selected for this project with type x has the type : (x) list, where x can be
because it has higher order logic, generic specifications, and any valid type (including type variables since HOL is
polymorphic type constructs. These features directly affect the polymorphic).
expressibility of the specification language. Furthermore, HOL EL is a curried function that accepts two arguments, a
is widely available, robust, and has a growing international number, n, and a list, and returns the rith member of the
user base. However, nothing in our work requires that the list.
HOL theorem-proving system be used. Tuples are formed using a comma. Parentheses are only
HOL is a general theorem-proving system developed at the required when the scope of the comma is ambiguous.
University of Cambridge [3, 81 that is based on Church’s The function FST returns the first member of a tuple and
theory of simple types, or higher order logic [4]. Although S N D returns the second.
Church developed higher order logic as a foundation for The construct let v l = e x p r l and v2 = expr2
mathematics, it can be used for reasoning about computational and . . . i n simultaneously defines local variables v l ,
systems of all kinds. Similar to predicate logic in allowing v2, etc. with values expr L , e x p r 2 , etc.
quantification over variables, higher order logic also allows
quantification over predicates and functions, thus permitting
more general systems to be described. 111. FORMAL
MICROPROCESSOR
MODELING
HOL is not a fully automated theorem prover, but, it is more Numerous efforts have been made to formally model mi-
than simply a proof checker; it serves a\ a proof assistant. HOL croprocessors. The best known of these include J. Joyce’s
has several features that contribute to its use as a verification Tamarack microprocessor 1121, W. Hunt’s FM8501 micro-
environment. processor [lo], and A. Cohn’s VIPER microprocessor [51.
Several built-in theories, including booleans, individuals, Tamarack is a simple microprocessor with only 8 instructions.
numbers, products, sums, lists, and trees. These theories FM850I is larger (roughly the size of a PDP-I 1) but has

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
56 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. I , JANUARY 1995

not been implemented (a 32-bit version has been verified and TABLE I
implemented by Hunt et al. 1111). Perhaps the most interesting BASICTYPESFOR INTERPRETER DEFINITION
of these is VIPER, since even though VIPER is signifi-
cantly simpler than today’s general-purpose microprocessors, {true, false}
its verification provides a benchmark of the state-of-the-art in
microprocessor verification.
VIPER was designed by Britain’s Royal Signals and Radar M N-+B stores
Establishment (RSRE) at Malvem to provide a formally ver-
ified microprocessor for use in safety critical applications; it
is commercially available. VIPER is the first microprocessor

ii i
intended for commercial use where formal verification was
used. However, the verification has not been completed be-
cause of the large number of instruction cases and the size of
the proofs in each of the cases. This is not to say that the proof 0 0 0 0 0 0 0 0 0
could not be completed, but that it could be carried out only
t; tj t; 1; 1; t:- t; t; tio
at great expense. Recent work on hierarchical specification
[ 181, coupled with the work presented here, has overcome F F F T F T T F T
the problems that faced the VIPER verification team, and Fig. 1. The function, 7 ,which maps time at one level to another, can be
microprocessors significantly more complicated than VIPER defined in terms of a predicate, G, which is true only when the mapping occurs.
are now within the realm of formal treatment. The case study
in Sections V-VI1 is one example.
n-tuples representing state. These n-tuples have the type
The specifications for the microprocessors mentioned above
appear very different on the surface; in fact, the specification (a1 x a2 x .. . x an-l x a,)
for FM8501 is even in a different language than the specifica-
tions of Tamarack and VIPER. On closer inspection, however, where
we find that each of them (as well as many others) use the
same implicit behavioral model. In general, the model uses a
state transition system to describe the microprocessor. We call
this model an interpreter. Whether or not S is interpreted, we write S 5 S’ to indicate
The essence of verification is to relate mathematical models that S is an abstraction of S‘. When S is an abstraction of S’
at different levels of abstraction. The rest of this section there exists a function, S:S’ + S. The function S is called
gives a mathematical definition of the interpreter model and the state abstraction function.
shows how two interpreters are related. In the discussion that
follows, and for the rest of the paper, we speak of the “abstract C. Time
level” and the “concrete level,” but these terms are relative; In general, different levels in the interpreter hierarchy have
as we move up and down a hierarchy of interpreters, what different views of time. A temporal abstraction function maps
we call “abstract” at one level will be termed “concrete” with time at the abstract level to time at the concrete level [ 9 ] ,
respect to the level above it. As a matter of convention, we
[12], 1151. Fig. 1 shows a temporal abstraction function, 3.
will decorate variables that represent the concrete level with The circles represent clock ticks. Notice that the number of
primes. clock ticks required at the concrete level to produce one clock
tick at the abstract level is irregular.
A. Basic Zypes The temporal projection, 3, can be defined recursively
on time. We define F in terms of a predicate, E, which is
The basic types for our model are shown in Table I. In true whenever there is a valid abstraction from the concrete
addition to these basic types, we also use the following type level to the abstract level. In a microprocessor specification,
constructors: product, written ( a x 0); coproduct, (or G is usually a predicate that indicates when the lower level
+
sum) written ( a p); and function, written ( ( 2 -+ 0). An interpreter is at the beginning of its cycle-a condition that
n-tuple is indicated by (a1 x a2 x . . . x a,-1 x a,). is easy to test.
The function 3 is defined recursively so that F(G.0) is
B. State
the first time that 4 is true and F(G,(n 1)) is the next +
time after time n when S is true. The resulting function is
At times it is convenient to treat state as an object of type monotonically increasing. We use N to represent time. Thus,
S, where S is uninterpreted. This allows us to treat state in we define F:(N + B) x N -+ N such that
an abstract manner, even though we may know nothing of its
structure or content. \inm . ( 7 ~ > m ) =+ (.F(S.n ) > F(G>m ) )
Eventually, we will provide interpretations for S to model
a specific machine. To provide such an interpretation, we We refer the interested reader to the references given above
represent state using n,-tuples. We let be the domain of and to 1171 for the details of the temporal abstraction function.

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 51

D. State Streams Interpreters are state transition systems. An interpreter, 1,

A state stream, U, is a function from time to state,~N-+ S. is a predicate defined in terms of a 3-tuple, 3.IC,C, where
We have chosen n-tuples of booleans, bit-vectors, and stores 3 . K , and C are defined as follows.
to represent state. The application of a stream to some time, Let J be the set of all functions with domain (S x E)
t , yields an n-tuple representing the state at time t. We use a and codomain S. Not all functions in J are meaningful;
lambda expression for our concrete representation. the specifier’s job is to choose meaningful functions. We
use a subset of J to represent the instruction set;‘we call
this set 3. The functions in 3 provide a denotational
semantics for the instructions that they represent.
where In order to uniquely identify each instruction in 3, we
associate it with a unique key. At the abstract level,
tli.a, E N + ( T + B + M ) we take keys from the uninterpreted domain, K . At the
concrete level, keys can have various representations, as
An important part of our theory is the abstraction between we will see in the example in Section 6. We must be
state streams at different levels. State stream u is an abstraction able to choose instructions from 3 according to some
of state stream u’ (written (u5 u’) if and only if predefined selection criteria. The selection is based on
the current state and environment. We define K to be a
1) each member of the range of ’u is a state abstraction of
function with domain (S x E) and codomain K.
some member of the range of u’, and.
We define C J to be a choice function that has domain K
2) there is a temporal mapping from time in u to time in u’. ,
and codomain (S x E -+ S ) .C z selects the state transition
There are two distinct kinds of abstraction here: the first is a function from J that is associated with key K.
data abstraction; the second is a temporal abstraction.
We define an interpreter, Z[s, e ] , as a predicate over the state
Using the state abstraction function, S, and the tempo-
stream, s, and the environment stream, e. The definition of Z
ral abstraction function, F,we define stream abstraction as
is given as
follows
e] E Vt:N . st+l
I[.$, = N(st,e t )
71 5 U’ E 3(S:S’ -+ S) . 3 ( F : N -+ N ) . S o U’ o F u
where
where o denotes function composition.

E. Environments and
The environment represents the external world; it plays kt = K ( s t , e t )
an important part in our theory. The environment is where
interrupt requests originate, reset signals are generated, and In this equation, st(et) is the state (environment) in the
so on. In our model, the environment is used only for input; state (environment) stream s(e) at time t. The predicate, I,
output to the environment is assumed to be simply a function constrains the state of the interpreter at time t 1 to be +
of the state and environment. a function, N , of the state and environment at time t. The
At the abstract level, we treat the environment as an function is determined by applying the choice function, Cz, to
uninterpreted type. We know nothing about its structure or the key retumed by K for the state and environement at time t.
content. We denote it as E. Just as we defined S , the state
abstraction function, we define an environment abstraction G. Interpreter VeriJication
function, E , such that €:E’ -+ E. When we provide an Our goal is to prove a correctness relation between the
interpretation for E , we represent the environment using n- interpreters at different levels of a microprocessor abstraction.
tuples of booleans and bit-vectors. In particular, for two interpreters, 1, and It,we wish to show
We perform the same kinds of abstraction on the environ- that
ment as on states. Temporal abstraction is performed as it was
for states. We define abstraction for environment streams in e m ] * &[se, eel
L[-?,,
the same manner as we defined it for state streams. Thus we
write e 5 e‘ when e is an stream abstraction of e’ and define where s,(e,) is the state (environment) stream at level m
stream abstraction for environment streams as follows: and se ( e t ) is the state (environment) stream at level e. By
definition, we require that s t 5 s, and et 5 e,.
e 5 e’ E 3(E:E’ + E) . 3 ( F : N -+ N) . E o e’ o F =e When this implication is true, 1,is an abstraction of 2,
and I,,,is said to implement It.
The correctness theorem above follows from the following
F. The Interpreter Specijcation lemma: P‘
The preceding parts of this section have given preliminary
Vj ~~..~,(sm,e,,)~(j=Cz(lct))
definitions for concepts that are important in the mathematical
definition of interpreters. This section presents that definition. 3 3~ 0 Sm)(t+c) = j ( ( s0 Sm)tr (E 0 em)t)

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
58 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. 1 . JANUARY 1995

This lemma, which we call the instruction correctness lemma, TABLE I1

states that every instruction follows from the concrete inter- THEABSTRACT FUNCTIONSAND THEIR
TYPES
FOR THE GENERIC
INTERPRETERMODEL
preter, I,. Specifically, it says that for every instruction, j
in J , if j is selected, then applying j to the current abstract Operation I Type
state and environment, (S o s ~ and) ( I~o e,)t, yields the
instructions I :(*kevx(*state-t*env+*state))list
same abstract state that results from letting the implementing
select I :* s t a t e - - + * e n v + * k e y
kev I :*kev-+num
interpreter 1, run for c cycles. substate I : * s t a t e ’- + * s t a t e 1
The instruction correctness lemma suggests a case analysis subenv :*env’+*env
on the instruction set and ignores temporal abstraction, stating Imp1 : ( t i m e ’ + * s t a t e ’ ) + ( t i m e -+*env J ) - + b o o l
only that there exists a time in the future when the states count :* s t a t e ’ + * e n v ’ +*kev
correspond. This lemma plays an important role in the work begin 1 :*key’ I
we describe next.

IV. A MODEL01;INTERPRETERS
IN HOL theory obligations-a set of predicates that define relationships
The similarities in past microprocessor verifications can be among members of the abstract representation. The abstract
exploited to form 8 methodology for microprocessor verifi- theory models any structure with objects and operations that
cation in general. To make this information usable, we have satisfy the predicates.
formalized the microprocessor specification model in the HOL The theory obligations axiomatize the theory. Using the
mechanical theorem-proving system. The formalization does obligations as axioms, we prove theorems of interest about the
several things. abstract objects and operations. The goal is to use the abstract
1) The formalization provides a step-by-step approach to theory to reason about specific objects by instantiating the
microprocessor specification by enumerating the impor- abstract theory with a concrete representation that has been
tant definitions that need to be made for any micropro- shown to meet the obligations. The instantiation specializes
cessor specification. the abstract theorems, producing a set of theorems about
2) Using the formalization, the verification tool can derive the concrete representation. The concrete representation is an
the lemmas that need to be verified from the specifica- instance of the abstract theory and represents a member of the
tion. class of abstract objects that the abstract theory describes.
3) After these lemmas have been established, the verifi- HOL, the verification environment used in the research
cation tool can use the formalization to automatically reported here, does not explicitly support abstract theories;
derive the final result from the lemmas. however, HOL’s metalanguage, ML, combined with higher
order logic, provides a framework sufficient for implementing
To formalize the model developed in the last section, we use
abstract theories [211. Several specification and verification
abstract theories. The next section discusses abstract theories
systems, such as EHDM [ 161, offer explicit support for abstract
and how they can be used to formalize mathematical models.
theories.
The remaining sections discuss the parts of the generic model.

A. Abstract Theories B. The Abstract Representation

A theory is a set of types, definitions, constants, axioms and We specify the abstract representation for the generic inter-
parent theories. Logics are extended by defining new theories. preter model by defining a list of abstract types and operations.
An abstract theory is parameterized so that some of the types Table I1 shows the operations and their types.
and constants in the theory are undefined inside the theory When compared with the mathematical description given in
except for their syntax and an algebraic specification of their the last section, the formalization in HOI, is more operational,
semantics. Group theory provides an example of an abstract largely for efficiency reasons. As an example, we will use
theory: the multiplication operator is undefined except for its lists, rather than sets, to describe the instruction set. HOL can
syntax (a binary operator on an uninterpreted type) and a express choice on sets, but the resulting proofs are consider-
semantics given by the axioms of group theory. ably more difficult than similar proofs about lists. Certainly
Abstract theories are useful because they provide proofs the readability of specifications is an important problem;
about abstract structures which can then be used to reason most microprocessor specifications are difficult enough to read
about specific instances of those structures. In groups, for without unneeded details. Current work by the author and
example, after showing that addition over the integers satisfies others is addressing these notational problems. Our ultimate
the axioms of group theory, we can use the theorems from goal is specifications that are readily readable as well as
group theory to reason about addition on the integers. practically verifiable.
There are two key components of an abstract theory: 1) Before describing the abstract representation, we must em-
the abstract representation and 2 ) the theory obligations. The phasize that the representation is abstract, and thus the types
abstract representation is a set of abstract objects and a set and operations have no definitions. The descriptions that
of abstract operations. The operations are unspecified; that follow are what we intend for the representation to mean.
is, we don’t know (inside the theory) what the objects and The representation is purely syntactic, however: the names
operations mean. Their partial meaning is specified through the are simply convenient mnemonics.

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 59

The following abstract types are used in the representation. environment at the concrete level to produce a key for
: *state represents the state and corresponds to S from the concrete level.
the last section. begin denotes the beginning of the implementation
: *eriv represents the environment and corresponds to E clock cycle.
from the last section. The functions count and begin are used to implement the
: *key is type containing all of the keys and corresponds predicate G that indicates when time at the concrete and
to K from the last section. abstract levels correspond.
In addition to these abstract types, the representation makes We must emphasize once again that even though we have
use of several concrete types: :time, :num,and :bool.The spent several paragraphs defining what each of the members
1i s t and 4 (function) type constructors are used as well. We of the abstract representation mean, they are truly abstract
add primes to the types to indicate that they represent state, and have no meaning in the formal model other than the
time, etc., at the concrete rather than the abstract level of the relationships that are defined in the theory obligations.
hierarchy.
The abstract representation is divided into three parts. The
C . The Theory Obligations
first contains those operations concerned with the interpreter
proper. Theory obligations represent the semantics of the generic
instructions represents the instruction set, which model. Inside the model, the only thing we know about the
is represented by a list. Each member of the list is an abstract representation presented in the last section is what the
instruction that associates a key with * a state transition theory obligations say about it.
function. Throughout the rest of the paper, we make To prove the correctness result, we must know something
use of two selector functions, KEY and IFUNC,which about the implementation. Since the implementation is a
respectively select the key and state transition function member of the abstract representation, nothing is known about
from an instruction. instructions corresponds to 3 it except the requirements given in the theory obligations.
from the last section. Proving that the implementation implies the interpreter def-
select represents the function that selects a key based inition is typically done by case analysis on the instructions;
on the present state and environment. select corre- we show that when the conditions for an instruction’s selection
sponds to K from the last section. are right, the instruction is implied by the implementation. We
key maps an object of type : *key to a number. This call this the instruction correctness lemma.
number is used to index the list containing the instruc- The predicate INSTRUCTION-CORRECT expresses the
tions. key is used in conjunction with the EL function conditions that we require in the instruction correctness lemma.
(which selects the nth member of a list) to implement C INSTRUCTION-CORRECTis a good example of the kind of
from the last section. information that is captured in the generic model. Previous
microprocessor verifications created this lemma, or one similar
The second part contains the abstraction functions that relate
to it, in a largely adhoc manner. INSTRUCTION-CORRECT
the state and environment at the concrete level to the state and
expresses the correctness condition for a single instruction,
environment at the abstract level.
namely that under certain conditions it follows from the
substate is the state abstraction function for the inter- definition of the more concrete implementation.
preter. The domain of substat e is primed indicating The complete definition of INSTRUCTION-CORRECT is
that it is from the concrete level. substate corresponds given below:
to S from the last section. kdef INSTRUCTION-CORRECT s’ e ’ inst =
subenv is the environment abstraction function similar let s = ( A t . (substate ( s ’ t))) in
to substate. subenv corresponds to I from the last let e = ( A t . (subenv (e’ t))) in
section. let g = ( A t . (count (s’ t) (e’ t)
Because we want to prove correctness results about the in- = begin)) in (
terpreter, we must have an implementation to verify the (Imp1 s‘ e ’ ) 3
interpreter against. The third part of the abstract representation ( V t: time‘.
contains three functions that provide the necessary abstract (select(s t) (e t)= (KEY
definitions lor the implementation. (count(s’ t) (e’ t)= beg
Imp1 is the abstract implementation. We could have 3 c. Next g (t,t+c) A
chosen to make this function more concrete and define it ((IFUNC inst) (s t) (e t
as we do the interpreter, but doing so would require that = (s (t + c))))).
every implementation be an interpreter or at least have In the definition, s ‘ ( e ) represents the state (environment)
some pre-chosen structure. As we see in the example, the stream at the more concrete level; s (e) is the state
implementation need not be modeled as an interpreter at stream (environment) at the abstract level and is derived from
all. Thus we say nothing about it except to define its type; s ‘ ( e ’) using the function substate (subenv). The
its structure and operation are completely unknown. predicate g is the predicate D of Fig. 1 . Recall that 0 was
count is analogous to select except it operates at true whenever the states in the concrete and abstract levels
the concrete level. Notice that it uses the state and corresponded. In our model this happens whenever the counter

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
60 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. I , JANUARY 1995

in the implementation (denoted by count ( s ’ t ) ( e ’ t ) ) let :3 =(substate o s’ o abs) <ind

is at the beginning (denoted by begin). Recall that KEY and 15 = (subenv o e‘ o abs) (
I F U N C are the selectors for the key and instruction function (Imp1 s‘ e ‘ ) A
respectively. ( 3 t . g t )=3
INSTRUCTION-CORRECT states that the implementation I N T E 3 P s e)
implies that for every time, t, if inst is selected and the The correctness statement says that if the implementation is
implementation’s counter is at the beginning, then there exists valid on its state and environment streams and there is a time
a time c cycles in the future such that applying the instruction when the concrete clock is at the beginning of its cycle, then
to the current state yields the same state change that the the interpreter is valid on its state and environment streams.
implementation does in c cycles. This theorem is remarkably similar to the requirement for
Using INSTRUCTION-CORRECT we can define the theory correctness developed in Section 111-G. The function abs is
obligations: analogous to 3 and is defined in terms of a general temporal
EVERY (INSTRUCTION-CORRECT S ’ e ’ ) abstraction function TempAbs using the predicate g.
instruct ion.; In the correctness statement, s (e ‘ ) is the state (environ-
k:*key . (key k) < (LENGTH ment) stream in the implementation. The term ( substate
inst ruct ions ) o s ’ o abs) ( ( subenv o e ’ cs abs)) is the state
V k:*key . k = (KEY (EL (key kj (environment) stream for the interpreter defined i n the model.
instructions)) . Thus by definition, s ( e ) is a data and temporal abstraction
The first obligation says that every instruction in the list of s ’ ( e ’ )and s 5 s’ (e 5 e‘).
of instructions, instructions,satisfies the predicate I N - There is one major difference between this correctness
S T R X T I O N - C O R R E C T . The second obligation says that ev- statement and the one given in Section 1114, the additional
ery key maps to some location in the instruction list. The third prerequisite that there exists at least one time when the
obligation says that the abstract function key maps a key to predicate g is true. This requirement is a reset requirement
the instruction with which it is associated (Le., that the list of that ensure liveness. The fact that it shows up here and not
instructions is ordered correctly). in the less formal statement is an example of the utility of
The obligations are used in two ways. First, they are mechanical verification: there are no hidden assumptions.
used axiomatically in proving the correctness result; we do The result in this section is a correctness statement for
this in the next section. Second, the obligations form a set a generic interpreter model. The model defines a class of
of necessary and sufficient conditions for showing that the computational objects. The correctness result is a verification
implementation meets its specification. In the second case, they of every microprocessor that matches the semantics defined in
are the properties that users of the model must prove about an the model; that is, once a microprocessor is shown to meet the
instantiation; we show this in Section VI. At first the theory theory obligations of our model, this correctness result applies
obligations may seem like an additional proof burden, but in to it without further work.
fact, they are typical of the lemmas that have to be proven The most important benefit of the generic model is that it
in any microprocessor proof. More to the point, the theory structures the proof. A generic model states explicitly which
obligations provide a method for deriving the proof obligations definitions must be made (one for each of the members of the
from the specification. Without the theory obligations, these abstract representation) and which lemmas need to be proven
lemmas would be amved at in an ad hoc fashion. about these definitions (namely, the three theory obligations).
This is a great improvement over previous microprocessor
verifications in which these decisions were made on an ad
D. The Currectness Statement hoc basis.
One of the important parts of the collection of abstract the-
orems is the definition of a generic interpreter. The definition
is based on functions from the abstract representation. V. AVM-1
kdef INTERP s e = We have designed and verified a computer designated AVM-
V t: time 1 ( A Verified Micruprucrssur) to serve as a test-bed for
let inst = E L (key (select ( s t) microprocessor verification. For a more detailed look at the
(e t))) instructions in architecture and organization of AVM-1, see [ 171.
s(t + ? j = (IFUNC inst) (s t) (e t) Our design is the result of an attempt to build a mi-
The specification of an interpreter is a predicate that relates croprocessor that is at once verifiable. implementable, and
the contents of the state stream at time 1 + 1 to the contents usable. We have been influenced by our own experience in
of the state stream at time t . The relationship is defined using verifying microprocessors 11 81, the experience of others [ 5 ] ,
the functions from the abstract representation. [ 121, and our desire to provide hardware features in support of
The correctness result can be proven from the definition of operating systems; such features include interrupts, memory
the interpreter and the theory obligations as follows: management, and supervisory modes. AVM-1 is part of a
t- let g = ( A t : time(count (s’ t) (e’ t ) verified chip set being designed and verified by the Computer
= begin)) in Systems Verification Group at the University of Califomia,
let abs = (?‘empubs g) Ln _ .- Other
Davis.
_ . commnents of the svstem include a memow

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 61

TABLE 111 Format 1:

THEPROGRAMSTATUS WORD 31 25 20 15 10 n

Last ALU result was zero

1 opcode dest 1 A 1 B 1 unused 1
Last ALU operation caused a carry Format 2:
Last ALU result was negative
Last ALU operation caused a overflow
Interrupts enabled
F
o
pc
a
dh
e
r
31
l ’
25 20
A 1
15

imrnediate ’1
In supervisory mode
opcode dest ’ unused

management unit, a floating point unit, an interrupt controller, Format 4:

and a direct memory access chip. 31 25 n
1 opcodel unused I
A. The Architectural View Fig. 2. The instruction formats in AVM-I
A computer’s architecture is its programming interface; an
architecture describes a language and how that language is
interpreted. The language definition contains a specification In formats 1 and 2, the instruction is divided into four fields.
of the computer’s state and the instructions available for The top 6 bits (31-26) give the opcode of the instructions.
manipulating that state. The architecture must also define how The next 5 bits (25-21) denote the destination register in most
instructions are selected. operations. The third field (bits 20-16) selects the register used
The Registers: AVM- 1 has a load-store architecture based as the A operand in most operations. In format I , the fourth
on a large register file. The register file is divided into three field is composed of bits 15-1 1 and is used to select the register
portions: used as the B operand. In format 2, the fourth field uses all
1 ) register 0, which is read-only and contains the constant of the 16 remaining bits to form an immediate number (0 to
0; (216 - 1)).
2) seven supervisor-mode registers, including a distin- Format 3 is identical to formats 1 and 2, except that only
guished register for use as the supervisor stack pointer the opcode and destination fields are used. Format 4 uses only
(SSP1. The supervisor-mode registers are read-only the opcode field.
unless the CPU is in supervisor-mode (determined by There is a trade-off between instruction format complexity
the state of the 6th bit in the program status word); and verification effort, so in general the instruction format
3) twenty-four general-purpose registers. should be kept as simple as possible. A regular instruction
Two additional registers are visible at the architectural level: format, while not essential to verification, can greatly reduce
the program counter and the program status word. The program the amount of detail that must be dealt with in the proof.
counter (PC) is used to sequence the computer-it indicates
which instruction to execute next. The program status word B. The Organizational View
(PSW) is used to keep track of the status of the last ALU The implementation of AVM-I can be divided into two
operation, whether or not interrupts are enabled, and the major parts: the datapath and the control unit. We will briefly
privilege level of the CPU. Table 111. shows the meaning of describe the datapath and discuss the timing issues that affect
the 6 bits in the program status word. AVM- 1’s control unit.
The Instruction Set: The instruction set contains 30 instruc- The AVM- 1 Datapath: The AVM- 1 datapath is loosely
tions. The instruction set for AVM- 1 was inspired by the RISC based on the AMD 2903 bit-sliced datapath [ I ] shown in
I instruction set found in Katevenis [ 141; it is a load-store Fig. 3. The signals shown at the right-hand side of the figure
architecture, meaning that most instructions are not, allowed connect to the control unit. The signals on the left go to or
to access memory for their operands. The instruction formats come from the environment. Note that none of the clocking
are simple and regular. signals are shown.
The 30 programming level instructions include the follow- The datapath has three buses, a register file containing 32
ing: registers, and numerous support registers and latches. Two
8, 3-argument arithmetic instructions buses, A and B, are connected to the output ports on the register
8, 2-argument arithmetic instructions that use a 16-bit file and system registers. The C bus is connected to the input
immediate value port on the register file and the system registers. tn addition,
4 instructions for loading and storing registers the interrupt vector is attached to the B bus through a special
10 instructions for performing user interrupts, jumps, port to the interrupt controller.
subroutine calls, and shifts. The A and B buses feed the inputs to the ALU through two
The Instruction Format: The instruction formats are simple latches. The memory buffer register can also serve as the A
and regular. Fig. 2 shows the four instruction formats. All the input to the ALU through a multiplexor on the ALU input.
formats use the same opcode field. The ALU performs simple arithmetic and boolean operations

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
 62 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. I . JANUARY 1995

Calculation
cond c n t l
u
Fig. 4. A phase diagram for AVM- 1.
I Jr-,

Architectural Level

carry src Interpreter

, S h i f t Function
Shifter

Fig. 3. The AVM-I datapath

on the values on its A and B inputs. The results of the ALU

Fig. 5 . A microprocessor specification can be decomposed as a series
operation are fed to the shifter which can perform logical and ofinterpreters.
arithmetic shifts. The result from the shifter is put onto the C
bus for distribution. In addition to a result, the ALU produces
a set of status bits (negative, zero, carry, and overflow) that parts of the specification to demonstrate how writing the
are directly saved in the program status word. specification is aided by the generic interpreter model.
Timing: Rather than describe the control unit of AVM-1 The specification of AVM-I is hierarchical in nature and
in detail, we concentrate on the timing behavior since that uses four levels, as shown in Fig. 5. The bottom level, or
is the most important feature for understanding what is to EBM, is a structural specification; we do not present it here. By
follow. The control unit establishes this timing. The timing of structural specification we mean a specification that describes
AVM-I is based on a four-phase clock as shown in Fig. 4. how the major components of the microprocessor, such as the
During the four phases, the machine performs the following register file and ALU, are connected together. The structural
transitions. specification in HOL corresponds to the netlists commonly
In phase 1, the microinstruction register is loaded from used to describe circuits textually and is similar in form to the
the micro-rom. structural descriptions of circuits written in VHDL or other
In phase 2, the latches that feed the ALU are loaded hardware description languages.
from the register file and system registers. The specifications above the electronic block model are
In phase 3, the results from the ALU and shifter are behavioral specifications. Based on stale transition functions,
calculated. In addition, the MAR can be loaded from they specify what happens without describing how it happens.
the PC in this phase. The use of a single behavioral model (that is, the generic
In phase 4, the result calculated in phase 3 is stored in interpreter model) to describe three different levels in the
the register file and system registers. microprocessor design may seem to be an instance of making
the problem fit the solution; however, modeling the various
levels of a microprocessor design in a uniform way is not
VI. SPECIFYING
AVM- 1 new (see [ 2 ] ) . Describing the behavior of each level in
Presenting the complete specification and verification of terms of state transitions modeled as instructions is quite
AVM-1 is beyond the scope of this paper. This section shows natural.

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 63

The descriptions of the three behavioral levels all follow TABLE IV

the pattem imposed by the generic model. The generic model JUMP CODESFOR THE JMP INSTRUCTION

requires that we define each of the abstract operations in the

representation; the following abstract operations are defined in
each section: instructions,select,key, substate,
and subenv.The definitions of Impl,count,and begin
are defined as part of the specification of the lower level. We
divide each section into parts and define each of these abstract
operations’.

A. Specijjing the Architectural Level

The architectural level is the topmost specification in our
hierarchy- and is thus the most abstract. The architectural
level specification is a formal specification of what one would
generally find in a programmer’s manual for a micropro-
cessor. The specification describes the effect of each of the
architectural level instructions on the processor’s state and
defines how the instructions are selected. The major difference
between the formal specification of the microprocessor and
the programmer’s manual is that the formal specification is
unambiguous and concise. i = GetImm pc mem and
This section provides definitions for thefollowing compo- d = GetDest pc mem in
nents of the architectural level specification: the state-tuple; let jump-cond = JUMP-COND d psw in
three sample architectural level instructions (JMP, ADD, and let new-pc = (jump-cond + (add(a, i ) )
the external interrupt); the architecural operations correspond- I inc pc) in
ing to the operations in the generic interpreter theory (select, (reg, psw, new-pc, mem, ivec)
key, etc); and the architectural level interpreter. The function GetSrcA retrieves the value of the A source
Defining the Architectural Level State: We use a state-tuple field from the word in memory that represents the current
to describe the architectural level interpreter state. instruction (as determined by the program counter). GetDest
(reg, psw, pc, mem, ivec) and Get Imm similarly retrieve the value of the destination and
The only state visible to the architectural level programmer immediate fields from the current instruction. The definitions
is the register file (reg), the program status word (psw), the of these auxiliary functions are precise and available to readers
program counter (pc), the memory (mem), and the interrupt of the specification. The definition of JUMP-COND describes
vector ( ivec). the conditions under which a jump occurs and retums a
Defining the Instruction List: The complete specification boolean value used in the calculation of the new value for
for the architectural level is contained in [19]; here we the program counter.
highlight three sample instructions. The ADD Instruction: The ADD instruction uses instruction
The JMP Insfruction: The JMP instruction uses instruction format 1. The ADD instruction adds the contents of the registers
format 2 (see Table 11). In the JMP instruction, the first 5- selected by the A and B fields in the current instruction and
bit field IS used to specify the jump condition (only the least
stores the result in the register selected by the destination
significant 4-bits are used), the second 5-bit field specifies the
field of the current instruction. In addition, the program status
index of the register to use as a base address, and the 16-bit
word is updated to reflect the results of the calculation, and
immediate tield is used as an offset from the base value.
the program counter is incremented. The HOL specification is
Behaviorally, the JMP instruction has a simple description.
given below:
The value of the program status word and the contents of the
kdef ADD (reg, psw, pc, mem, ivec) =
destination field of the current instruction are used to determine
let a = EL (GetSrcA pc mem) reg and
if a jump should occur according to the conditions in Table
b = EL (GetSrcB pc mem) req and
IV. If so, the program counter is loaded with the sum of the A
d = GetDest pc mem in
register and the value of the immediate field from the current
let result = add (a, b) in
instruction. Otherwise, the program counter is incremented.
let cflag = addp (a, b, result) and
kd,,f J M P (reg, psw, pc, mem, ivec) =
vflag = aovfl (a, b, result) and
let a - EL (GetSrcA pc mem) reg and
nflag = negp result and
’ Note that the presentation that follows is not intended to be an engineering
document that presents the specification and analysis, but rather an expository
zflag
sm
= zerop result and
= get-sm psw and
document that shows how microprocessors can be specified and verified. An ie = get-ie psw in
engineering presentation would differ considerably since the purpose of the
document would be to demonstrate the correctness of the design rather than let new-reg = UPDATE-REG psw d reg
the utility of the model. result and

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
 64 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. 1. JANUARY 1995

new-psw = mk-psw (sm, i e , vflag, newmem = s t o r e (mem, a d d r e s s c d ,

nflag, c f l a g , z f l a g ) and pc) i n
new-pc = i n c pc i n (new-reg, new-psw, new-pc , newmem,
(new-reg , new-psw, new-pc , mem, i v e c ) ivec) .
Clearly there is more to an add instruction than just cal- In the specification, SSP-REG selects the SSP register from
culating the new value and storing it in the right place, the register file; s s p - r e g is a constant value used to avoid
although that is certainly the high point. The specification arbitrary numbers in the specification (much as one tries to
unambiguously defines what state changes take place and avoid them in programming). Several other functions also bear
the definitions of auxiliary functions tell precisely how the explanation: band is bitwise logical conjunction, a d d r e s s
new state is calculated. For example, addp returns a boolean coerces an n-bit word into an address, and s t o r e updates
result, indicating whether there was carry out, aovf 1 returns a a value in memory at a particular address. The constant
boolean result that is true when overflow has occurred, negp lower-8 _ b i t s is an n-bit word with integer value 256.
determines if the result is negative, and zerop determines The Instruction List: Before defining the instruction list and
whether the result was zero. Unlike some reference manuals, the selection function for the architectural level, we must
the definitions of these functions are available for inspection decide on a representation for the keys. The instruction’s
by readers of the specification. One can look at the definitions opcode seems particularly well suited to be used as the key
of these functions and know exactly ho&, for example, carry since it uniquely identifies the instruction and is a natural part
or overflow are calculated. of the description of an assembly language. However, one
The E I N T Instruction: The E I N T instruction describes the instruction, E I N T , has no opcode. We could assign an unused
behavior of the microprocessor upon an extemal interrupt. We opcode to E l ” , but this raises the issue of what to do if
include the specification of the external interrupt in this paper that opcode appears in a program, not to mention making the
because it has interest both in its own right and in showing architectural level model unverifiable.
how events not typically thought of as instructions can be We chose to represent the keys at the architectural level
specified in our model. using a coproduct of boolean five-tuples ( : b t 5 ) and the
The selection criterion for the external interrupt instruction type containing exactly one object ( : one). Left injections on
distinguishes it from the other instructions specified at this the type represent real instructions and right injections repre-
level. Every other instruction is selected based on the value of sent pseudoinstructions. We chose boolean five-tuples because
the opcode portion of the word in memory pointed to by the there were approximately 32 instructions. There is only one
program counter; the E I N T instruction is selected whenever pseudoinstruction, so : one, the type with only one member,
the external interrupt line in the environment is set. Because its was the logical choice for its representation. There was nothing
selection criterion differs substantially from that of the other special about associating :one with the pseudoinstructions;
instructions (and because an assembly language programmer if there had been more than one pseudoinstruction, another
would not really consider it an instruction) we term E I N T a representation (such as boolean n-tuples) would have worked.
“pseudoinstruction.” We now define the architectural level instruction list. Every
Every state variable in the architectural level state except instruction uses the environment abstraction function to give it
the interrupt vector is changed in the execution of the E I N T the proper type. The keys readily distinguish between the real
instruction. The program status word is updated to enter instructions and the pseudoinstructions--clearly specifying the
supervisory mode and disable further interrupts. The contents opcodes associated with each real instruction.
of the program counter are pushed onto the supervisory stack, tdef arch-instructions -
the supervisory stack pointer (SSP) is incremented, and the [ ( I N L ( F , F , F , F , F ) ,JMF);
program counter is loaded with the 8 least significant bits of
the interrupt vector.
( I N L ( T , F , F , F , F ),ADD);
kdet E I N T ( r e g , psw, p c , m e m , i v e c ) =
l e t cd = SSP-REG r e g and
d = ssp-reg i n (INR(one), EINT) ;
let cflag = get-cf psw and I.
vflag = get-vf psw and Dejining s e l e c t : The instruction selection function Op-
nflag get-nf
= psw and code uses the environment and the state to determine which
zflag = get-zf psw and instruction to execute.
sm = T and tde, Opcode ( r e g , psw, p c , m e m , i v e c )
ie = F in (int-e, reset-e) =
l e t new-psw = ( i n t - e A ( g e t - i e psw) ) -+
mk-psw ( s m , i e , v f l a g , n f l a g , INR(one) 1
cflag, zflag) i n INL(opcode ( f e t c h (mem, a d d r e s s
l e t new-reg = UPDATE-REG new-psw d r e g PC))).
( i n c cdj and If the interrupt line in the environment is high and interrupts
new-pc = band (lower-8-bitsIi v e c ) are enabled, then the key associated with the external interrupt
and instruction, I N R ( o n e ), is returned. Otherwise, a left injection

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 65

of the 5-bit opcode portion of the word in memory pointed to TABLE V

by the program counter is returned. THEFUNCTIONS USED TO INSTANTIATE THE ABSTRACTREPRESENTATION OF
THE GENERIC INTERPRETER MODELFOR THE ARCHITECTLRAL LEVEL
Dejining key: To instantiate the generic interpreter model,
we must be able to turn a key into a number that indexes the
instruction associated with that key in the instruction list. The
function Opc-Val performs that task: Opc-Val
t d e f Opc-Val (x:( b t 5 + o n e ) = select Opcode
(ISL x) .--) ( b t 5 - v a l (OUTL x))
I 32.
The function determines whether its argument is a left or
right injection and then, for a left injection, uses b t 5-val
(which retums the integer value of a boolean 5-tuple) to return
the value. Because there is only one possible right injection,
we return 32 without any further work. level interpreter:
Defining s u b s t a t e : Micro-Substate is the function t-Micro-Int s e =
used to transform a micro-level state-tuple into the architec- (V t .
tural level state tuple shown above. s ( t + 1) =
t-def Micro-Substate ( r e g , psw, p c , m e m ,
IFUNC (EL ( b t 6 - v a l ( G e t M P C ( s t ) ( e t ) ))
i v e c , i r , mar, mbr, m p c ) =
micro-instruct ions)
( r e g , PSW, PC, mem, (s t )
ivec) .
(e t))
The instruction register (ir), memory address register
(mar), memory buffer register (mbr), and microprogram
counter (mpc), which are all visible at the micro-level, C. Specifiing the Phase-Level
are deleted from the micro-level state-tuple to produce the The phase-level model is the behavioral representation of
architectural level state-tuple. AVM-1 from the standpoint of AVM-1's polyphase clock.
+Defining subenv: The environment is identical at the AVM-1 has a 4-phase clock that describes how each microin-
architectural level and the micro-level; therefore, the subenv struction is executed. The term instruction does not really fit
function is represented using the built-in identity function, I . at this level, but the idea of a state transition function does
Dejining Impl, c l o c k , and begin: The definitions of and the description of the phase-level behavior by means of
Impl, c l o c k , and b e g i n are taken directly from the spec- the generic interpreter model is both natural and useful.
ification of the micro-level. Imp1 is the definition of the This section provides definitions for the following com-
micro-level interpreter. c l o c k is the microprogram counter ponents of the phase-level specification: the state-tuple, one
and b e g i n is the starting location for the microprogram, sample phase-level instruction (for phase two), the phase-level
FETCHADDR. operations corresponding to the operations in the generic inter-
Dejining the Architectural Level Interpreter: In Section IV, preter theory (select, key, etc.), and the phase-level interpreter.
we defined the generic interpreter, INTERP. The first argument Dejining the Phase-Level State: The state-tuple that de-
to INTERP is the representation. The representation tuple scribes the phase-level interpreter state is shown below.
contains the concrete functions that instantiate the abstract ( r e g , psw, p c , m e m , i v e c , i r , mar, mbr,
operations from the abstract representation. We use the def- , mpc, a l a t c h , b l a t c h , i r e q - f f , i a c k - f f ,
initions from the previous sections to instantiate INTERP m i r , urom, c l k )
and produce a top-level specification of the interpreter at the
architectural level. The instantiation is given in Table V. The variables correspond to the registers, flip-flops, and
k Arch-Int s e = memories in the datapath shown in Fig. 3.
(V t . Defining the Instruction List: The operation of the phase-
s ( t + 1) = level interpreter is fairly simple. We associate each phase in the
I F'UNC system clock with an instruction in the phase-level interpreter.
(EL (Opc-Val(0pcode (s t) ( e t ) ) ) The instructions define the state transitions that occur during
arch-instructions) each phase of the clock. This same information is available
(s t ) in the electronic block model, but is not as apparent there.
(e t ) 1 . During the four phases, the machine performs the following
state transitions shown in Fig. 4 and described in Section V-
B-2. The formal definitions for these phases describe in detail
B. Speczfving the Micro-Level what happens in each phase. Due to space constraints, we
We do not present the details of the specification of the present only the definition of the second phase.
micro-level interpreter because it is similar to the architectural Phase-Two: During the second phase, the latches that feed
level interpreter. The final product of the specification is a def- the ALU are loaded from the register file and system registers
inition that looks much like the definition of the architectural according to the S r c A and SrcB fields in the microinstruction

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
 66 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. I , JANUARY 1995

register. In addition, the interrupt acknowledge flip-flop is set

if the interrupt acknowledge field is set in the microinstruction
register. The clock is updated to select the third phase.
l-d,fphase-two ( r e g , psw, p c , mem, i v e c , Operation Instantiation
i r , mar, mbr, mpc, a l a t c h , instructions list of phase instructions
b l a t c h , ireq-f f , iack f f , key bt2-val
m i r , urom, c l k ) select GetPhaseClock
(int-e) = subst a t e The identity function, 1
l e t new-alatch = (
subenv The identity function, 1
Impl EBM
((SrcA m i r ) = ( F , F , F ) ) --f
count GetEBMClock
(EL (reg-len ( s r c a i r ) reg) I
beain EBMBezin
( ( S r c A m i r ) = ( F , F , T ) ) -+
(EL (reg-len ( d e s t i r ) r e g ) I
( { S r c A m i r ) = ( F , T , F ) ) -+ specification is a predicate called EBM operating over a state
(SSP-REG r e g ) I and environment stream.
( ( S r c A m i r ) = ( F , T , T ) ) -+ psw I The definitions of count and b e g i n are trivial since
( { S r c A m i r ) = ( T , F , F ) ) -+ (wordn 2 5 5 ) there is no temporal abstraction between the electronic block
I PC) i n model and the phase-level. They describe a single phase-
let newhlatch = ( clock, so GetEBMClock returns an arbitrary constant value,
( ; S r c B m i r ) = ( F , F ) ) -+ EBM-Beg i n .
(EL (reg-len ( s r c b i r ) ) reg) I Defining the Phase-Level Interpreter: Table VI shows the
( ( S r c B m i r ) = ( F , T ) ) -i functions used to instantiate the abstract representation. The
(int-fetch ivec) 1 ( i m m i r ) ) i n result is a specification of the phase-level interpreter:
l e t new-iack-ff = I a c k m i r and I- Phase-Int s e =
new-clk = ( T , F ) i n (V t .
( r e g , psw, p c , m e m , i v e c , i r , mar, mbr, s ( t + 1 ) = I F U N C (FL ( h t 2 - v a l
mpc, new-alatch, new-blatch, i r e q - f f , (GetPhaseClock (s t ) ( e t ) ) )
new-iack-ff, m i r , urom, n e w - c l k ) . I ( F , F ) ,phase-one;
The state transition function takes a state tuple and an ( F , T ) ,phase-two;
environment tuple as its arguments and returns a new state ( T , F ) ,phase-three;
tuple. ( T , T ) ,phase-four 1 ) (s t ) ( e t ) ) .
Phase-One, Phase-Three, and Phase-Four: To complete This theorem defines the phase-level interpreter by relating
the specification of this level, we would write formal +
the state at time t 1 to the state and environment at time t.
descriptions of the state transitions that take place in the The relationship is based on the nth member of the instruction
first, third, and fourth phases. list where n is calculated from the phase-level clock.
Dejining s e l e c t : The abstract function s e l e c t returns
a key based on the value of the state and the environment. In AVM- I
VII. VERIFYING
the case of the phase-level, the key is simply the phase-clock.
In this section, we instantiate the generic interpreter model
kdef G e t Phaseclock
to provide the desired correctness lemmas for each level of
( r e g , psw, p c , m e m , i v e c , i r , mar,
the AVM-1 specification. These correctness lemmas are later
mbr, mpc, a l a t c h , b l a t c h , i r e q - f f ,
combined to provide an overall correctness theorem for AVM-
i a c k - f f , m i r , urom, c l k )
1.
1:int-e) = c l k .
For each level, we carryout the following steps.
Dejining key: Key transforms a key into a number. Our
clock is represented by a boolean 2-tuple, so the tuple function 1 ) Instantiate the generic correctness predicate so that it can
bt2-vdl serves as the representation for key. be used in the proofs of the theory obligations.
Defining s u b s t a t e : The state is identical at the phase- 2) Prove the three theory obligations for the instantiation.
level and the electronic block model; therefore, the sub- 3) Using the proofs of the theory obligations, instantiate
s t a t e function is represented using the built-in identity the correctness result from the generic model.
function, I.
Defining subenv: The environment is identical at the A. Verifying the Architectural Level
phase-level and the electronic block model; therefore, the The goal of the architectural level verification is to show
subenv function is represented using the built-in identity that the micro-level implements the architectural level. At
function, I. this level, the micro-level specification becomes the imple-
Defining Impl, count, and begin: The implementation mentation and the architectural level interpreter is used as the
for the phase-level is the electronic block model. The specifi- abstract behavioral model. We want to show that under some
cation of the electronic block model is a structural description; small set of assumptions, the micro-level specification implies
fully expanded, it is about 6 pages long. The top-level of the the architectural level specification.

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 61

The Instruction Correctness Predicate: The correctness Arch-Int-CORRECT-LEMMA =:

predicate represents one of the most important parts of the k- EVERY ( A r c h - I n s t - C o r r e c t
theory obligations. The main advantage of using the generic ( A t . r e g t , p s w t , pc t ,
interpreter model is that once the specification is completed, m e m t , ivec t , i r t ,
the theorem prover can instantiate the generic model to m a r t , m b r t , mpc t )
produce the goals that need to be established to prove the ( A t . i n t - e t ))
final result. This is much better than determining these goals arch-instruct ions.
by trial and error. The Length Lemma: In the length lemma at the architec-
The instruction correctness predicate, once instantiated, says tural level, the opcode variable, o p c , has the type :b t 5+one.
exactly what must be proven about the instructions at the ar- The representation of the keys as coproducts makes the proof
chitectural level to meet the theory obligations and instantiate of the length lemma slightly more interesting than the proof of
the generic model. the length lemma for the other levels, but it is not substantially
A r c h-Ins t -Correc t = more difficult.
FArch-Inst-Correct s’ e ’ p = A r c h - I n t -LENGTH-LEMMA =
Micro-Int s‘ e‘ + k- t/ opc . O p c - V a l opc < (LENGTH
(V t . arch-instructions).
(Opcode ( M i c r o - S u b s t a t e ( s ’ t ) )( e ’ t ) The Order Lemma: The proof of the order lemma for the
KEY p ) A architectural level is also different from the proof of the order
(GetMPC(s’ t )( e ’ t ) = F , E , F , F , F , F ) + lemma for the other levels due to the coproduct representation
(3 c . of the keys. Again, the result is not difficult to prove.
A r c h - I n t -0RDER-LEMMA =
Next(A t ’ . G e t M P C ( s ’ t ’ ) ( e ‘ t ’ )
k- V OPC . OPC = (KEY (EL ( O p c - V a l opt)
= F,F,F,F,F,F) ( t , t + C) A
arch-instructions)) .
(IFUNC p ( M i c r o - S u b s t a t e (s‘ t ) )
Instantiating the Correctness Theorem: After the theory
(e‘ t ) =
obligations for the architectural level have been established,
M i c r o - S u b s t a t e ( ~ ’ ( +t c ) )) ) )
we can instantiate the generic model to provide a correctness
It is interesting to compare this version of the instruction
result for this level. After the instantiation is complete, some
correctness predicate with the generic one given in Section
minor rewriting and beta reduction lead to the final result for
IV-C. The structure is the same, but the names have changed.
this level:
The Theory Obligations: We are required to meet three
ARCH-LEVEL-CORRECT-LEMMA =
theory obligations before we can instantiate the generic model.
k Micro-Int
1) We must show that each instruction in the archi- ( A t . ( r e g t , p s w t , p c t,mern t ,
tectural level specification is correct with respect ivec t , i r t , m a r t , m b r t , m p c t ) )
to the micro-level specification. Specifically, we ( A t . (int-e t ) ) A
must prove that the instruction correctness predicate, ( 3 t . mpc t = F , F , F , F , F , F ) +
A r c h - I n s t - C o r r e c t , iS true for every instruction in Arch-I nt
the architectural level specification. ( ( A t . (reg t , p s w t,pc t , m e m t ,
2) We must show that every key selects an instruction. ivec t ) ) o
3) We must show that every key selects the right instruc- ( T e m p A b s ( A t . mpc t
tion. = F,F,F,F,F,F)))
The Instruction Correctness Lemma: We can prove the in- ( ( A t . (int-e t ) ) o (TempAbs(A t .
struction correctness lemma using symbolic execution for each mpc t = F , F , F , F , F , F ) ) ) .
instruction at the architectural level. For example, here is the According to this result, that the architectural level inter-
instruction correctness lemma for the first instruction in the preter is correct with respect to the micro-level interpreter.
list, JMP. The expression
k A r c h - I n s t - C o r r ec t ( T e m p A b s ( A t . mpc t = F , F , F , F , F , F ) )
( A t . r e g t , p s w t , pc t , m e m t , is the temporal abstraction function that relates time at the
ivec t , i r t , m a r t , mbr t , mpc t) architectural level to time at the micro-level.
( A t . int-e t )
( I N L ( F , F , F , F , F ), J M P ) .
Because of the regularity imposed by the generic interpreter B. Verifiing the Micro-Level
model, we are able to develop a single HOL tactic that proves We do not present the verification of the micro-level because
the instruction correctness lemma for every instruction in the of space constriants. The verification of the micro-level is
architectural level instruction set.This relieves much of the much like the verification of the architectural level. The
burden of proving the instruction correctness lemma. Using following theorem is the final result of the verification:
the individual results for each instruction in the list, we can MICRO-LEVEL-CORRECT-LEMMA =
prove the instruction correctness lemma for the architectural t P h a s e - I n t ( A t . ( r e g t,psw t,pc t,mem t ,
level. ivec t , i r t , m a r t ,

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
 68 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. 1, JANUARY 1995

mbr t,mpc t, alatch t , The Thmry Obligations: Just as at the architectural level,
blatch t ,ires-ff t , the theory obligations to be proven are automatically derived
iack-ff t,mir t, from the abstract theory obligations by HOL.
micro-rom,clk t)) The Instruction Correctness Lemma: To establish the first
( A t . (int-e t)) A theory obligation for the generic interpreter model, we first
(3 t. . clk t = F,F) 3 prove that the phase-level instruction correctness predicate
Micro-Int applies to each of the phases and then use these results to
( ( A t . (reg t,psw t,pc t,mem t,ivec t , establish that the predicate applies to every instruction.
ir t,mar t,mbr t,mpc t ) ) o The following theorem holds that the instruction correctness
(TempAbs(A t . clk t = F,F))) predicate applied to the first instruction, phds e-one,is a
( ( A t . (int-e t)) o tautology.
(TempAbs(A t . clk t = F,F))). PHASE-0VE -EBM-LEMMA =
The lambda expression k Phase-In t-1n st -Cor rect
( A t . (reg t,psw t,pc t,mem t,ivec t,ir t, ( A t . reg t - , p s w t,pc t,mem t,ivec t,ir
mar t,mbr t,mpc t)) t, mar t,mbr t,mpc t ,
in the above theorem models a state vector that is a function alatch t,blatch t , ireq-ff t ,
of time, or in other words, a state stream. This expression iack-ff t,mir t,urom,clk t))
represents a data abstraction of the phase-level state stream ( A t . (ireq-e t))
and is not a micro-level state stream until it is composed with ((F,F),phase-one).
the temporal abstraction function
(TempAbs(X t . clk t = F,F)) We also have to prove a similar lemma about each of the
that maps micro-level time onto phase-level time. other instructions in the phase-level specification. The proofs
The correctness result also contains the following assump- in each case are long but fairly straightforward. They are not,
tion: however, uniform and each must be dealt with individually.
(3 t . (:lk t = F , F ). After we have shown that the instruction correctness pred-
This assumption must be met for the correctness result to icate is true for each of the instructions, we can show that
be valid. That is, unless we can guarantee that at some time it is true for every instruction. This satisfies the first theory
the clock will be at the beginning of its cycle, we cannot say obligation
that the computer will function correctly. Of course, we can Phase-Int-Correct-LEMMA =
guarantee this using a reset button. EVERY
( Phase-Int-Inst-Correct
C. Verifvirig the Phase-Level ( A t . (reg t,psw t,pc t,mem t ,
The verification of the phase-level differs from the veri- ivec t,ir t,mar t,mbr t, mpc t,
fication of the architectural level and the micro-level in a alatch t,blatch t - , ireq-ff t ,
significant way: the implementation is a structural represen- iack-ff t , nir t,urom,(-lkt) )
tation of the electronic block model rather than a behavioral ( A t . (ireq-e t)))
representation. This makes some steps in the verification less [ (F,F),phase-one;(F,T),phase-two;(T,F),
uniform, but the overall process is essentially the same. phase-three;(T,T),phase-four1.
The Instruction Correctness Predicate: Each of the phase-
level instructions must satisfy the instruction correctness pred- The Length Lemma: The second theory obligation is easy
icate if we are to meet the theory obligations. We use the same to show. The theorem holds that the numeric value of a boolean
procedure that produced the phase-level interpreter specifica- 2-tuple is always less than the length of a four-element list.
tion to instantiate the generic correctness predicate. Phase-Int-LENGTH-LEMMA =
Phase-Int-Inst-Correct = t- V clk bt2-val clk <
FPhase-Int-Inst-Correct s f e‘ p = (LENGTH [ (F,F),phase-one;(F,T),phase-two;
EBM :s’ e ’ + (T,F),phase-three;(T,T), phase-four]).
(V t . The Order Lemma: The third theory obligation holds that
(GezPhaseClock (s‘ t)(e’ t ) = KEY p) A the numeric value of the first part of the pair denoting an
(GetEBMClock (s’ t ) (e‘ t) = EBM-Start) instruction is the index of that instruction in the instruction
(3 (I‘ ’ list (i.e., the list is correctly ordered). This lemma is also quite
Next(A t ’ . GetEBMClock (s’ t ‘ ) easy to show by case analysis.
(e’ t’) = EBM-Start)( t , t + c) A Phase-Int-ORDER-LEMMA =
(IFUNC p (s’ t) (e’ t) = s‘(t + c))) I- V clk . clk =
KEY (EL (bt2-val clk)
Because the instruction correctness predicate is derived from [(F,F),phase-one;(F,T),phase-two;
the specification rather than being developed in an ad hoc (T,F),phase-three;(T,T’) ,phase-four]) .
manner, it has the same form as the instruction correctness Instantiating the Correctness Theorem: Having proven the
predicate for the architectural level. theory obligations, we can now instantiate the generic inter-

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 69

preter model. The result of the instantiation can be simplified VIII. OBSERVATIONS
through minor rewriting and beta reduction. Having completed the formal specification and verification
PHASE-LEVEL-CORRECT-LEMMA = of AVM- 1, we make several observations.
FEBM ( A t .
We have shown how a variety of architectural and
(reg t,psw t,pc t,mem t,ivec t,ir t ,
mar t,mbr t,mpc t,alatch t, organizational features can be modeled using the generic
blatch t,ireq-ff t , iack-ff t , mir t , interpreter model. One should not assume that we claim
urom,clk t)) that every architectural feature will map onto the model
(A t . (ireq-e t)) + presented in Section IV. Indeed, many may not.
Phase-Int What does this say, then, for the utility of abstract
(A t . theories? Certainly, many interesting features, such as
(reg t,psw t,pc t,mem t,ivec t,ir t , interrupts, can be mapped onto the model given in this
mar t,mbr t,mpc t,alatch t , paper. Furthermore, formalizing new models is not a
blatch t , ireq-ff t , iack-ff t ,mir t , difficult process. We expect that our models will change
urom,clk t)) and new models will be developed to suit new features.
( A t . (ireq-e t)). The major utility of abstract theories-structuring the
proof-is not diminished.
The result states that the electronic block model implies We are currently exploring the application of the
the phase-level for the concrete state and environment in our generic interpreter theory to the verification of pipelined
model. architectures with feedback. In [23]. we show why
the model presented in this paper will not work for
pipelined microprocessors, describe what it means for a
D. AVM-I is Correct
microprocessor with an instruction pipeline to be correct,
We have successfully instantiated the generic interpreter and provide an example verification of a microprocessor
theory for each of the levels in our hierarchical decomposition. with a 5-stage instruction pipeline.
We establish Each of the interpreter levels uses a different concept
of key. The phase-level, for example, uses the value of
a polyphase clock as the instruction key. The micro-
level, on the other hand, uses location in memory, in
in stages by showing
our representation, as the key to select an instruction.
The architectural level uses an opcode as the key. Thus
a program that is thousands of instructions long at the
We will use the correctness results from each of the levels and micro-level implies that there are thousands of instruc-
Modus Ponens to prove the correctness result for the entire tions in the model. A program that is thousands of lines
CPU. long at the architectural level would still only use the
AVM-CORRECT = 30 instructions given here. For longer microprograms, a
I- let micro-abs = TempAbs different representation of keys would have to be chosen.
( A t . clk t = F,F) in Another interesting point concerning keys is their use
let abs = micro-abs o at the architectural level to distinguish between user
(TempAbs( A t . (mpc o instructions and pseudoinstructions. When specifying an
micro-abs)t = F,F,F,F,F,F))in interpreter, it is important to be flexible about the concept
EBM ( A t . (reg t,psw t,pc t,mem t, of an instruction. We would not have been able to model
ivec t,ir t,mar t,mbr t,mpc t, the external interrupts using the generic interpreter model
alatch t,blatch t , ireq-ff t , if we had not been willing to think of it as just another
iack-ff t,mir t,micro-rom,clk t)) instruction that is selected using an environment signal
(A t (ireq-e t) ) A instead of the program counter.
(3 t clk t = F,F) A The use of coproducts to specify the user instructions
(3 t (mpc o micro-abs)t = and pseudoinstruction keys also points out the utility
F,F,F,F,F,F) * of having a specification language that is powerful and
Arc h-Int ((A t . (reg t,psw t,pc t, expressive. Because HOL had coproducts, we were easily
mem t , ivec t )) o abs) able to specify the distinction between these two types of
( ( A t . (ireq-e t ) ) o abs)). instructions while continuing to use the opcode to select
user instructions.
This result is the same result that we would have proven In order to deal with detailed timing issues, gate-delays
had we not used hierarchical decomposition and the generic would have to be built into the models. There is nothing
interpreter model. However, the process by which we arrived to keep us from building specifications that model gate-
at this result was methodical-the generic interpreter theory delay; however, the models would be more complex and
guided the specification and verification at every level. the verification more difficult.

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
70 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. I . JANUARY 1995

We believe that a better approach is to use heterogeneous

verification environments that make use of several tools
such as standard simulators, symbolic simulators, and
E.)
theorem-proving tools. We are currently working on the
integration of the HOL theorem-proving environment (LL3
and a set of VLSI design tools including a low-level
simulator [7]. Jeffrey Joyce and Carl Seger are working
on integrating the HOL theorem proving environment and
8 (Ie
the Voss symbolic simulator [13]. Other work involving
the integration of BDD’s, model checking and other
theorem-proving tools is underway as well.
The combination of theorem-proving with other means
&3&
of verifying design correctness provides a way to use
the nght tool for the right job. Symbolic simulation, Fig. 6 . The theory hierarchy for the proof of AVM-1.
model checking, and BDD’s are most useful at less
abstract levels of the system design (BDD specifications,
for example, are given in terms of boolean formulae) pected observation is that most of that time was spent on
and theorem provers are most useful at more abstract the specification. The verification was tedious at times,
levels of the system design (reasoning about mathematical yet relatively straightforward. Specification seems to be
operations, for example). the difficult task.
One of the merits of an abstract specification can be Writing a correct specification of the total functionality of
clearly seen in the phase-level specification. The interrupt a large system is usually an iterative process. One writes
request environment signal, ireq-e, is latched into the the specification in pieces, performs some verification,
interrupt flip-flop in the datapath during the first phase. and then uses the feedback from the verification to
The value of the flip-flop is not used until the fourth phase, extend and correct the specification. Once this process is
when its contents are used by the control unit to calculate completed and the specification IS right, the verification
the new contents for the microprogram counter. One could of that fact is relatively simple. This IS just another
legitimately ask why the line is latched so early. The way of saying that the final result is not what is of
point of this discussion is not to debate that issue, but most importance; rather, the process is what is impor-
to point out that the phase-level specification is a useful tant.
tool for exploring these kinds of design issues. The circuit Since writing the specification is the most difficult part,
diagram and specification of the electronic book model we choose to use a theorem prover that provides a more
contain this information, but it is more difficult to extract. expressive specification language, rather than one that
Each level in the decomposition hierarchy corresponds to provides more automation for the proof process. Using a
a real level in the microprocessor. We could introduce logic that forces the specification into unnatural mappings
levels that do not correspond to these real levels. For onto unfamiliar concepts only increases the conceptual
example, we might add an additional level of abstraction burden on the verifier.
between the micro-level and phase-level to reduce the As a result of this observation, we question the com-
size of the instruction set that we have to use at the parison of various theorem-proving environments as be-
micro-level. This is an area that needs further exploration. ing easier to use than others, particularly when the
comparisons are based on redoing a completed proof.
The proof of the instruction correctness lemma was
Once the proof of correctness has been completed in one
done using one tactic at the architectural level and an-
theorem proving environment, the process of reverifying
other tactic at the micro-level. These tactics both operate
it in another should be easy!
through symbolic execution. Because of the great regu-
The proof for AVM-1 contains more than 25 theories.
larity imposed on the proofs of correctness by the generic
Fig. 6 shows how the main theories of the proof of AVM-
interpreter theory, it should be possible to write a tactic
1 are related. This hierarchy shows A m as the child
that solves the instruction correctness lemma for any
theory of a long ancestry that follows the hierarchical
instantiation (provided that the implementation was an
decomposition discussed in the body of this paper. The
interpreter). This would be an important step, since the
picture is not complete; many theories are not shown. For
instruction correctness lemma represents the greatest part example, a theory containing auxiliary definitions is the
of the effort involved in instantiating the theory. ancestor of almost every theory in the proof. A complete
We can also make some observations regarding the actual text of the proof is contained in [ 191.
proof process. Table VI1 presents the run-times for the various theories
It took a person who was intimately familiar with the in the proof on a SPARCStation with 16 megabytes of
HOL theorem prover and experienced in hardware specifi- memory. The times are CPU seconds. The table also gives
cation and verification about 2 person-months to complete the number of primitive inferences required to run the
the specification and verification of AVM-1. One unex- corresponding ML script in HOL. We were using version

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
WINDLEY: FORMAL MODELING AND VERIFICATION OF MICROPROCESSORS 71

TABLE VI1 Even so, this detail must be manipulated to complete

SCRIIT RUN-TIMES
ON A WITH 16 M
SPARCSTATION OF MEMORY the proof.
Temporal abstraction issues are handled completely
within the generic model. This frees the user of the
model from proving theorems about the temporal
abstraction; it is only done once-when the model
is built.
Similarly, data abstraction between the state and en-
vironment streams at the two levels in the model is
clearly defined and consistently performed. The user’s
contributions are to define the abstractions, the model
uses the abstractions to effect the proof.
The abstract proof can be instantiated which allows the
theorems to be reused and saves the effort required to
reverify them.
I mkgen-alu.ml I 8038.4 I 101155 I We believe that the structure provided by the generic
defalu.ml 70815
interpreter model, coupled with the savings afforded by the
defshift .ml 129.0
hierarchical decomposition strategy, make the verification of
defselect .ml
usable microprocessors a viable engineering activity. We are
def-block.ml 1316.0 14738
currently in the process of validating this belief by hav-
mkphase.ml 12818.4 355161
ing graduate students with only an introductory knowledge
of HOL verify microprocessors as a semester project in a
hardware verification class.
The use of a generic interpreter model for specifying
and verifying microprocessors provides a methodological ap-
proach. Making specification and verification methodological
is an important step in turning what has been primarily a
research activity into an engineering activity.
mkavm.ml I 790.9 I 10031
208029.1 I 5167063
REFERENCES
[I1 Advanced Micro Devices, Bipolar Microprocessor Logic and Interface
Data Book, AMD Inc., 1983.
1.11 of HOL, which was built using the Austin Kyoto [*I F. Anceau, The Architecture of Microprocessors. Reading, MA:
Addison-Wesley, 1986.
Common Lisp compiler. [3I A. Camilleri, M. Gordon, and T. Melham, “Hardware verification
The total time to run the proof was 208 029 CPU seconds, using higher order logic.” inFrom HDL Descriptions to Guaranteed
or nearly 58 CPU hours. The proof took almost a week Correct Circuit Designs, D. Borrione, Ed. New York: Elsevier,
1987.
of elapsed time because the core images were quite large [41 A. Church, “A formulation of the simple theory of types,” J. Symbolic
(as high as 29 megabytes) and caused the operating Logic, vol. 5, pp. 56-115, 1940.
system to thrash when garbage collecting (due to a bug [51 A. Cohn, “Correctness properties of the VIPER block model: The second
level,” Tech. Rep. 134, Univ. of Cambridge Comput. Lab., May 1988.
in the memory management unit on the original SPARC [61 -, ‘The notion of proof in hardware verification,” J. Automated
Station). Reasoning. vol. 5, pp. 127-139, 1989.
[71 J. W. Gambles and P. J. Windley, “Integrating formal verification with
CAD tool environments,” in Proc. Fourth Annu. IEEHNASA Symp. VLSI
Design, Oct. 1992, pp. 6.3.1-6.3.11.
181 M. J. Gordon, “HOL: A proof generating system for higher order
IX. CONCLUSION logic,” in VLSI Specifcarion, Verifcation, und Synthesis, G. Birtwhistle
and P. Subrahmanyam, Eds. New York: Kluwer Academic Press,
This paper has shown that the verification of realistic 1988.
microprocessors can be made practical by use of a model of 191 J. Herbert, “Temporal abstraction of digital designs,” in The Fusion of
generic interpreters. The correctness theorem, definitions, and Hardware Design and Verifcarion, Proceedings of the IFlP WG 10.2
lntemational Working Conference. Glasgow, Scotkind, G. Milne, Ed.
abstractions that make up the model are important, for several Amsterdam, The Netherlands: North-Holland, 1988.
reasons. 1101 W. A. Hunt, “The mechanical verification of a microprocessor design,”
in From HDL Descriptions to Guaranteed Correct Circuit Designs, D.
1 ) The model shows exactly what is required to verify that Borrione, Ed. New York: Elsevier, 1987.
an interpreter is correct. No superAuous detail clutters 1111 -, ‘‘Microprocessor design verification,” J. Automuted Reasoning,
vol. 5 , pp. 4 2 9 4 6 0 , 1989.
up the definitions and theorems. J. J. Joyce, “Multi-level verification of microprocessor-hased systems,”
121
2) The abstract proof is easier than the specific proof. Ph.D. thesis, Cambridge Univ., Dec. 1989.
In proving theorems about specific interpreters, some 131 J. J. Joyce and C. Seger, private communication, Univ. of British
Columbia, Oct. 1992.
amount of detail is always necessary for the specific , , 4 1 M. G. H. Katevenis, Reduced Instruction S d Computer Architectures for
interpreter, but not meaningful in the correctness result. VLSI. Cambridge, MA: MIT Press. 1985.

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.
 12 IEEE TRANSACTIONS ON COMPUTERS, VOL. 44, NO. I . JANUARY 1995

[I51 T. Melham, “Abstraction mechanisms for hardware verification,” in [23] P. J. Windley and M. Coe, “The formal verification of instruction
VLSI Specification, Verification and Synthesis, G . Birtwhistle and P. pipelines,” in Proceedings of the 1994 Conference on Theorem Provers
A. Subrahmanyam, Eds. New York: Kluwer Academic Publishers, in Circuir Design, Lecrure Notes in Compurer Science, R. Kumar and T.
1988. Kropf, Eds. New York: Springer-Verlag, Sept. 1994.
(161 SRI Int. Comput. Sci. Lab., EHDM Specification and Verijcafion Sys-
tem: User’s Guide, Version 4.1, 1988.
[17] P. J. Windley, “The Formal verification of generic interpreters,” Ph.D.
thesis, Univ. of California. Davis, Div. of Comput. Sci., June 1990. Phillip J. Windley received the Ph.D. degree in
[18] -, “A hierarchical methodology for the verification of micropro- computer science from the University of California,
grammed microprocessors,” in Proc. IEEE Symp. Security and Privacy, Davis, in 1990.
May 1990, pp. 345-359. He was a member of the faculty at the University
[19] -, “The verification of AVM-1, Tech. Rep. CSE-90-21, Univ. of of Idaho and a member of the technical staff at the
California, Davis, Div. of Comput. Sci., 1990. Department of Energy’s Division of Naval Reactors.
I201 -, “Using correctness results to verify behavioral properties of He is an Assistant Professor with the Department
microprocessors,” in Pmc. IEEE Comput. Assurance Con$, June 1991, of Computer Science at Brighdm Young University,
pp. 99-106. Provo, UT, where he directs the Laboratory for
[21] -, “Abstract theories in HOL.” in Proceedings of rhe 1992 Inter- Applied Logic. His research interests center on
national Worbhop on the HOL Theorem Prover and its Applications, L. the use of formal methods in computer science;
Claesen and M. J. C. Gordon, Eds. New York: North-Holland, Nov. particularly the specification and verification of hardware. He has taught
1992. numerous courses on the use of higher order logic and the HOL theorem
[22] -, “Instruction set commutivity,” in Proc. Fourfh Annu. prover in computer system verification. Dr. Windley is a member of the
IEEEITVIASA Symp. VLSI Design, Oct. 1992, pp. 6.5.1-6.5.11. Association for Computing Machinery.

Authorized licensed use limited to: Univ of Calif Santa Cruz. Downloaded on October 15,2024 at 21:07:37 UTC from IEEE Xplore. Restrictions apply.