Accelerating high-level bounded model checking

We illustrate EFSM model M of a FIFO example (implemented using a RAM) using a State Transition Graph (STG) as shown in FIG. 2( a ) where S={S 0 , . . . S 11 } I={ren,wen,fifo_in}, O={fifo_out,is_full,is_empty}, D={rptr,wptr,is_full,is_empty,RAM[10]}. The enabling functions are shown in italics and update transitions are shown in non-italics in FIG. 2( a ). For example, the transition S 2 → T23 S 3 has enabling function T 23 =(rptr==wptr−1)∥(rptr=0 && wptr==9)) and update transition {RAM[rptr]=in; is_empty=0}.

Flow Graphs

Those skilled in the art will recognize that a flow graph G(V,E,r) is a directed graph with an entry node r. A path from u to v, denoted as p(u,v), is a sequence of nodes u=s 1 , . . . s k =v such that (s 1 ,s i+1 )∈E for 1≦i≦k. We denote Path(u,v) as a set of paths between u and v, and the length of a path p∈Path(u,v), is the number of edges in the sequence.

For p x p y ∈Path(u,v)p x ≠p y , if the sequence of states in p x is different from p y ; such paths are called re-converging paths. A concatenation of paths p(t,u) and p(u,v), denoted as p(t,v)=p(t,u)⊕p(u,v), represents a path from t to v that goes through u. A node n is said to dominate node m denoted as dom(m) if every path from r to m goes through n. As such, the node r dominates every other node in the graph.

A Strongly Connected Component (SCC) (V i ,E i ), is a subgraph of G such that for all u,v∈V i , there exists a path u=s 1 , . . . s k =v such that (s j ,s j+1 )∈E i for 1≦j≦k. The SCC (V i ,E i ,r i ) is a loop with entry r i if r i dominates all the nodes in V i . An edge (u,v) is called a back-edge if v dominates u; otherwise it is called a forward-edge. Given a back-edge (u,v) a natural loop of the edge is defined as the set of nodes (including u) that can reach u without going through v.

For a given G(V,E,r), and any pair of natural loops, L 1 =(V 1 ,E 1 ,r 1 ) and L 2 =(V 2 , E 2 , r 2 ) one of the following cases holds: 1) they are disjoint i.e., V 1 ∩V 2 =φ; 2) they are disjoint but have the same entry node i.e., V 1 ∩V 2 ={r 1 }={r 2 }; or 3) one is completely nested in the other, i.e., V 1 ⊂ V 2 or V 2 ⊂ V 1 . Finally, a sink node is a node with no outgoing edge.

A flow graph G(V,E,r) is reducible if and only if E can be partitioned into disjoint set front-edge set E f and back-edge set E b such that G d (V,E f ,r) forms a direct-acyclic graph (DAG) where each v∈V can be reached from the entry node r. The reducible graph has the property that there is no jump into the middle of the loops from outside and there is only one entry node per loop. As can be appreciated, most flow graphs that occur frequently fall into the class of reducible flow graphs.

The use of structured control flow statements such as if-then-else, while-do, continue, and break produce programs whose flow graphs are always reducible. Unstructured programs due to the use of goto can cause irreducibility of the graphs. Thus focusing on a reducible graph is not a significant restriction of our method and techniques, and advantageously is in accordance with practical guidelines.

For a given EFSM <s 0 ,S,I,O,D,T>, let G=(v,E,r) be a flow graph with start vertex r, such that V=S, E={(s,t)|s→t}, and r=s 0 . The sets to(s) and from(s) represent the set of outgoing nodes and incoming nodes of a node s, respectively. A reachability analysis on a flow graph corresponds to control state reachability (CSR) analysis of the corresponding EFSM.

High-Level BMC

