January 16, 2012 -- In this second 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 as the traditional method of simulation proves too slow, too costly, and insufficient in terms of coverage.

Formal algorithm

A number of Satisfiability (SAT)- and Binary Decision Diagram (BDD)-based formal engines are available in the industry. In all subsequent sections, a basic SAT solver has been used as a reference to discuss the formal algorithms. Further assume that our SAT solver can verify EF(P) type of properties only, where P is a property which is a simple atomic expression.

An actual user, however, might have different types of complex properties that need to be verified. Hence, a modeling layer needs to be developed to convert those properties to the EF(P) format before passing them to the SAT solver.

Properties of the type AG(P) can be simply negated and converted to the required format as EF(!P) by the modeling layer. But this is true only when the property is a simple atomic expression.

There can be other cases where P is a temporal property or the property may have been specified using any of the standard languages such as OVL, PSL, etc., which the SAT solver cannot directly understand. In such cases, the modeling layer would create automata/additional-logic to convert it to the EF(P) kind of CTL properties. Different kinds of automata are described in literature such as AR automata, Buchi automata, etc. The additional logic added by the modeling layer can vary from simple combinational logic to very complex sequential logic.

In the case of a liveness property, there is additional complexity and the modeling layer has to first convert it to an equivalent safety property before proceeding further.

Once the property is available in the EF(P) format, it can be passed to the SAT solver along with the design. SAT engines need the following 4 inputs to begin with:

Design description. Property to be verified. Initial state of the design. Constraints, if any.

The modeling layer takes all the above inputs from the user and transforms them to a format required by SAT.

The SAT engine always tries to find a "witness" for the property EF(P) passed to it. A witness is a finite-length input sequence which eventually makes the assertion true while satisfying the given constraints throughout the path. If the SAT engine is not able to find a witness, it tries to prove that the witness can never exist. This is known as "proof."

Based on witness and proof search, the output of the SAT engine can be any one of the following:

Pass (when a witness was found). Fail (when the witness is not possible under any conditions). Undecided (when it could not find a witness, and could not guarantee that a witness is not possible).

In the case where the original design property was of the type EF(P), the Pass/Fail status from the SAT engine is directly applicable for the design property. If the original design property was of the type AG(P), however, the Pass from the SAT engine would be treated as a Fail and a witness would exist for it, and a Fail would be treated as a Pass.

Let's now describe the SAT algorithm in detail for combinatorial and sequential circuits.

Formal analysis of combinatorial circuits

First, let's describe the SAT-based formal algorithm in the case of combinatorial circuits.
Traditional SAT engines work on the Conjunctive Normal Form, also known as CNF. CNF is a mathematical representation which can be used to describe the design functionality as well as the property to be tested. Figure 1 shows the CNF of two basic gates.

Figure 1. Conjunctive Normal Form of two basic gates.

CNF of basic gates

Since CNF represents the gate's functionality, it can be set to 1, implying that it always holds true. For example, in the case of an OR gate, it can be thought of as (!a+o)(!b+o)(a+b+!o)=1.

This representation is not limited to a single gate and can be used to capture the functionality of any combinatorial logic. An example is illustrated in Figure 2.

Figure 2.

CNF of a combinatorial circuit

This CNF (CNF1) always holds true as it is just representing the design function. In other words, CNF1 can be set equal to 1.

Assume that in this design we want to verify that there is at least one input sequence which makes x=0 and y=1. This property can be represented as EF(!x & y).

The CNF for this property is added to the design CNF as shown in Figure 3.

Figure 3.

CNF of property added to design CNF

It can be seen that for the given assertion to be true, there should be at least one input sequence where the equation CNF2=1 is true.

So the task of the SAT engine from this stage is to determine a set of assignments for the 3 input signals a, b and c which can make the above equation true. If the SAT engine is able to determine one such set, it will become the witness of the property and the property will pass.

Before describing the flow of how the SAT engine achieves that, some important terms are defined here, which will be used in the SAT algorithm.

Consider the following CNF: (a+!o) (b+!o) (!a+!b+o)

Each sum in a CNF is called a clause. So the above CNF has 3 clauses. To satisfy the CNF, each clause should be true.

Each design signal is a variable. In the above CNF there are 3 variables: a, b and o.

Each term in a clause is a literal. The variable and its inverted form are considered two separate literals. In the example above, there are 6 literals: a, b, o, !a, !b, !o. For a clause to be true, at least one literal in that clause should be true.

An assignment simply means assigning a value to a variable.

An implication is the value forced on a variable due to assignment of other variables.

This happens when except one literal, all the other literals in a clause have been fixed to a value 0 (due to assignment or implication) due to which the remaining literal is forced to be 1 in order to make the clause true.

For example, in clause (a+b), the assignment of a=0, would force b to take a value 1 so that the clause can be equal to 1. This is the implication.

A conflict is the condition in which a clause becomes 0. This can happen when all the literals in a clause are forced to a value of 0 because of assignment or implication.

Consider, for example, the CNF (a+b)(a+c)(a+!b+!c). In this case, if a is assigned to 0, then to make the first 2 clauses true, b and c will have an implied value of 1. But this would cause the third clause to be forced to 0. This is a conflict.

The DPLL algorithm

The DPLL Algorithm is the key algorithm used in SAT engines and is given below:

The basic task of the DPLL algorithm is to find a set of variable assignments which can make the given CNF true.

Figure 4. Variable assignment and clause traversal by the SAT engine.

Simplified DPLL algorithm

Referring to the Figure 4 above, the SAT engine begins with assignment of variables. Variables are assigned one by one and are pushed to an assignment stack. Each assignment is followed by a traversal of all the clauses to find out if there are any implications.

If no implications are found, the engine checks if all the variables have been assigned or if all clauses have become true in which case a satisfiable assignment (or witness) is obtained. In this case, the engine returns the status SATISFIABLE, else it goes back to the variable assignment.

If some implications are found, they get propagated and the engine checks for the presence of a conflict. If a conflict is found, the engine tries to resolve the conflict by swapping the assignment of the last assigned variable. If the conflict still exists, it pops out the last assigned variable from the stack and reverses the assignment of the next available variable on the stack. If, in this process the stack becomes empty, it is a proof that there are no satisfiable assignments.

In other words, it is proved that the conflict cannot be resolved with any possible set of assignments. In this case it returns a NOT SATISFIABLE status, also known as Proof. If at any stage, by reversing the assignment of any variable, there is no further conflict, the conflict gets resolved.

If there was no conflict or the conflict got resolved, it goes back to clause traversal and propagates each implication similar to variable assignment and continues in the loop, until a SATISFIABLE or NOT SATISFIABLE state is reached. In some cases, it may not be able to reach a conclusion due to memory and/or performance issues, in which case the status is INDETERMINATE.

It is interesting to note that the NOT_SATISFIABLE status can be obtained without actually assigning all the variables. This is the beauty of SAT for finding Proofs. The order of variable assignments is the key to the SAT algorithm. The earlier a conflict can be found, the better it is. Certain heuristics are used to determine the order of variable assignments so that a conclusive state can be reached quickly, such as VSIDS, DLIS, Random.

There are other techniques, also, which improve the convergence of the SAT algorithm. For example, schemes such as "Two watched literals" save the clause traversal time. "Conflict clauses" and "Learned Clauses" can be added to CNFs to achieve quick design convergence.

To summarize: for combinatorial circuits, if a valid assignment is found, it is a one-cycle witness and the property holds true or passes, else, if it returns NOT_SATISFIABLE, then it is proved that the property will never hold true, and hence it fails.

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.