January 31, 2012 -- In this final article in a three-part series about formal verification concepts, we examine the assertion-based verification flow and some of the formal verification algorithms. This kind of approach has become necessary as SOC designs become more challenging and the traditional method of simulation proves too slow, too costly, and insufficient in terms of coverage.

Some satisfiability (SAT) tools work partly on the circuit and partly on conjunctive normal form (CNF). These are called hybrid SAT solvers. The netlist is kept along with learned clauses and conflict clauses, which are added during analysis.

Formal analysis of sequential circuits with a single clock

In the case of sequential designs, the SAT engine first tries to find a witness for the EF(P) type of property passed to it. If it is not able to find a witness, it tries to find a proof that the property can never be true. The DPLL algorithm is used for witness search and the well-known induction theorem in combination with DPLL is used for proof search. These are described in detail in the subsequent sections. However, before that, it is necessary to understand the concept of unrolling.

The mathematical engine of SAT — the DPLL algorithm — always analyzes combinatorial logic. In reality, however, the designs are always sequential in nature. As a result, the sequential logic needs to be converted to combinatorial logic before it can be used by the DPLL algorithm. This brings in the concept of "unrolling."

Unrolling

Assume that the design always begins with a pre-determined initial state. Here "state" means the value of all the sequential elements or flops in the design. During SAT analysis, all the flops are removed from the design to begin with and the initial value of each flop is applied to its output net. This is just the representation of the design in its initial state without the flops. The original circuit and the circuit without flops are shown in Figures 1 and 2, respectively. The initial state of both the flops is assumed to be 0.

Figure 1. Original circuit.

Figure 2. Circuit at cycle 0.

Whenever a clock cycle comes, the state of the design changes and the value at D pin of each flop is propagated to Q. At this stage, unrolling is done. This means a copy of the complete design is created which represents the design state at the end of cycle 1. Now, the complete design appears twice, the first version represents the design state at cycle 0 (or the initial state) and the second version represents the design state at cycle 1 where the variables in cycle 1 are represented in terms of variables in cycle 0 and/or cycle 1. This is illustrated in Figure 3.

Figure 3. Circuit at cycle 1.

Note that there are eight design variables after the removal of the flops at cycle 0. In cycle 1, a copy of the design is created which duplicates the same eight variables and appropriately connects the cycle 1 variables to cycle 0 variables, wherever necessary. Hence, the following connections are made:

Optimization is done at each stage and the actual circuit generated may get reduced. It can be seen that now the design state at cycle 0 as well as at cycle 1 is available, purely in terms of combinatorial logic. Similar unrolling can be done in subsequent cycles as required. The combinatorial circuit generated by unrolling is used by SAT for witness and proof search.

It is interesting to note here that, in formal analysis, when we are at a particular cycle, say at cycle n, the state of the design in all previous clock cycles is not fixed, and it is represented in terms of variables of all previous cycles. Hence, SAT is free to assign values to variables in any clock cycle to find a witness. This is the basic concept of formal, that it has control on variables of all previous cycles and can assign values to them. This is different from the simulation method, where once we reach cycle n, the signal values for all previous cycles are fixed.

Witness search

The DPLL algorithm is used for witness search. Unlike the combinatorial circuits, where there is no concept of clock, in sequential circuits the witness search is not limited to the initial state of the design. If a witness is not obtained in the cycle 0, it needs to be searched in subsequent cycles. This is possible by unrolling the circuit at each active edge of the clock. After unrolling, it again becomes a combinatorial witness search problem, and is handled in the same way as explained previously. Note that the design being single-clock, no clock is actually passed to the SAT solver. Each unrolling is just a global clock tick for all flops.

In this case, the tool begins with witness search in cycle 0 or the initial state of the design. If it is not able to find it, it unrolls the design once and again does a witness search. This process goes on until it is able to find a witness. If, however, it is not able to find the witness even after several cycles, it halts its analysis, and instead tries to prove that the property can never become true.

As an example to illustrate the witness search, refer to Figure 2. For property EF(!x & y), there is no witness at cycle 0 (i.e., no satisfiable assignments for x(0)=0 & y(0)=1). But a satisfying condition (a witness) can be found at cycle 1 which involves variable assignments from both the cycles. It can be seen from Figure 3, that in this case the witness for x(1)=0 & y(1)=1 is a(0)=0, b(0)=1, a(1)=1 and all others are don't care.

Thus it can be concluded that a witness exists for property EF(!x & y) at cycle 1 and the witness is a=01, b=1x, c=xx where the values of all the variables are defined for 2 cycles. x in the witness is eventually replaced with 0 or 1 so as to take care of optimizations happening for re-convergent logic, otherwise simulators may show different results.

Proof search

Unlike combinatorial circuits, proof for sequential circuits means proving that the property will not hold true in any clock cycle. One of the algorithms for finding a proof is the Induction Algorithm. There are two main steps in this algorithm:

Step 1 finds an induction condition, that if the given formula (or CNF) is not true for N consecutive cycles, starting with an all x state of the design, then it cannot be true in N+1th clock cycle. This is depicted in Figure 4. Step 2 checks that the formula is indeed not true for the first N cycles starting from the initial state of the design.

The above two steps together prove that the property will never be true.

In Step 1, if no witness is found in the first cycle itself when all flops are at the x state, the property is proved to be false, as the first state covers all possible states.