FIG. 1 depicts a flow diagram of accelerated high-level BMC according to an aspect of the present invention. More particularly, given an EFSM Model M and a property P, we perform a series of property preserving transformations. Next, we perform a control state reachability analysis on the transformed model. Using the reachability information obtained from the reachability analysis, we next generate novel simplification constraints on-the-fly at each unroll depth k. As will be shown, these simplification constraints are used by an expression simplifier during unrolling to reduce the formula. In addition, these constraints are used to improve the search on the translated problem. Finally, an incremental learning technique may be employed i.e., reuse of theory lemmas in high-level BMC framework.

Expression Simplifier

High-level expressions—according to the present invention—include Boolean expressions bool-expr and term expressions term-expr. Boolean expressions are used to express Boolean values as true or false, Boolean variables (bool-var), propositional connectives ( , ), relational operators (<,>,≧,≦,==) between term expressions, and uninterpreted predicates (UP). Term expressions are used to express integer values (integer-const) and real values (real-const), integer values (integer-var) and real variables (real-vars), linear arithmetic with addition (+) and multiplication (*) with integer-const and real-const, uninterpreted functions (UF), if-then-else (ITE), and read and write to model memories. To model behavior of a sequential system, we employ a next operator to express the next state behavior of the state variables.

Our high-level design description is represented in a semi-canonical form using an expression simplifier. The simplifier rewrites expressions using local and recursive transformations in order to remove structural and multi-level functionality redundant expressions, similar to simplifications proposed for Boolean logic, and also for first order logic. Our expression simplifier has a “compose” operator that can be applied to unroll a high-level transition relation and obtain on-the-fly expression simplification; thereby achieving simplification not only within each time frame but also across time frames during unrolling of the transition relation in BMC.

Incremental Learning in High-Level BMC

Learning from overlapping instances of prepositional formulas has been proposed (See, e.g., O. Strichman, “Pruning Techniques for SAT-Based Bounded Model Checking,” Proceedings of TACAS, 2001; M. Ganai and A. Aziz, “Improved SAT-Based Bounded Reachability Analysis,” Proceedings of VLSI Design Conference, 2002; and J. Whittemore, J. Kim and K. Sakallah, “SATIRE: A New Incremental Satisfiability Engine,” Proceedings of DAC, 2001) and found to be useful in Boolean SAT-based BMC (See, e.g., M. Ganai, A. Gupta, and P. Ashar, “DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems, Proceedings of TACAS, 2005; and M. Ganai, A. Gupta, and P. Ashar, “Beyond Safety: Customized SAT-based Model Checking”, Proceedings of DAC, 2005). We use incremental learning of theory lemmas across time-frames, and advantageously have found this technique to be—according to the present invention—beneficial in the context of high-level BMC.

Property-Based ESFM Reduction

According to an aspect of the present invention, our method performs slicing on ESFM with respect to variables of interest as defined by the property and obtains contributing and non-contributing states and transitions. Advantageously, slicing away behaviors (and the elements) unrelated to the specific properties can significantly reduce the model size and thereby improve the verification effort. According to the present invention, two such techniques are described namely, cone-of-influence (COI) and reduction and collapsing.

Cone-of-Influence Reduction

In performing COI reduction, we first remove all non-contributing states and their outgoing transitions. Additionally, any non-contributing transitions s→ f(x,i) t where s is a contributing state, is replaced by a transition s→ f(x,i) SINK. Furthermore, if we are concerned with the reachability of a state s∈S from a start state s 0 , then we remove the outgoing transition from s since it is non-contributing for the shortest counter-example or proof. For example, the self-loop translation S 1 →S 1 (not specifically shown in FIG. 2( a )) is non-contributing and hence is replaced by S 1 →SINK as depicted in FIG. 2( a ).

Collapsing

We define a collapsing condition as that when all states in to(s) are NOP and none of them directly appears in a reachability check. Under such a condition, we collapse all of the NOP states and merge them with s. In other words, ∀t∈to(s), (with t being NOP), we remove the transitions s→ f(x,i) t and t→ TRUE q and add a new transition s→ f(x,i) q.

Extraction: Control State Reachability (CSR)

