Formal Verification

As described in chapter 9 the aim of formal verification is to prove the correctness of a circuit implementation with respect to its specification. In theory the proof of correctness can be carried out by simulating the circuit for all possible input samples and comparing the results with the specification. However, in practice such a verification by exhaustive simulation is too time consuming. Using formal verification the same information can be obtained in less time.

As result of formal verification one either gets some information about the successful verification or otherwise input patterns are generated demonstrating the inequality of two circuit descriptions or illustrating that a required condition is not satisfied.

Similarly to specifying the desired level of abstraction for simulation one has to specify on which level the correctness has to be checked. For example two circuits may be equivalent with respect to their logical behavior but they may have different timings.

Using formal verification one has to distinguish between the method of model checking verifying  a certain property of a design or an implementation and the method of equivalence checking comparing two given circuit descriptions.

To demonstrate the principles of both methods we first introduce an example of a circuit calculating the sum s = a + b + c + d for non-negative binary numbers of length n bits. As shown in figure 14.1 the circuit consists of a ‘4 to 2 reducer’ reducing the four input values to two numbers y and z and a final adder computing s = y + z. The implementation of the 4 to 2 reducer is given in figure 14.2 and figure 14.3 shows a circuit for the final addition.

Model Checking

In a proof of correctness using the method of model checking one has to prove that the property a + b + c + d = y + z (14.1) is satisfied for the 4 to 2 reduction and y + z = s (14.2)

holds for the final addition. Combining both properties we obtain the logical correctness of the complete circuit.

Depending upon the complexity of a circuit such a proof can be performed fully automatically or may require interactive assistance from the user. In the given example the shown decomposition of the problem into two simple conditions (14.1) and (14.2) is such a possible assistance.

Model checking generally requires that the de- signer knows precisely how the circuit works. He should be able to do the proof of correctness by himself, but can delegate the details of the proof to a verification tool.

For the given example the 4 to 2 reduction could alternatively be implemented by using a sub-circuit from the circuit shown in figure 14.4 instead of the circuit from figure 14.2. Both circuits produce quite different intermediate values y and z because different addition methods are used. Nevertheless, both circuits are correct, because the sum y + z is the same for both circuits. Thus the 4 to 2 re- duction is an example of a design task in which the result should be specified in terms of abstract properties to maintain enough freedom in looking for a good design solution.

Example: ‘Pentium Bug’

In [14.8] the verification method of model checking is impressively demonstrated by the example of a well known bug within the division unit of the first Intel Pentium processor. The division unit performs the sequential SRT algorithm producing two bits of the result within every clock cycle using a look up table. It is very difficult to check the device by simulation because the input patterns must be skillfully selected in order to check all entries of the look-up-table.

On the other hand, it is well known that during the SRT procedure all intermediate results have to satisfy an easily formulated arithmetical condition. Thus the formal verification of the division unit by model checking has to check whether, for the implemented hardware, the arithmetical condition of the SRT algorithm really holds. In this way a few minutes of computational time are enough to detect the bug. Furthermore, using the simulation inputs generated by the verification tool it is also easy to localize the fault within the design.

In this example a well known proof of correctness for an algorithm is used to verify essential proper- ties of the designed hardware.

Equivalence Checking

Using the method of equivalence checking to prove the correctness of a design one compares the implemented circuit against another circuit which is known to be correct (the specification). For the example from figure 14.1 describing a circuit to add four binary numbers the specification might be the circuit from figure 14.4 using a sequence of three carry ripple adders. Then equivalence- checking has to prove that both circuits really implement the same function. There are different approaches to carrying out that proof. For example, both circuits can be represented by a normalized notation to simplify the comparison. This method will be described in this section.

A quite different comparison method results from test techniques for manufactured chips presented in section 15.4.1. For example, such a chip test

has to check whether there is a stuck at 0 fault at the primary output y. For that test an automatic test pattern generator (ATPG: Automatic Test Pattern Generation) has to generate input patterns to derive the result y = 1.

