
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
infolal@lal.cs.byu.edu
Abstract
As hardware designs grow in size and complexity, current design methods are proving less adequate. Current methods for specification, design, and test are typically empirical or informal, that is, they are based on experience and argument. Formal methods are solidly based on mathematical logic systems and precise rules of inference. Formal methods offer a discipline which complements current methods so designers can successfully meet the demand for high performance systems.
Formal methods covers a broad and diverse set of techniques aimed at improving computer correctness. This paper explains the role of specifications and implementation models in formal methods, and different approaches to proving their correspondence. We refer to excellent overview papers and cite some recent successful examples of using formal methods in hardware design.
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 using only informal techniques and practices. The term formal methods includes a set of techniques based on mathematical foundations and analysis. Formal methods [10] 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.1 We discuss what they are, describe different methodologies grouped under the heading formal methods, and suggest where they can be used successfully. Due to space considerations, the bibliography 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 under
contract MDA90494C6115.
1This 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.
What are Formal Methods?
Formal methods are an analytical approach relying on
mathematical models for excluding design errors in hardware.
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 mathematical
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 methods
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 behavior or properties, called the specification,
2. a mathematical model of the design's structure, called the implementation model, or more briefly, the implementation, and
3. mathematical expressions stating relationships between the models established using analysis (proof) to demonstrate that the relations hold.
Formal methods begin with a specification, an implementation model, and a mathematical expression stating the relationship between them. They finish by demonstrating the relationship via precisely defined rules. However, formal methods need not include all three aspects. Benefits accrue from simply writing a formal specification which then serves as an unambiguous reference for implementation, 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:
`def xor2_spec a b out = (out = :(a = b))