We may now discuss extraction of high-level control-flow information of the design/program which is subsequently used to simplify the unrolled formula—which we shall describe later.

Starting from an initial state S 0 we compute control state reachability (CSR) using a breadth first search (BFS). A control state S i is one step reachable from S j if and only if there exists an enabling transition between them. At a given sequential depth d, let R(d) represent the set of control states that can be reached statically on one step from the states R(d−1) with R(0)−{S 0 }. Note that we are not computing the fixed-point diameter.

For some d, if R(d−1)≠R(d)=R(d+1), we say the CSR saturates at depth d and stop; otherwise we compute R(d) and |R(d)| i.e., size of R(d) up to the BMC bound. Note, CSR information is static information without considering the enabling functions, i.e., if a control state is not reachable from the initial state in CSR, it is definitely not reachable in the model, however, the other way is not true in general. Applying CSR on the FIFO of example 1, we obtain the set R(d) as shown in Table 1(a). Note that the saturation depth is 15, |R(15)|=|R(16)|=11 where R(15)={S 1 , S 2 , . . . S 11 }

On-The-Fly Simplification and Learning

For n control states S 1 . . . Sn we introduce n Boolean variables B S1 . . . B Sn . If we let the Boolean variable B r =TRUE if and only if configuration of M is (r,x) for some x∈V. Equivalently, B r corresponds to a predicate on the control state variable, called the PC (Program Counter) i.e., B r ≡(PC==r). Let B r d denote the Boolean variable B r at depth d during BMC unrolling.

At any unrolling depth d of high-level BMC, we apply the following on-the-fly structural and clausal (learning based) simplification on the corresponding formula. Note, these simplifications are effective for small |R(d)|. We use a procedure we call Simplify(BoolExpr e, Boolean v) which constrains a Boolean expression e to a Boolean value v, and also reduces the expressions that use e. Later, we will illustrate this with an example.

1. Unreachable Block Constraint (UBC)

∀ r∉R(d) Simplify(B r d ,0) Since the state r is not reachable at depth d, the predicate B r will evaluate to FALSE at depth d. Therefore, simplifying the formula by propagating B r =0 at depth d preserves the behavior of the design.

2. Reachable Block Constraint (RBC)

Simplify(V r∈R(d) B r d ,1) At any depth d, at least one state in R(d) is reachable.

3. Mutual Exclusion Constraint (MEC)

∀ r,i∈R(d),r≠t Simplify((B r d B t d ),1) At any depth d, at most one state in R(d) is the current state.

4. Forward Reachable Block Constraint (FRBC)

∀ r∈R(d) Simplify((B r d s∈to(r) B s d+1 ),1) At any depth d, if the current state is r i.e., B r d =TRUE then the next state must be among the to(r) set.

5. Backward Reachable Block Constraint (BRBC)

∀ r∈R(d) Simplify((B r d s∈from(r) B s d−1 ),1) At any depth d, if the current state is r i.e., B r d =TRUE, then the previous state at depth d−1 must be among the from(r) set.

Block-Specific Invariant (BSI)

∀ r∈R(d) Simplify((B r d C r d ),1) At any depth d, a given invariant C r for a given state r is valid only if r is the current state at depth d.

Importantly, certain prior attempts (See., e.g., F. Ivanic, J. Yang, M. Ganai, A. Gupta and P. Ashar, “Efficient SAT-based Bounded Model Checking for Software” Proceedings o ISOLA, 2004) added some of these constraints in the transition relation so as to include them in the formula at each unrolling. In sharp contrast, the present invention adds only the relevant constraints at any unrolling thereby reducing the overall formula size. Therefore, we would prefer a smaller set R(d) to increase the effectiveness of our simplification. Later we discuss how we transform EFSM model to reduce the set R(d).

Example 1 We may now illustrate simplification constraints at depth d=4. In particular, we consider the effect of simplification on the unrolled expression for variable is_full. The transition relation for the state variable is_full is defined as follows