Note, that when we start with an all x state, we allow any state to be the initial state, and hence at cycle N we cover all possible N-length sequences of the design starting from any state and completing on any state N cycle forward from that. Now, if we find that when a property is not true for N cycles implies that it is not true for N+1th cycle, then this rule is valid for all N-length sequences of the design.

Hence, if it can be proved that the property does not hold true for the first N cycles starting from the initial state, it is proved by induction that the property will not hold true in N+1th cycle and so on. This proves the property false for all the cycles.

The complete algorithm is depicted below.

Figure 4. Finding induction condition.

Figure 5. Complete Induction Algorithm.

One can think that if any property is actually false, then it should never occur. In other words, no witness should exist for that property. Hence, the proof should always be found in the first cycle itself. But this is not true.

The reason being that on starting from an all x state as the initial state, the complete state space of the design is 2n where n is the number of flops in the design. A lot of states in the complete state space may be unreachable if started from a valid initial state of the design. As a result, the witnesses that are found during the process of proving belong to the unreachable state space. During proof search, all the states in the complete design state space are available to SAT to find a witness, since it starts from an all x state. When the design is unrolled for the first time, all the states that can be reached after 1 cycle starting from any state in the design are available to the SAT engine. Similarly, in the Nth cycle, all the states which are N-1 cycles away from any state of the design are available to SAT.

For a false property, in case a witness is found in the Nth clock cycle, it means that an N-length sequence exists in the unreachable state space of the design where the property holds true in the Nth state. The more the value of N, the longer it takes for SAT to find a proof. Hence, decreasing the sequence length in the unreachable state space helps the SAT solver to find the proof faster. Consider an example given below where a minor RTL change enhances the SAT solver's performance drastically. Assume there is a counter counting from 0 to 20. The RTL is:

In this case, if it is a 5-bit counter, the total possible states are 32 out of which 21 are reachable states. In order to check if cnt is ever equal to 31, the SAT engine can go on wandering up to 11 clock cycles in the unreachable state space. Let the RTL be modified, however, as follows:

In this case, as soon as the SAT starts from any unreachable state, it is pulled back into the reachable space by the RTL code. Such RTL is "formal friendly."

There are several methods that help proof algorithms to converge faster. Some methods reduce the unreachable state-space while others apply some abstraction techniques to reduce the complexity of design [3].

Formal analysis of sequential circuits with multiple clocks

As discussed earlier, unrolling eliminates all flops of the design and connects the input of each flop in cycle m to its fanout logic in cycle m+1 at the active edge of the clock. In the case of a single-clock design, this generates correct logic. But this is not valid if the design has multiple clocks running on different frequencies because in this case, all flops of the design may not be triggered on a single-clock event. As a result, the clocks cannot be abstracted-out in this case and actual clock waveforms are needed for the formal analysis.

To overcome the above problem, an FSM can be inserted in the design which works on a virtual clock and generates the actual design-clock waveforms. The design flops in this case are transformed into a master-slave configuration as depicted in Figure 5 and the clocks generated by the FSM are connected to these flops. Additional logic is added for handling asynchronous set or reset signals.

Figure 6. Flop transformation (master-slave).

Once this transformation is done the formal analysis becomes similar to the single-clock design as described earlier.

Formal-verification applications

The formal verification technique is effectively being used in several verification products in the EDA industry. SpyGlass® is one such predictive analysis tool which works on the concept of "Early Design Closure®."

The SpyGlass family makes use of formal technology to verify properties across various design domains. It has a rich set of rules which automatically identify such design properties, create implicit assertions, and then verify them using formal technology. These properties include, but are not limited to:

Grey encoding check. FIFO and handshake checks. Data loss check in case of fast to slow clock domain crossings. Dead code check. Unreachable FSM state check. Timing exceptions verification.

In summary

In this article we have described some concepts related to formal verification. We have also seen how they are different from the traditional verification method of simulation and how this technique can be used to complement the simulation method.

The formal engine-based ABV technique has been discussed in depth and several related algorithms have also been described.

By Ashima S. Dabare

and Saurabh Verma

Ashima S. Dabare is a Senior Consulting Applications Engineer at Atrenta India Pvt., Ltd. She has a masters degree from Indian Institute of Technology, Delhi. She has rich experience in several areas of ASIC design flow including clocks, static timing analysis, design-for-test, formal technology and RTL prototyping.

Saurabh Verma is a Senior Manager at Atrenta India Pvt., Ltd. He has a bachelors degree from Indian Institute of Technology, Kanpur. He has rich experience in the area of formal technology, rule-based design verification, clocks, synthesis and optimization.

References

1.  Matthew W.Moskewicz, Concor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik, "Chaff: Engineering an Efficient SAT solver", EE Times August 28, 2006. DAC, 2001.
2.  L. Zhang, C. Madigan, M. Moskewicz and S. Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver", Proceedings of International Conference on Computer Aided Design (ICCAD2001).
3.  Aarti Gupta, Malay Ganai, Zijiang Yang, Pranav Ashar, Iterative Abstraction using SAT-based BMC with Proof Analysis, International Conference on Computer Aided Design – 2003.
4 - A. Kuehlmann, M. Ganai, and V. Paruthi, "Circuit-based Boolean Reasoning," in Proceedings of Design Automation Conference, 2001.