Formal Verification:Sequential Circuits

Sequential Circuits

A simple approach for equivalence checking of sequential circuits is to find a mapping between the flip flops of both circuits. For example, this works well if one circuit is obtained by small modifications from the other. In this case the mapping may already be given because of the known names of nets. Alternatively one can decompose the circuit at the flip flops into combinatorial sub-circuits and then identify the flip flops by comparing structures of adjacent sub-circuits or signatures of signals.

As a result the problem of equivalence checking is reduced to check the equivalence of combinatorial sub-circuits.

For completely different structured circuits comparison becomes more difficult. As an example the next section considers the special case of finite state machines.

Equivalence of Finite State Machines

The sequential circuits M in figure 14.9 and M t in figure 14.10 have the same inputs and outputs, and because all flip flops are driven by the rising edge of a clock signal clk the circuits can be interpreted as finite state machines (FSM).

To compare both circuits we can consider the state diagrams (figures 14.11 and 14.12) of the finite state machines describing the circuit behavior. Then the problem of equivalence checking is reduced to the question of whether both automata are equivalent. In order to answer this question we need a formal description of the problem. Firstly, the following definition describes an FSM without output.

For the circuit M from figure 14.9 we obtain a state diagram with four states shown in figure 14.11. Obviously, if we use (0, 0) as starting state only three of the four states can be reached in practice. Since the output signal y is defined by y = s1 + x we obtain the output function for a given state as is shown in table 14.1.

Because of the following definition two automata are equivalent if they both have the same output behavior. However, the automata may use quite different codings of states, and even the number of states may differ.

Comparing both state diagrams (figures 14.11 and14.12) it turns out that indeed they are equivalent, at though the state codings are different. For example, the state (s0, s1) = (1, 1) of machine M is equivalent to state (s0, s1) = (0, 1) of machine M t.

Considering the different state codings the output functions are always the same for both machines. This is shown in table 14.2.

Using start states S = (0, 0) and St = (0, 0) both machines are equivalent according to the definition. Please note again that in general it is not necessary that both machines have the same number of states. Furthermore, the output functions only have to be identical for reachable states. Therefore it is important that the start states of the circuits are well defined. Also, in practice it should be possible to reach the start state from any other state. Without that reset ability the behavior of the circuits may be undefined in practice.

Altogether, the equivalence proof of the sequential   circuits M and M t of figures 14.9 and 14.10 is performed by constructing the state diagrams and proving the equivalence of both finite state ma- chines using predefined start states.

Modeling of Concurrent Processes

Important properties of sequential circuits that have to be verified are, for example, whether a given state is reachable and whether the circuit is dead lock free. A dead lock is a state that cannot be left for any input.

As an example we consider an asynchronous communication between two hardware units such that each receipt of a message has to be acknowledged. In such a system a dead lock occurs if both components simultaneously become inactive, because both are waiting for an acknowledge. Of course a good implementation of a communication system should be dead lock free. Such synchronization properties can be modeled by Petri nets.

A Petri net consists of places, transitions, and oriented edges from places to transitions and from transitions to places. In figure 14.13 an example of a Petri net is given. The places are denoted by circles and the beams denote the transitions. A state may contain tokens which are individually drawn as dots or which may be indicated by an integer denoting the total number of tokens at a place. In the example the place S1 contains two tokens and place S6 contains one token.

A transition can fire by removing one token from every incoming edge and producing a new token to every outgoing edge. In the example only transition T1 is able to fire. Doing this, a token is removed from S1 and places S2 and S3 will get

If several transitions are able to fire then they may fire in any order. This way one models the unknown duration of concurrent processes and arbitrary signal changes at the primary inputs of a circuit.

Interpreting the given example as a communication process between two components, T1 denotes a transmission of data and T2 denotes the receipt of  an acknowledge. In the given model the transmitter has to wait for an acknowledge after at most two transmissions.

For example, it is of interest whether the protocol is correct or whether under certain circumstances the transmission process may stop because of a dead lock such that none of the transitions is able to fire.

In the given example we have the special case of a finite Petri net such that during its operation the total number of tokens always remains limited. Since finite Petri nets can be also described as finite state machines, one can use methods from automata theory to decide whether a Petri net is dead lock free. Thereby the possible allocations of tokens correspond to the states of a FSM.

Correctness of Synthesis Steps

With automated design tools there are many steps of converting and modifying a design to optimize or refine it or to add some additional information. During the sequence of steps it should be proven that the output produced is never in contradiction with the input. Then we have a correctness by construction. But since in practice the design systems are very complex the correct interaction of all synthesis steps cannot always be proven in advance.

