page 2  (4 pages)
to previous section1
3to next section

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 interconnected NAND gates. In addition, we must have rigorous definitions of the meaning of MODULE, .nand2, BEGIN, etc., so that the above implementation model also has an unambiguous meaning.

We wish to show that the implementation satisfies the specification. We can express this with the mathematical relation implies and express rigorous definitions of the netlist (not given here for brevity) as a function INTERP in the following manner :

` 8 a b out. INTERP(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 mathematical analysis and the definitions of .xor2 imp, xor2 spec, and INTERP, we can prove that the implementation satisfies the specification.

Notice that the relationship covers all values of the inputs and output (a, b, and out), not just some test values. Of course, in this simple example an exhaustive simulation is trivial, but many formal methods can be applied to circuits with 10100 states or more and still show that the relationship holds for all possibilities.

How Do I Put Formal Methods to Work?

Various formalisms and techniques are applicable to 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 order 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, registertransfer level, or higher) is appropriate as well as which formalism to use (first order logic, higher order logic, automata, 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

Writing 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 of 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 two 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 implementation meets the specification; but how does one ensure that the specification is correct? Ultimately it must 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 representations 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 abstractions 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 implementation. Thus several simple abstractions can be independently verified to yield the overall proof.

Related to the level of abstraction is the expressiveness 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 correctness 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 reason about.

More abstract and expressive languages are more powerful in the long run, but tend to require more initial investment since they are more mathematical and less like representations with which designers are familiar.