Then the ATPG method can be used for equivalence checking in the following way. As shown in figure 14.5, one defines a virtual circuit S combining the circuits to be compared so that output y becomes 1 exactly when the results of specification and implementation differ for an input pattern. Then one starts a test pattern generation to test circuit S for the error y stuck at 0. Whenever a test pattern is found it demonstrates that specification and implementation are not equivalent. On the other hand, if the generator determines that there is no such test pattern then the equivalence between both circuits is proven.

Fundamental Techniques

In this section fundamental techniques are presented which are used by verification tools. To simplify the description we only consider combinatorial circuits. Special problems arising from sequential circuits are presented in section 14.4. 14

Decision Diagrams

A typical problem arising in designing circuits is to verify the correctness of a circuit modification or of a design refinement. As an example we consider the circuits shown in figure 14.6. S2 is a refinement of sub-circuit S1 used within the 4 to 2 reduction from figure 14.2.

A simple way of comparing both circuits S1 and S2 is to derive boolean formulas for the three output signals and to compare the normalized representations. For the example using the full adder function (sum, carry) = FA(a, b, c) = (a ⊕ b ⊕ c, ab + ac + bc) and the half adder function (sum, carry) = HA(a, b) = (a ⊕ b, ab) we obtain the following expressions for S1:

Since the normalized formulas of S1 and S2 are identical both circuits obviously perform the same logic function. Thus indeed S2 is a correct refinement of S1. Please note that this kind of equivalence checking is done by performing boolean transformations. Therefore theorem provers known from computer science, are well suited for that task. They are often used within verification tools.

Unfortunately symbolical transformation of boolean expressions is very time consuming because normalized expressions may become very long. As an alternative representation one can use binary decision trees (BDT) or the more compact binary decision diagrams (BDD) [14.1]. As an example figure 14.7 shows the decision tree and the decision diagram of the function f = a ⊕ b ⊕ c ⊕ d. Starting at the root node value f (a, b, c, d) can be calculated by traversing edges labeled with corresponding input values. In figure 14.7 the path corresponding to f (1, 0, 1, 1) = 1 is emphasized.

By the example it is noticeable that the size of the decision tree for the operator ⊕ grows exponentially with the number n of arguments and has 2n leafs. On the other hand, the size of the decision diagram only grows linearly with n. Here the diagram only consists of 2n + 1 nodes. For this reason the BDD representation is well suited to comparing two circuits efficiently. A normalized compact representation is the so called reduced ordered binary decision diagram (ROBDD). A BDD is called reduced if equivalent subtrees of the BDT are represented by the same node and nodes without branches are omitted. In figure 14.8 an example is shown using the function y = a · b + c.

A BDD is ordered if the order of input variables is well defined. In this case the representation by a ROBDD is uniquely determined. Thus for equivalent functions the ROBDD representations are identical. Since the size of diagrams depends strongly on the chosen order of variables one uses heuristics to determine a favorable order [14.10], [14.5].

Signatures

Using decision diagrams one can easily derive characteristic numbers, called signatures, representing properties of the circuit structure. For example, in the BDD of figure 14.8 there are three different paths from root a to output value 0 and five paths from a to 1. This means that for the 8 possible inputs the result 0 is obtained for 3 times and the result becomes 1 for 5 times.

Similar characteristic numbers can be used to identify circuit inputs. In particular, if one has to compare sub-circuits there is no explicit allocation of input variables such that the order needed for a ROBDD is unknown. In this case one tries to identify the inputs on the base of signatures representing the circuit structure. For example the signature function | fxi | describes how often the circuit produces the result 1 assuming that xi holds. For this counting we assign constant 1 to xi and consider the BDD for the function with the remaining free inputs. Accordingly the signature | fxi | describes how often the circuit result becomes 1 for xi = 0.

For the example from figure 14.8 using the function y = a · b + c the signatures of inputs a, b and c are as follows:

For two equivalent implementations of the function y = a · b + c we can localize c in both circuits because of its signatures. But for inputs a and b such an identification is not possible because these inputs are exchangeable without changing the behavior of the circuit.

In addition to signature functions for input variables there are other signatures to distinguish be- tween arbitrary internal signals. A systematic investigation of the usability of signatures is given in [14.7].