next(is_full)=( B S0 ∥B S7 )?0:( B S3 )?1:is_full

The high level expression for the unrolled variable, corresponding to next(is_full) at depth 5 would be:

is_full 5 =( B S0 4 ∥B S7 4 )?0:( B S3 4 )?1:is_full 4

For the sake of brevity, we describe only the Unreachable Block Constraint. Note that at d=4 only S 4 , S 5 , S 6 , S 9 , S 10 and S 11 are reachable (See, e.g., Table 1(a)) Accordingly,

∀ r∈ {S0,S1,S2,S3,S7,S8}Simplify(B r 4 ,0)

Using this simplification, the expression for is_full 5 is mapped to an existing variable is_full 4 , thereby reducing the additional logic, i.e., is_full 5 =is_full 4 .

EFSM Transformation: Balancing Re-Convergence

As can be appreciated, the efficiency of on-the-fly simplification depends on he size of the set R(d) i.e., |R(d)|. A larger |R(d)| reduces the scope of simplification at depth d and hence the performance of high-level BMC. Re-converging paths of different lengths inside loops is one of the reasons for the saturation of reachability and inclusion of all looping control states in the set R. To improve the performance of high-level BMC further, we advantageously adopt a strategy called “Balancing Re-convergence” that transforms the original model into a “BMC friendly” model but preserves the validity of the model with respect to the property expressed in LTL\X (Linear Temporal Logic Without the next-time operator).

Strategy: Intuition

For balancing re-convergence and reducing the set R(d) and thereby improving the scope for simplification of high-level BMC, we transform an ESFM by inserting NOP states such that the lengths of the re-convergence paths are the same and control state reachability does not saturate. Reduction in R(d) in general, improves the scope of on-the-fly simplifications. Note that the additional NOP states have little effect on simplification, although they increase the total number of control states and transitions, and possibly the search depth. As NOP states do not add complexity to the transition relations of any state variables except the program variables encoding the control states, the Unreachable Block Constraint simplification at depth d is practically unaffected by inclusion of such states in R(d). Also, the Forward and Backward Block Constraint simplifications are not affected, as these additional transitions are single outgoing transitions (and therefore always enabled) from NOP states.

We define R(d)={s|s∈R(d) and s is not a NOP state}. We use max d |R − (d)| to measure the effectiveness of our strategy in improving the scope of simplification of high-level BMC. Note that the above transformation preserves LTL\X properties, as NOP states can only increase the length of traces but not the eventuality and global behavior. As the state of data variables does not change in an NOP state, the validity of atomic propositions is not affected.

For the EFSM model shown in FIG. 2( a ), paths S 2 →S 3 →S 4 and S 2 →S 4 are re-converging with different lengths. For balancing, we insert a NOP state S 2 a such that transition S 2 → ˜T23 S 4 is replaced by S 2 → ˜T23 S 2 a → TRUE S 4 . Similarly, as paths S 7 →S 8 →S 9 and S 7 →S 9 are re-converging with different lengths, we insert another NOP state S 7 a and replace the transition S 7 ˜T78 S 7 a → TRUE S 9 . The modified EFSM model M′ is shown diagrammatically in FIG. 2( b ). CSR on M′ is shown in Table 1(b). Note that at depth max d R − (d)=4. Also CSR on M′ does not saturate.

Balancing Re-Convergence without Loops

Consider the DAG, G(V,E f ,r) corresponding to the reducible flow graph G(V,E,r) with an entry node r and front-edge set E f . Let w(e) denote the weight of the edge, e=(a,b)∈E f . As we will later see, the weight of the edge (a,b) corresponds to one more than the number of NOP states that need to be inserted between nodes a and b. We define weight for a path p= S 1 . . . S k ,denoted as w(p)=Σ 1≦i≦k w(e i ) where e i =(s i ,s i+1 )∈E f . We may now define the problem as follows.

