Introduction

1. No mathematical knowledge at all should be required to use a formal verification tool, nor should it be necessary to learn specific languages. We wanted to use a notation designers already know, which they would find intuitive, and which they use for design purposes as well.
2. Formal verification suffers from the well-known state-space explosion problem. Therefore, FV should be integrated into the overall verification process flow so that, if a model size problem arises, we can easily switch back to random simulation. The effort required to do this should take less than an hour.

Why formal verification?

The second force is trends in simulation, which lead naturally to formal verification (see Table 2). If we look at the way simulation was done over three successive generations of CMOS-based mainframe systems, we observe the following trends:

1. Constant decrease in model size. In CMOS 1 the most important unit of test was the system model, whereas in CMOS 3 the most important unit of test was one functional unit of a chip.
2. Change from deterministic tests to random tests.

In general, random tests have more error-detection capability than deterministic tests, but unfortunately the debug time for an error found by random simulation is greater than that for deterministic tests. Another problem in random simulation is that there is no answer to the question "If we run random simulation again, will we improve the test coverage?" If we look again at Table 2, the next logical steps in the evolution are the following:

• Verification: Since the control logic is the major source of design errors, verification models containing only the control logic are the most important models. We designate such a unit of test a module. (A functional unit consists of both dataflow and control logic.)
• Moving from random tests to exhaustive tests.

Models which contain only control logic are small enough to be formally verified; since FV provides exhaustive tests, FV is the ideal candidate for this next step. If successfully applicable, FV outperforms random and deterministic tests in all areas:

1. Since a complete state space is explored, test coverage is better than that of random tests.
2. Error analysis is easier and faster with an FV tool than with simulation using deterministic handwritten tests, because the FV tool searches for a short path to an error.
3. Clearly, there is no way to show that the properties specified by a designer comprise all of the properties required for a circuit to operate correctly. However, in contrast to random simulation, it is known that all of the specified properties hold.

Background

A temporal logic operator consists of two parts: the path quantor and the temporal operator. There are two path quantors: A, which means on all paths, and E, which means for some path. There are four basic temporal operators: G, which means always; F, which means eventually; X, which means next; and U, which means until. See Table 3 for a short description of the basic temporal operators.

For a detailed treatment of temporal logic, see References [2-7]. There are two very important classes of temporal formulas: Safety formulas specify properties that must hold in the complete state space of the circuit, and liveness formulas describe the absence of deadlock in the design.

Integrating FV in a design verification methodology

Figure 1

Module test is divided into dataflow test (typically done by simulation) and control logic test. Testing the control logic requires a complete understanding of the behavior of the design; this activity should therefore be performed by the designers. Since the control logic is normally the most complex logic, formal verification should be used. Introducing such a new step in the overall process flow requires acceptance by the workers involved. We therefore had the following goals:

1. Ease the introduction.
   To ease the introduction of FV for the designers, little knowledge about FV should be required. Ideally no new languages should have to be learned.
2. Reuse protocol checkers in the next level of verification.
   We found it very useful to enhance our test models with protocol checkers. These protocol checkers should also be usable for module test, or, if they are developed during module test, they should be integrable in the next level of verification. This approach reduces the amount of work devoted exclusively to module test.
3. Minimize the risk.
   Currently, formal verification can fail because of model size problems, rendering useless the whole model-generation effort. To avoid this, we have developed a method which is nearly identical for simulation and formal verification. If formal verification fails, we perform random simulation; the extra effort required typically takes less than an hour.

1. Our experience shows that all components in the environment of the model can be represented as FSMs. Therefore this notation, which is familiar and intuitive, was chosen as the input language.
2. The protocol checkers are used instead of complex equations in the computation tree logic (CTL) language [2,7]. We found only simple CTL equations to be intuitively comprehensible; nontrivial CTL equations are hard to understand and prone to error.

Figure 2

The concept of protocol checkers implemented as finite-state machines (FSMs) allows us to automatically generate safety formulas for the formal verification tool. In addition, the protocol checkers can be used in the integration test, improving the overall test process.

Since there are many modules in a complex chip, there are many module test models as well. Therefore, how do we ensure that the module environment description is correct? The technique to achieve this is shown in Figure 3 using two design units which communicate via a protocol. To verify these two units, two module test models are generated [Figure 3(a)]. The first model tests design unit 1, and protocol generator 1 is required to implement the protocol in place of design unit 2. The same scheme holds for the second model, which tests design unit 2 and requires protocol generator 2.

Figure 3

In order to check the protocol, a protocol checker is required; since it can be used in both models, it is called a common protocol checker. Note that this common protocol checker can also be used in the integration test [Figure 3(c)], further increasing our confidence in the environment description of the module test models.

FSM generator

Figure 4

Since timing charts are converted internally to state tables, only state tables are considered next. Figure 5 shows the format of a state table. There are four columns, which describe the current state, the input vector value, the output vector value, and the next state. States are coded symbolically, and input and output values can be represented as binary or symbolic values. In addition, the OTHERWISE statement is supported in the input column. In addition to Mealy and Moore machines [8], two different classes of machines can be represented: deterministic and nondeterministic. Nondeterministic machines require an @ sign to mark state transitions that should be done nondeterministically (e.g., the machine transitions from S1 and the input vector 010 to the states S1 and S2). In simulation, one transition of the set of possible transitions is selected randomly, while in FV all possible transitions are verified exhaustively.

Figure 5

To the states given in the state table, the generator adds an additional state, the error state. The state machine enters this state if during execution an input vector is found which is not defined in the state table for the current state (e.g., if in state Sx an input vector 110 occurs). Both simulation and formal verification check to ensure that no state machine ever enters the error state.