Therfore an explicit verification for each application of a synthesis step becomes necessary. For this one may compare the design before and after a modification. In this special case one can use the fact that both descriptions are very similar and that the type of differences is well known.

For example, the logical behavior of a circuit should not be changed because of the automatic insertion of a scan path and after layout generation the transistor netlist obtained should be equivalent to the former gate level netlist. For these two applications of synthesis tools we now sketch how the verification can be done in practice.

Generating a Scan Path

After automatically generating a scan path the functionality of the circuit is enlarged, improving its testability. Furthermore, there are additional  inputs and outputs. Thus the generated circuit is intentionally not equivalent to the circuit without scan path. Therefore we have to introduce additional specifications about the usage of the new primary inputs in such a way that the new circuit has to behave like the former one. Then using equivalence checking we can prove that the former functionality is also provided by the modified circuit. It is more difficult to verify the correctness of extended functionality because there is no equivalent circuit given by the designer. Thus we need an automatic generation of a high level specification for the scan path to prove the equivalence. Of course that scan path specification itself has to be verified by the designer (section 14.6).

Layout Synthesis

The layout synthesis generates a geometrical de- scription from a given netlist. In a verification step called ‘layout versus schematic’ the circuit information is extracted from the layout and then both circuits are compared. Here circuit extraction needs special attention (chapter 22). Considering the design rules the extractor generates a transistor netlist which may also include resistances and capacities of wires.

Then the verification problem is to compare a transistor netlist (neglecting resistances and capacities) to a gate level netlist. This can be done by replacing subnets of the transistor netlist by gates or flip flops to convert the transistor netlist to a gate level netlist. Also the other way is possible to convert a gate level netlist into a transistor netlist. After that both netlists have the same format and the equivalence check can be performed as shown above.

However, the needed computation time will grow exponentially in the size of the netlist. This effort can be reduced if the mapping of components and nets from one netlist to the other is known. In this case the structure of both netlists can be compared in linear time.

Indeed the mapping needed can be logged during the automatic placement and routing in such a way that it can be used for verification. This example demonstrates that the verification of circuit modification is heavily simplified if the modification steps are well known. In this sense a cooperation between synthesis and verification is useful.

Design Verification

The aim of design verification is to establish the correctness of the first design at a high level of abstraction. This proof of correctness is the basis of the verification of all following design modifications and refinements. It presupposes that a specification of the problem is given in a precise well defined form.

The special difficulty of design verification is that typically the problem specification does not contain hints on how to solve the problem. On the one hand this is because at the time of formulating the problem perhaps no idea of the solution is known. On the other hand, it is a good idea to specify the problem in a quite different way from describing a solution so that it becomes unlikely that the same errors are made within both descriptions.

As an example we consider a specification for dividing numbers. It may specify that for given numbers a and b a value y has to be computed in such a way that the property a = y · b holds. Of course, further information about range and type of numbers and about the precision of the result are necessary. In this way division is specified as the inverse operation of multiplication. The essential point with this specification is that nothing is said about the algorithm for dividing numbers. The specification only describes what has to be computed but not how it can be done.

For example, if we use the SRT algorithm mentioned in section 14.1.1 to solve the given problem then design verification exactly corresponds to proving the correctness of that algorithm. The crucial steps of the proof have to be given by the designer or must be derived by a theorem prover.

For a precise and well defined problem specification one may use a special logic language like HOL (HOL: High Order Logic) [14.3], [14.6] which is suitable for automatic theorem provers. Because the semantics of all statements has to be well defined in terms of a precise mathematical definition such specification languages typically consist of only a few types of statements. There- fore the formulation of a precise problem specification may be as complex as a circuit design.

More powerful languages like VHDL are easier to use because, for example, behavioral descriptions can be written in an easily read notation. Indeed, there are extensions of VHDL which enable the designer also to formulate verification tasks [14.9]. For example the well known test bench used to check a design by simulation is then replaced by a verification bench to describe all relevant properties of a circuit which have to be verified. Furthermore, there are compilers for converting VHDL descriptions into precise logic languages. To accelerate the speed of verification it is even possible to generate automatically more abstract description levels [14.4].

But for all these approaches it has to be noted that in practice the meaning (semantic) of design languages is often not precise enough for a for- mal verification. For example, the same VHDL description may be interpreted differently by a simulator and a synthesis tool, as demonstrated in section 9.1.1. As a consequence a VHDL specification, and also a design verification, may be faulty because of a wrong interpretation of the specification.