Problem 1: For a given DAG G(V,E f ,r) find a weight function w:E f →Z such that ∀p x ,p y ∈P(u,v)w(p x ), where u,v∈V. Note that if we are able to find a feasible w, then the number of NOP states introduced for an edge, e=(a,b)∈E f will be equal to w(e)−1. We say that the set P(u,v) is balanced when all the paths from u to v have equal weights, i.e., ∀p x ,p y ∈P(u,v),w(p x )=w(p y ).

Let W(u) denote the weight of the paths in the balanced set P(r,u) with W(r)=0.

Lemma 1: If P(r,v) is balanced and P(u,v)≠φ, then P(u,v) is balanced.

Proof: We may prove by contradiction, in particular Let p 1 (r,u)∈P(r,u) and assume that P(u,v) is not balanced, i.e., there exists at least two paths p 1 (u,v)∈P(u,v) and p 2 (u,v)∈P(u,v) such that w(p 1 )≠w(p 2 ). Let p 0 (u,v)∈P(u,v). The weight of the concatenated path p 0 ⊕p 2 is w(p 0 )+w(p 1 ) and that p 0 ⊕p 2 is w(p 0 )+w(p 2 ). Since w(p 1 )≠w(p 2 ), the weight of the concatenated paths are different, however since p 0 ⊕p 2 , p 0 ⊕p 2 ∈P(r,v) is balanced, we get a contradiction. Thus, P(u,v) is also balanced.

Using Lemma 1 we reformulate the problem as follows. In particular, problem 1 may be stated differently as: Given a DAG G(V,E f ,r) find a weight function w:E f →Z and w:V→Z such that P(r,v) is balanced i.e., w(p x )=w(p y )=W(v),∀p x p y ∈P(r,v).

Solution: If P(r,u) is balanced ∀u∈from(v), i.e., W(u) is computed, we can balance P(r,v) recursively as follows.

∀ u∈from(v) w ( u,v )= t−W ( u )

where t=(max u∈from(v) W(u))+1. Set W(v)=t as for any path p(r,v) through u will have weight W(u)+w(u,v)=W(u)+t−W(u)=t.

We may start with an initial set of nodes S which are sink nodes in G(V,E f ,r). Then, we recursively apply the above steps in the procedure BalancePath as shown in FIG. 3 . Termination is guaranteed as the recursive sub-procedure BalanceAux is invoked only once per node. The correctness of the algorithm may also be shown through the use of an inductive argument.

Collapsing NOP States

As previously discussed, according to the present invention we insert NOP states corresponding to the edge weights obtained after executing BalancePath. For an edge e=(u,v), we insert (w(e)−1) NOP states. As can be readily appreciated by those skilled in the art, the method of BalancePath adds/inserts a minimum number of NOP states when balancing paths. However, the inserted NOP states together with NOP states in the original FESM may generate a collapsing condition discussed earlier. In that case, we collapse the NOP states as also discussed earlier. We then re-run BalancePath as the lengths of the re-converging paths may have changed due to the collapsing. Note that the collapsing may be integrated with the procedure BalancePath thereby avoiding re-running the procedure.

Balancing Re-Convergence with Loops

Since the flow graph G(V,E,r) is reducible, we know that every loop L i =G(V i ,L i ,r i ) is a natural loop corresponding to back-edge set (b i r i )∈E b and has a single entry node r i . As can be understood, the presence of back-edges in loops and their relative skews cause re-convergence paths of different lengths, which in turn can also lead to saturation during control reachability analysis. Accordingly, we say that a loop L i is saturated at depth s when ∀v∈v i , v∈R(t) for t≧s. Given balanced Path (r i b i ) for each loop L i , we define forward loop length, C i , for loop L i as follows:

C i =W ( b i )− W ( r i )

Where W:V→Z is the weight function we obtain for each node in G(V,E f ,r) using the BalancePath procedure described earlier and shown in FIG. 3 . Observe that then entry node j; of loop L i reappears in control reachability after N i =C i +w(b i ,r i ) steps i.e., r i ∈R(d i +n i N i ) where d i N i ∈Z. We call N i the loop period of L i .

