A Brief Introduction to Formal Methods *
Paul E. Black Kelly M. Hall Michael D. Jones Trent N. Larson Phillip J. Windley
Laboratory for Applied Logic
Brigham Young University
i nfo- lal@ lal . cs. byu . edu
Abstract
As hardware designs grow in size and complexity, cur-rent
design methods are proving less adequate. Current
methods for specification, design, and test are typically
empirical or informal] that is, they are based on expe-rience
and argument. Formal methods are solidly based
on mathematical logic systems and precise rules of infer-ence.
Formal methods offer a discipline which comple-ments
current methods so designers can successfully meet
the demand for high performance systems.
Formal methods covers a broad and diverse set of tech-niques
aimed at improving computer correctness. This
paper explains the role of specifications and implementa-tion
models in formal methods, and different approaches
to proving their correspondence. We refer to excellent
overview papers and cite some recent successful examples
of using formal methods in hardware design.
Introduction
Current hardware and software designs are orders of
magnitude larger and more complex than they have been.
It is therefore more difficult to design correct systems us-ing
only informal techniques and practices. The term for-m
a l methods includes a set of techniques based on math-ematical
foundations and analysis. Formal methods [ lo]
improve computer design by reducing design errors when
used as a complement to empirical techniques currently
used. This paper provides a brief introduction to formal
methods for hardware design.' We discuss what they are,
describe different methodologies grouped under the head-ing
formal methods, and suggest where they can be used
successfully. Due to space considerations, the bibliogra-phy
is not extensive, but it was carefully chosen to provide
a good starting place for further exploration.
' This work was sponsored by the National Science Foundation
under NSF grant MIP- 9412581 and the Department of Defense un-der
contract MDA904- 94- C- 6115.
' This paper focuses exclusively on formal methods in hardware
design. Formal methods can also be used in broader system design,
including software, but such discussion is beyond the scope of this
paper.
1 7
What are Formal Methods?
Formal methods are an analytical approach relying on
mathematical models for excluding design errors in hard-ware.
Other approaches to design fault exclusion, such
as simulation, are empirical in nature. The chief benefit
of analytical techniques is that they offer 100% coverage
of the design space. That is, with a precise mathemati-cal
model, one can reason about all possible cases. The
chief drawback is the difficulty of building models and
conducting analysis. The precise nature of formal nieth-ods
precludes informal hand waving to dismiss difficult,
extreme cases.
All formal methods involve one or more of the following
three parts:
1. a mathematical model of the design's intended be-havior
or properties, called the specification,
2. a mathematical model of the design's structure,
called the i m p l e m e n t a t i o n model, or more briefly, the
implementation] and
3. mathematical expressions stating relationships be-tween
the models established using analysis ( proof)
to demonstrate that the relations hold.
Formal methods begin with a specification, an implemen-tation
model, and a mathematical expression stating thr
relationship between them. They finish by demonstrating
the relationship via precisely defined rules. However ~ for-mal
methods need not include all three aspects. Benefits
accrue from simply writing a formal specification which
then serves as an unambiguous reference for impleinenta-tion,
simulation, and testing.
A. Simple Example of Formal Methods
As an example of the activities and models discussed
above, we might specify the behavior of an exclusive- or
gate with the following mathematical formula:
I 1
0- 7803- 3177- 6 $ 5.00 0 1996 IEEE
1 1 . 1 . 1 377
IEEE 1996 CUSTOM INTEGRATED CIRCUITS CONFERENCE;
That is, the behavior of an exclusive- or relates inputs, a
and b, and the output, out. Note that the above formula
can easily be assigned a rigorously defined meaning. The
implementation model could be described using a netlist:
MODULE out . xor2_ imp a b;
BEGIN
p . nand2 a b ;
q . nand2 a p ;
r . nand2 p b ;
out . nand2 q r ;
END ;
This implementation is four interconneded NAND gates. In
addition, we must have rigorous definitions of the meaning
of MODULE, . nand2, BEGIN, etc., so that the above imple-inentation
model also has an unambiguous meaning.
We wish to show that the implementdon satisfies the
specification. We can express t, his with the mathemati-cal
relation implies and express rigorous definitions of the
netlist ( not given here for brevity) as a function INTERP
in the following manner :
t V a b out. IPITERP( out . xor2_ imp a b) +
xor2- spec a b out
One can also read the formula as, for all a, b and out,
the interpretation of an XOR2 implementation ( as defined
above) on a, b and out implies the XOR2 specification
( also defined above) on a, b and out. Using mathemati-cal
analysis and the definitions of . xor2imp, x o r 2 s p e c ,
and INTERP, we can prove that the imp1ement. ation satis-fies
the specification.
Notice that the relationship covers all values of the in-puts
and output ( a, b, and out), not just some test values.
Of course, in this simple example an exhaustive simula-tion
is trivial, but many formal methods can be applied
to circuits with lo1'' states or more and still show that
the relationship holds for all possibilities.
How Do I Put Formal Methods to Work?
Va. rious formalisms and techniques are applicable tmo
each part of the process described in the previous section.
To write a formal specification, one must make choices
about which formalism to use ( first order logic, higher or-der
logic, temporal logic, state machines, automata, trace
specifications, etc.) and the kinds of criteria to specify
( functional correctness, liveness, safety, timing, and so
on). To model a circuit, one must decide which level of
abstraction ( gate level, switch level, circuit level, register-transfer
level. or higher) is appropriate as well as which
formalism to use ( first order logic, higher order logic, au-tomat,
a, etc.). The relationship of implementation and
specification may be equivalence, implication, etc. How
one handles each of the three parts forms a taxonomy of
formal methods tools and techniques [ 3 ] .
A. The Specification
W- riting a specification for a design is perhaps the most
difficult aspect of the formal methods process. Formal
specifications require the designer to clearly, concisely,
and unambiguously state what a circuit must do. To
be oi any benefit, the specification must be an abstract
representation of the implementation. That is, it should
state what a circuit must do, not, how. The abstractions
may be any combination of structural ( an ALU instead
of gates), data ( numbers instead of bit vectors), temporal
( instruction cycles instead of clock cycles), or behavioral
( a page from memory is saved to disk instead of which
page is saved to which cylinder). Specifications may be
quite comprehensive, or they may include relatively few
fundamental requirements such as a request is eventually
granted or twc communicating devices never deadlock.
Specifications can also indicate timing properties, load
characteristics, and other properties of the device.
The idea of formal methods is to show that the im-plementation
meets the specification; but how does one
ensure that the specification is correct? Ultimately it
inus6 be validated by the designers: they must examine
the specification and decide that it expresses what they
want. Higher level abstractions help by making it easier
to state desired properties and behaviors. More powerful
representations can more easily and concisely express the
designer's desires. A specification of a few fundamental
properties may be easy to judge correct, but leaves other
important properties only informally specified. Some rep-resentations
are executable, allowing designers to validate
the specification by simulation in addition to review.
One of the most important choices to make is the level
of abstraction in the specification. Higher level abstrac-tions
tend to allow more concise specifications, since less
detail is included. Abstraction causes the specification
to be more easily modified and validated. On the other
hand. an abstract specification is more difficult to relate
to the implementation. Multi- level verification treats the
one level's specification as the next higher level's imple-mentation.
Thus several simple abstractions can be inde-pendently
verified to yield the overall proof.
Related to t3he level of abstraction is the expressive-ness
of the language. A simple language, such as state
machines or first order logic, is easy to reason about -
in fact, many simple languages are decidable: they have
completely automatic algorithms for calculating the cor-rectness
of statements. More expressive languages, such
as higher- order logic, can more concisely express a wide
range of specifications, but, they are more difficult to rea-son
about.
More abstract and expressive languages are more pow-erful
in the long run, but tend to require more initial in-vestment
since they are more mathematical and less like
representations with which designers are familiar.
378 17.1.2
B. The Implementation Model
Creating a model of the implementation is a standard
task for hardware designers. Implementation models are
similar to simulation models in use by designers now. An
implementfation model may be extracted from the simula-tion
model, or, potentially, the same model may be used
for both verification and simulation. The implementation
model must have a well defined interpretation or mean-ing.
A model with simple primitives is easier to reason
about, but is a poor representation of the circuit. A more
detailed model is a better representation of the circuit,
but it is more difficult to use in a verification.
How does one ensure that the implementation model
actually represents the physical device? As with the spec-ification,
validating the implementation can not be done
by machine. Since the model only represents certain char-acteristics
of the device, the final design must be checked
to ensure that it has those characteristics.
Few formal methods tools accept models written for
standard simulation tools without significant syntactic
changes to the model. Most tools require a completely
new model expressed in a different modeling framework.
Thus, a designer often must construct multiple models of
their circuit, one for each design tool ( simulator, formal
methods tool, etc.). Multiple versions raise the cost of
design maintenance and can lead to version skew prob-lems.
Current research in formal methods is aimed at
using standard HDLs for implementation modeling and
providing increased simulation capability.
C. Relating the Implementation and the Specification
There are several methods currently being used for re-lating
implementations to specifications. These include
theorem proving, model checking, equivalence checking,
and language containment. Among these, the most com-monly
used are model checking and theorem proving.
In the model- checking approach, the specification is ex-pressed
as a formula in temporal logic. Such logics make
statements about a world that changes through t, ime, and
they allow reasoning about dynamically changing situa-tions.
Implementation models are usually in the form of
state transition graphs. They can be compared with tlhe
specification automatically. The system may verify that
the models are valid, or it may provide counter- examples
for any specifications falsified by the implementation.
Since model checking typically uses state- based hard-ware
descriptions, it is hetter suited for checking control
structures, as it expresses things such as concurrency and
synchronization. Also, by modeling a particular kind of
logic and world, model checkers aren’t excessively com-plex.
Of coiirse, this means that they are not readily
used on other types of problems.
As an example, the well known model checker SMV [ 6]
uses specifications written in the temporal logic CTL and
implementation models written in a VHDL- like language
for creating state machines.
Theorem proving, in contrast, is a more interactive
technique. When one uses a theorem prover to verify
hardware the usual process is to design a specification and
implementation as logic descriptions first- order predicate
logic, higher- order logic, etc. The designer then guides the
proof assistant tool through rigorous proof steps showing
that the implementation model satisfies the logical specifi-cation.
The level of interaction required of t, he user varies
widely between theorem prover tools: some tools demand
much detail but offer great flexibility ( e. g., HOL); other
tools are more automatic at the expense of flexibility ( e. g.,
PVS, NQTHM).
Theorem provers ultimately rely on the designer to cre-ate
an appropriate model of the hardware, and even to
guide the system ( sometimes explicitly) along the path
to a proof. This can be a complex process, but theorem
provers are very general and can be employed in a wide
range of applications. Theorem provers are not as useful
for reasoning about temporal aspects of hardware. But
theorem provers are well suited for hierarchical methods
of development ( due to their abstraction mechanisms) as
well as reasoning about functional specifications and pa-rameterized
descriptions.
The NQTHM theorem prover uses Boyer- Moore
quantifier- free first order logic ( with equality) to repre-sent
both specifications and implementation models [ 4].
The HOL theorem prover [ 9] uses higher- order logic to
produce a flexible, but demanding environment for crest-ing
specification and implementation models.
What Will Formal Methods Do?
Formal methods will ensure that an implementation
meets a specification, but they will not guarantee that
the final product will always operate perfectly. What for-mal
methods can do is limited by the philosophical limits
on what can be proven, informally defined description lan-guages
and extra- logical factors. These limitations ought
to be kept in mind when describing and discussing the
results of a formal verification project. A more complete
discussion of what formal methods will and will not do
can be found in [ a].
There are aspects of the design process to which the no-tions
of specification and implementation simply do not
apply. Specifications can not convey design intentions and
implementation models can not describe physical proper-ties.
Consequently, the verifier is forced to choose a level
of abstraction for the specification and a sufficiently con-crete
level for the implementation model. These decisions
are part of the process, but should be explicitly stated
when making a claim about verification. For example,
claiming that a microprocessor has been verified at the
gate- level implementation to meet a functional block spec-ification
more completely conveys the scope of the veri-
17.1.3 379
fication than simply stating that the processor has been
verified.
In practice, the designer, verifier and each manufacturer
use different, informally defined languages to describe the
design. Often, the translations between these languages
requires a combination of experience, intuition and luck.
This is especially true of low- level design descriptions
which may consist of nothing more than annotated di-agrams
and a few paragraphs of text. Without mathe-matically
precise definitions of the design- description lan-guage,
it is impossible to know if the verifier’s interpreta-tion
of the design is the same as the designer and if the
design manufactured is the same as the one described by
the verifier. These gaps can be bridged by using a com-mon,
formally defined language at all three levels. 1Vorli
on these t, ypes of languages is underway at Computational
Logic, Inc. and Brigham Young University [ 11].
Claims about verified devices, especially in safety or se-curity
critical applications, should be strictly limited to
factors covered by the logic. Faulty communication, so-cial
hierarchies, political climates, and so forth are usually
not covered in the verification process. For example! ver-ification
dernonstrating that the low- level model of a chip
prevents unauthorized users from accessing data does not
guarantee that a passer- by could not read sensitive data
on a monitor. Consideration of these factors ought to
temper broad guarantees about verified devices.
Formal methods have been successfully used in com-mercial
and academic designs. We mention a few to sug-gest
the wide applicability and utility of formal methods.
Johnson, Miner, and Camilleri[ 5] compare several for-mal
tools by implementing a simple circuit in each of
them. They “ contrast how the underlying formalisms in-fluence
one’s perspective on design and verification.”
Windley and Coe[ 8] verified the correctness of a sim-ple
pipelined microprocessor using HOL ~ and Srivas and
Miller[ 7] report, the formal verification of a commercial
microprocessor. Bainbridge, Camilleri, and Fleming[ l] re-late
verifying menlory protocols in an industrial setting.
They point out formal methods can be used even with a
short trme to m, arket.
Conclusion
Formal methods are a useful addition to the hardware
design process. To male use of formal methods, first a
specification must be written which expresses the design
criteria., then an implementation model must be written
or captured which represents the design. Formal verifica-tion
demonstrates that an implementat, ion model meets
a specification for all cases. However formal methods are
not a silver bullet which prevents all errors. Rather formal
methods are a complement to good design methodology
and testing. The chief benefit of formal methods is not
the final true from the tool, but rather the process that is
required to get, the final result.
While the wide variety of specification and implemen-tation
modeling techniques and the many ways of relating
them can make the choice of how and when to apply for-mal
methods sound daunting, in fact there are relatively
few tools to choose from. Of these tools, the best criteria
for choosing is how they handle the task of relating the
implementation model and the specification. Once a par-ticular
tool is chosen, many of the options for creating the
implementation model and specification are eliminated.
References
[ l] Simon Bainbridge, Albert Camilleri, and Roger
Fleming, Theorem Proving as an Industrial Tool for
System Level Design, in V. Stavridou, T. F. Melham,
and R. T. Boute ( eds.) Theorem Provers in Circuit
Deszgn, North- Holland, 1992.
[ a] Avra Cohn, The Nntion of Proof in Hardware Veri-fication:
Journal of Automated Reasoning, Vol 5, No
4, pp. 127- 139, 1989.
[ 3] Aarti Gupta, Formal Hardware Verification Methods:
A Survey, Formal Methods in System Design, Vol. 1,
1992, pp. 151- 238, Kluwer Academic Publishers.
[ 4] William A. Hunt, Jr., Microprocessor Design Verifi-cation,
Journal of Automated Reasoning, Vol 5, No
4, pp. 429- 460, 1989.
[ 5] Steven D. Johnson, Paul S. Miner, and Albert Camil-leri
Studies of the Single Pulser in Varrous Reasoning
Systems, in R. Kumar and T. Kropf ( eds.), Theorem
Provers zn Czrcuzt Design, Springer, 1994.
[ 6] Kenneth L. McMillan, Symbolic Model Checking, An
Approach to the State Exploszon Problem, Ph. D. the-sis,
School of Computer Science, Carnegie Mellon
University, Pittsburgh, PA, 1992.
[ 7] Mandayam Srivas and Steven P. Miller, Applying
Form a 1 VeriJ cat io n to a Comm ercial Microprocessor,
Proceedings of the 1995 IFIP International Confer-ence
on Computer Hardware Description Languages.
[ B] Phillip J. Windley and Michael Coe, A Correctness
Model for Pipelined Microprocessors, in T. Kropf and
R. Kumar ( eds.), Proceedings of th, e 1994 Conference
on Theorem Provers in Circuat Design.
[ 9] Description of the HOL Theorem Proving System,
( URL: http:// lal. cs. byu. edu/ lal/ hol- desc. htm1)
[ lo] Other Formal Methods Sites page, ( URL:
http:// lal. cs. byu. edu/ otherFMSites. html)
[ ll] The Laborutory for Applied Logic homepage, ( URL:
ht t p: // la1 . cs. byu. edu/)
380
17.1.4