Figure 6 shows an example of a request unit which generates a request accompanied by a request vector, and eventually receives a grant. The request vector points to eight different targets (T0, .., T7), which should be selected nondeterministically. The decision to generate a request should also be done nondeterministically. The FSM may nondeterministically transition from the initial state S0 to any of the request states (R_T0, .., R_T7), or may remain in the initial state. In each of the request states, the FSM generates the request signal and a corresponding Req_Vec value (which is symbolically coded T0, .., T7). As long as no grant is received, the FSM remains in the request state; if a grant is received, the FSM returns to the initial state S0.

Figure 6

Since this tool is used for design and simulation, the designers are already familiar with it. There is no need to learn a new language in order to generate an environment description for formal verification.

Switching between FV and random simulation

Figure 7

Since the model structure contains all FSMs, it is possible to identify all error states in the model. These error states are used in safety formulas. An example is shown in Figure 8 where the first formula states that for all possible execution paths (AG = always globally) in every cycle, the condition holds that the state of the FSM REQ_U0 is not the error state.

Figure 8

Safety formulas are an important class of temporal formulas. Since they can be generated automatically from the model structure, all components required by the formal verification tool are available with no FV knowledge. Users can therefore use the formal verification tool immediately and get accustomed to it.

RuleBase: A formal verification tool

The primary features of RuleBase are the following:

• Several hardware description languages are supported, including VHDL, Verilog**, and DSL (an IBM internal hardware description language).
• RuleBase is integrated in a variety of design environments and is easily integrable into others.
• Sugar, the RuleBase specification language, provides a way for hardware designers who are not CTL experts to read and write specifications easily.
• Various methods address model size problems:
  1. New, efficient model-checking algorithms.
  2. Enhancements of the original SMV algorithms.
  3. Automatic design reductions which leave only parts that influence formula correctness.
  4. New dynamic binary decision diagram (BDD) ordering.
• Debugging aids support result analysis and process analysis:
  1. Counterexamples are presented as simulation-like timing diagrams.
  2. Counterexamples can be translated into simulation control programs.
  3. Formulas which are trivially correct are detected.
• A graphical user interface allows convenient control over the formal verification process. The user interface facilitates user intervention in the process, while allowing a fully automated verification when the user chooses not to intervene.

An example

1. The unit which won the arbitration receives a grant.
2. The Slt_Avl bit for the target selected is reset via the R_Slt_Avl signal.

Figure 9

If we wish to verify the command transfer process, we need a model of the dotted area in Figure 9. We can abstract most of the behavior of the command buffer and the SPL, and build a model which contains only the relevant behavior for the unit to test, as shown in Figure 10 for the unit of the command transfer arbiter. Every SPL is replaced by a request unit, which nondeterministically generates requests and Req_Vec values and eventually receives a grant from the arbiter. The different slots of the command buffer are represented by eight slot units, which provide the Slt_Avl signals. In addition there are two protocol checkers, which check whether more than one grant signal or more than one R_Slt_Avl signal is active at a time. (Note that in reality there are more than two protocol checkers.) The principle of the request generator is shown in Figure 6. Note that every request unit will fall into the error state if it receives a grant without having issued a request.

Figure 10

Figure 11 shows a state table which checks that only one grant (or no grant) is active at a time. In this table only the legal conditions are shown; all other input conditions cause the FSM to transit to the error state. Using the built-in error states of the FSMs, it is easy to generate the temporal formulas which specify that no FSM should ever enter the error state. The corresponding formulas for our model are shown in Figure 8. With the environment description and the safety formulas, a formal verification run could be started. After some time the designer becomes comfortable with the tool, gradually adding liveness formulas to the set of safety formulas which were automatically generated. In Figure 12 an example is given. The first formula states that for some execution path in the future (EF = eventually future) the state of FSM_i will be some state named Sx. Obviously some equations (in addition to those for the safety formulas) are generic and could be generated automatically at the outset. Other formulas, however, are model-specific, such as the last formula, which states that for every request there must eventually be a grant.

Figure 11 Figure 12

Results

The method presented here has been successfully applied to the design process of the MBA chip for the next S/390* generation. Table 5 shows the number of detected design errors in a functional unit of the chip found by different verification techniques. FV detected 24% of the errors very early in the design flow. In this example simulation started very early, so the majority of errors were still found by simulation. However, there were errors that would also have been found by FV. But far more important is that the majority of the errors found by FV would not have been detected by simulation. Table 6 shows that only 36% of the errors found by FV could have been detected by simulation without much effort; 24% were rather complex cases that would have been detected eventually, and 40% of the failed FV cases would probably have slipped through simulation as well.

Summary

1. It relies on the familiar and intuitive notation of finite-state machines; therefore, no learning curve is required.
2. It allows us to switch back to simulation within an hour if FV fails because of model size problems.
3. The protocol checkers developed for FV can be used in the chip and system integration tests, which increases confidence in the protocol checkers. In addition, they help to find and isolate errors during integration testing.

Outlook

• We use message sequence charts [12] as a documentation aid to describe the behavior between components of a module. It would be very useful to compile these charts directly into CTL formulas.
• Most of the FV models which had a state-space explosion problem were characterized by very large structural symmetries. These symmetries induce an equivalence relation between states, which permits a dramatic reduction of state space [13,14]. Ongoing research in this area seems to be very promising.
• Most designers find it easier to specify rules for the behavior of the dataflow than rules for the control logic. A major goal would be to generate automatically an abstracted model of the dataflow; such a model should be behaviorally equivalent to the real dataflow from a control logic point of view. This would allow the control logic to be verified at the same time as the dataflow.

**Trademark or registered trademark of Cadence Design Systems, Inc.

References

Received December 12, 1996; accepted for publication July 10, 1997