If there is only one loop, it is relatively easy to see that d i =W(r i ). However when there are multiple loops, one must account for the paths from other loops to loop L i . More particularly, if there is a path from entry node r j of some loop L j to r i , then entry r i also re-appears after N j .

We define loop clusters LC as sets of disjoint entry nodes such that for any two clusters LC x and LC y ∀s∈LC x , ∀t∈LC y , P(s,t)=P(t,s)=Φ. Note that a loop in a cluster does not affect the loop in another cluster as far as reachability is concerned. In the following problem statement, we discuss how to prevent loop saturation using suitable transformations.

Problem 2: Given a reducible flow graph G(V,E,r) with E=E f ∪E b , find w:E b →Z and N i so that loop L i is not saturated.

Solution: We define a set from(i)={j|r j =r i or Path (r j r i )≠φ}. Therefore, d i =W(r i )+Σ j∈from(i) n j N j where n j ∈Z. We define D i =min k∈from(i)∪{i} N k . It is relatively straightforward to see that a loop L i gets saturated at depth t+D i during reachability if r i ∈R(t+k) ∀k, 0≦k≦D i . This is captured by the following integer linear equations in terms of s and n j 's forgiven N j 's, N i , and W(r i ), in particular:

W ( r i )+Σ j∈from(i) n j N j +n i N i =s

W ( r i )+Σ j∈from(i) n j N j +n i N i =s+ 1

. . .

W ( r i )+Σ j∈from(i) n j N j +n i N i =s+D i −1

To prevent saturation of loop L i , we need to find N j 's and N i such that there is no feasible solution to the above equations. One strategy is to choose a weight function w:E b →Z such that the loop lengths match, i.e., N i =N j ∀j∈from(i). As can be readily appreciated, one can verify the infeasibility for this solution assuming that each loop has at least two nodes, i.e., N i ≧2.

We consider one loop cluster at a time. We define maximum loop period over all loops in the cluster (i.e., those whose entry nodes are in the cluster) N=(max i C i )+1. We assign a weight to each back-edge (b i r i ) as follows:

w ( b i r i )= N−C i ;

For each loop L i in the cluster, the entry node r i ∈R(W(r i )+nN) where n∈Z. Thus, the upper bound on |R(d)| for G(V,E,r) at any depth d>>1, |R(d)|≦Σ t max t |R i (t)|, where R i (t) is the control reachability set (including NOP states) on loop L i at depth t. Similarly, the upper bound on |R − (d)| for G(V,E,r) at any depth d>>1, is |R − (d)|≦Σ i max t |R i − (t)|, where R − (t) is the control reachability set (of only non-NOP states) on loop L i at depth t.

We now illustrate our method for balancing flow graph using an example shown in FIG. 4( a ). Let v i represent the node with index i (shown inside the circle). Note that the flow graph G(V,E,v i ) has three natural loops L 1 , L 2 and L 3 corresponding to the back-edges (v 6 ,v 3 ),(v 7 ,v 1 ), and (v 8 ,v 3 ) respectively. The corresponding entry nodes for the loops are v 3 , v 1 , and v 3 respectively. Note, they all form a cluster. The DAG G(V,E f ,v i ) corresponding to the front-edge set, E f =E−{(v 6 ,v 3 ),(v 7 ,v 1 ),(v 8 ,v 3 )} is shown in FIG. 4( b ). After executing BalancePath, we obtain edge weights, also shown in FIG. 4( b ), that balance all re-convergence paths in E f . Note that the edge with no weight shown has an implicit weight of 1. Also, shown are the W values of each node. For instance, W(v 6 )=5 denotes that all the paths in the set P(v 1 ,v 6 ) have weights equal to 5.

Next, we compute the forward loop length of each loop and the weights of the back-edges. The forward loop length of loop with back-edge (v 6 v 3 ) is W(v 6 )−W(v 3 )=3; similarly, with back-edge (v 7 v 1 ) is 6, and with back-edge (v 8 v 3 ) is 5. Thus, the value of N as defined, is 7. The weight of the back-edges (v 6 ,v 3 ), (v 7 ,v 1 ) and (v 8 ,v 3 ) are 4, 1, and 2 respectively as shown in FIG. 4( c ). For each edge with weight w, we insert w−1 nodes corresponding to NOP states as shown as un-shaded circles in the modified flow graph in FIG. 4( d ).

Reachability on the original flow graph G(V,E,v 1 ) shown in FIG. 4( a ) saturates at depth 6 with 8 nodes. The reachability on the balanced flow graph in FIG. 4( d ) does not saturate. Instead, the set of reachable nodes R(d) at depth d shows a periodic behavior with period, N=7. If we do a reachability analysis separately on each loop of the modified flow graph in FIG. 4( d ), we obtain max t |R 1 (t)|=2, max t |R 2 (t)|=2, and max t |R 3 (t)|=2. Thus the upper bound on |R(t)| is 6. Similarly, max t |R − 1 (t)=1, max t |R − 2 (t)|=1, and max t |R − 3 (t)|=1 and upper bound on max t |R − (t)| is 3. In this case max t |R − (t)|=4 and max t |R − (t)|=2. Clearly, the scope of simplification during BMC is significantly improved.

Experimental Evaluation of High-Level BMC

Our inventive method was evaluated on a public benchmark bc-1.06, a C-program for an arbitrary precision calculator language with interactive execution of statements. This program has a known array bound access bug (checked as an error-label reachability property). Using the known program verification tool F-soft, we first generated an ESFM model M with 36 control states and 24 state variables. The data path elements include 10 adders, 106 if-then-else, 52 constant multipliers, 11 inequalities, and 49 equalities. The corresponding flow graph has two loops, with 4 and 8 nodes (control states) respectively. We also used statically generated invariants to provide block specific invariants.

We have performed controlled experiments to evaluate the role of various accelerators discussed in improving the performance of high-level BMC. In doing so, we employed the difference logic solver—SLICE—in the backend. We modified the solver to support incremental learning across time frames and translated conservatively each BMC problem instance into a difference logic problem. (A precise translation would have been to a UTVPI—Unit Two Variables Per Inequality—problem). To understand the effectiveness of our methods, a conservative translation suffices as long as we do not get false negatives, which advantageously was not an issue for this example.

Table 2 shows the results of our experiments run on three EFSM models M, M′, and M″. Model M is the original model without any proposed transformations. Model M′ is the model obtained from M using the procedure described earlier namely, Balancing Re-Convergence With Loops.

Column 1 of Table 2 shows the loop sizes in each of the models for loops L 1 , and L 2 ; the number of control states (including inserted NOP states); the results of control reachability on each of the models i.e., either saturation depth or max loop period N; maximum size of the reachable set of control states overall depth R max =max d R(d); and maximum size of the reachable set of non-NOP control states overall depth R max =max d R(d).

Column 2 of Table 2 presents various learning and simplification strategies denoted as follows: A for Expression Simplification (ES), B for Incremental Learning (IL) combined with B,D for Reachable Block Constraint (RBC) combined with C,E, for Forward Reachable Block Constraint (FRBC) combined with D, F, for Backward Reachable Block Constraint (BRBC) combined with E, and G for Block Specific Invariants combined with F. Column 3 shows the number of calls (#HS) made to the high-level solver when the expression simplifier cannot reduce the problem to a tautology.

Column 4 shows the depth D reached by high-level BMC under a given time limit (“*” denotes time out). Column 5 shows the time taken (in seconds) to find the witness; TO denotes that time out occurred. Column 6 shows whether a witness was found in the given time limit—if so the witness length is equal to D.

Discussion

Note that fewer calls (#HS) made to the SMT solver directly translates into performance improvement as the expression simplifier structurally solves the remaining D-#HS SMT problems more efficiently. We now discuss the effect of various learning scheme in improving the structural simplifications. As can be seen, CSR on Model M saturates at depth 13 with 36 control states. Although Unreachable Block Constraint (UBC) allows deeper search with fewer solver calls, the simplification scope is very limited due to the large set R(d). This also prevents other simplification strategies from being useful. As shown in Column 6, none of the strategies is able to find the witness in the given time limit. When we apply the procedure BalancePath with the procedure collapsing of NOP states on Model M, we obtain a model with M′ with 34 control states with reduced loop size |L 2 |.

As can be appreciated, CSR on M′ does not saturate and has max d R(d)=4 and max d R − (d)=3. This increases the scope of simplification significantly. As shown in Column 6, all simplifications strategies C-G are able to fined the witness in the given time limit. Except for FRBC, all simplification strategies seem useful in reducing the search time; although only UBC can reduce the number of calls to the high-level solver as shown in Column 3. Block Specific invariants added on-the-fly are also found to be useful. Note, although strategy B with only incremental learning does not find the witness, it still helps to search deeper compared to strategy A.

By applying our loop balancing procedure on the model M′, we obtain a model M″ with matching loop lengths of 6 and total number of control states of 36. We added two NOP-states in the back-edge of loop L 1 to get a loop length of 6. Control reachability on M″ has max d R(d)=3 and max d R − (d)=2, further increasing the scope of simplification as indicated by a decreased number of calls to the high-level solver. Those skilled in the art will recognize that this is indicated by the reduced solve time (=19 s) using strategy F, although there is a small performance degradation with strategy G. Not surprisingly, the witness length has gone up to 205. Overall, we see progressive and cumulative improvements with various learning techniques and strategies.

Comparison with Boolean-Level BMC

To compare our inventive techniques with Boolean-level BMC, we used our state of the art Boolean-level BMC framework DiVer on a Boolean translation of the model M (with 654 latches, 6K gates) to witness the bug, and used an identical experimental setup as discussed. Note that we added high-level information such as mutual exclusion constraint and backward reachable block constraints in the transition relation beforehand. Thus, all these constraints get included in every unrolled BMC instance automatically, in sharp contrast to the method of the instant invention. The Boolean-level BMC is able to find a witness at depth 143 in 723 s. Not surprisingly, the number of instances solved by structural simplification is merely 15, while 128 calls are made to the SAT-solver. Thus a reduced scope of simplification can greatly affect the performance of BMC, further the case for synthesizing “BMC friendly” models.

Experiments with Industry Software

We also experimented on industry software written in “C” having about 17K lines of code. To perform the experimentation, we first generated an EFSM model M with 259 control states and 149 state (term) variables. The data path elements include 45 adders, 987 if-then-else, 394 constant multipliers, 53 inequalities, 501 equalities and 36 un-interpreted functions. The corresponding flow graph has 12 natural loops.

We consider reachability properties P 1 -P 6 corresponding to six control states. CSR on M saturates at depth 84. After transforming M using path and loop balancing algorithms, we obtain a model M″ with 439 control states and max loop period N=4. Using a similar experimental setup (discussed earlier), we ran high-level BMC (HBMC) for 500 s on each of P 1 -P 6 on: (I) Model M with strategy A (using only expression simplification), (II) Model M using strategy F (all simplifications), and (III) transformed Model M″ using F. We present our results in Table 3. Column 1 gives the property checked; Column 2-4 give BMC depth reached (* denotes depth at time out, TO), time taken (in sec) and whether witness was found (Y/N) respectively for combination (I). Similarly, Columns 5-7 and 8-10 present information for combinations (II) and (III) respectively. The results clearly show that combination (III) is superior to (II)

At this point, while we have discussed and described our invention using some specific examples, those skilled in the art will recognize that our teachings are not so limited. Accordingly, our invention should be only limited by the scope of the claims attached hereto.