Method for optimizing integrated circuit device design and service

FIELD AND BACKGROUND OF INVENTION

This invention relates to integrated circuit design techniques.

The design of integrated circuit devices conventionally uses hardware description languages (HDLs) to describe circuits (herein also sometimes called “systems”) at various levels of abstraction. As a circuit design evolves, designers and verification engineers (whose job it is to assure that the design functions appropriately) conduct analysis of the device being designed to evaluate the quality of the design and to hopefully find and eliminate any inadequacies potentially leading to future problems such as impossibility or inaccuracy in performance of the device.

One problem encountered in such analysis is referred to as a “state explosion”, which occurs when an input to the design, intended to permit analysis of the response of the device to a particular input, generates such a large number of possible output or intermediate states as to overrun any memory used in supporting the analysis.

Reachability analysis plays a central role in formal verification of sequential circuits. One of the state-of-the-art approaches for reachability analysis and formal verification of circuits modeled as Finite State Machines (FSMs) exploits symbolic computations based on Binary Decision Diagrams (BDDs). However, the known state explosion problem may cause large intermediate BDD sizes during the exploration of the state space of a system. The conventional breadth-first search (BFS) strategy, used in most implicit model checking algorithms, is the main culprit. Others have approached this problem by devising techniques that simplify the system model employed during BFS.

Some recent work in avoiding the state explosion problem during one known analysis procedure, breadth-first symbolic traversal based on Binary Decision Diagrams (BDDs), applies hints to constrain the transition relation of the system to be verified. Hints are expressed as constraints on the primary inputs and states of a circuit modeled as a Finite State Machine (FSM) and can often be found with the help of simple heuristics by someone who understands the circuit well enough to devise simulation stimuli or verification properties for it. However, the ease of finding good hints is limited by the size and complexity of the design, and extending their applicability to larger designs is a key issue.

In one such proposal, “hints” are used to guide the exploration of the state space. In that proposal, hints are classified into those that depend on the invariants being checked (proving properties that should hold in all reachable states of a system) and those that capture knowledge of the design. Hints are applied by constraining the transition relation of the system; the constrained traversal of the state space proceeds much faster than the unconstrained system (original transition relation). This method obtained orders-of-magnitude reductions in time and space requirements during the exploration of the state space. Hints can often be found by someone who understands the design well enough to devise simulation stimuli or verification properties for it. However, in large complex designs, identifying good hints can be a labor-intensive process requiring many attempts, and in most cases does not avoid the state space explosion problem. Acceptance of this method by designers and verification engineers will certainly benefit from a more efficient technique to devise good hints from a system being verified.

SUMMARY OF THE INVENTION

Having in mind the field and problems identified above, one purpose of this invention is to facilitate improved analysis of integrated circuit device design. In realizing this purpose of this invention, the state explosion problem is preempted by constructing systems small enough to make automatic checking tractable, yet large enough to capture the information relevant to the property being checked—reachability in this case. The method here disclosed exploits these observations and can be summarized as follows: first, the original program is partitioned into subprograms representing valid computational paths; second, each subprogram is refined when cyclic dependencies are found to exist between the variables; third, computational paths whose over-approximated reachable states are found to be contained in another computational path are merged; and finally, the remaining subprograms conjoined decision conditions become candidates for hints.

BRIEF DESCRIPTION OF DRAWINGS

Some of the purposes of the invention having been stated, others will appear as the description proceeds, when taken in connection with the accompanying drawings, in which:

<figref idref="DRAWINGS">FIG. 1</figref> is a schematic illustration of the steps of a method in accordance with this invention; and

<figref idref="DRAWINGS">FIG. 2</figref> is an illustrative representation of BDDs; and

<figref idref="DRAWINGS">FIGS. 3–7</figref> are flowcharts illustrating the steps of methods in exemplary embodiments of the invention.

DETAILED DESCRIPTION OF INVENTION

While the present invention will be described more fully hereinafter with reference to the accompanying drawings, in which a preferred embodiment of the present invention is shown, it is to be understood at the outset of the description which follows that persons of skill in the appropriate arts may modify the invention here described while still achieving the favorable results of the invention. Accordingly, the description which follows is to be understood as being a broad, teaching disclosure directed to persons of skill in the appropriate arts, and not as limiting upon the present invention. In particular, while the context for this disclosure is the design of integrated circuit devices, it is known that the “state explosion” problem here addressed is also found in software design and believed that the techniques and method here described will find usefulness in such applicatins.

The program analysis techniques employed to accomplish the objective outlined above are program parsing or slicing to abstract subprograms from the original program text, and abstract interpretation to obtain the over-approximate reachable states and relevant properties for each subprogram. Additionally, the program dependence graph (PDG) is the intermediate form of choice for its rich set of supporting algorithms and efficient representation of control and data dependencies of program operations. The steps of such a method are illustrated in <figref idref="DRAWINGS">FIG. 1</figref>.

Analysis done on programs using this technique is achieved at a higher level of abstraction (program text) thus circumventing the time-space complexity issues that plague BDD-based formal verification methods. This has been validated using a subset of Verilog (behavioral Verilog), however, it is not restricted to this class of languages. It can be easily extended to any simple imperative language.

Hardware description languages (HDLs) like Verilog and VHDL, are used by hardware developers to describe circuits at various levels of abstraction (e.g., RTL, behavioral). HDL programs are translated into Finite State Machines (FSMs) to do reachability analysis. While the technique here described has been validated using behavioral Verilog, it will here be explained using the much simpler imperative While language of Nielson et al, <i>Principles of Program Analysis</i>, Springer-Verlag, Berlin, 1999. The syntax of the While language is represented below. A single entry and exit element are assumed for each well-formed program. &lt;br /&gt;<i>AEXP::=n</i>|var|<i>a</i>1<i>+a</i>2<i>|a</i>1<i>−a</i>2&lt;br /&gt;<i>BEXP::=</i>true|false|<i>a</i>1<i>=a</i>2<i>|a</i>1<i>&lt;a</i>2<i>|a</i>1<i>≦a</i>2<i>|a</i>1<i>&gt;a</i>2<i>|a</i>1 <i>≧a</i>2<i>|−b|b</i>1<img file="US7246331B2_D0001.tif" /><i>b</i>2&lt;br /&gt;<i>S</i>::=var:<i>=a|S</i>₁<i>; S</i>₂|read <i>x</i>

if b then S₁else S₂|b do S|skip

What is here used is a structural operational semantics for While as defined in the Neilson citation above. The meaning of a program P is defined as the final state, where state σ is a mapping from variables to values (integers), that can be reached after a number of transitions. Each transition has the form (S, σ)→ρ where ρ is either an intermediate state (S′, σ′) or the final state σ′. The rules for the transition are as follows: <ul id="ul0001" list-style="none"><li id="ul0001-0001" num="0000"><ul id="ul0002" list-style="none"><li id="ul0002-0001" num="0018">1. The var:=a rule updates the state with the value of the right-hand side.</li><li id="ul0002-0002" num="0019">2. The if . . . rule selects the true or false alternative, depending on the value of the condition without changing the value of state (S₁, σ) if true, or (S₂, σ) otherwise.</li><li id="ul0002-0003" num="0020">3. The while . . . rule repeats the statement S until the condition b is false, when it terminates with a skip statement ((if b then (S; while b do S) else skip, σ))</li><li id="ul0002-0004" num="0021">4. The S₁;S₂sequence rules: one, when the first statement S₁in a sequence goes to an intermediate statement and state (S₁′;S₂, σ′ (which is the case for the if . . . , while . . . , S₁;S₂); two, when the first statement terminates immediately (S₂, σ′) (which is the case for the var:=a and skip).</li><li id="ul0002-0005" num="0022">5. The skip rule does nothing—no change to state.</li></ul></li></ul>

Given a set of hints τ₁, τ₂, . . . τ_k(where each τ is a transition relation obtained by constraining the inputs or state variables of the model) the computation of the reachable states can be decomposed into the computation of a sequence of fix points—one for each hint. If hints are chosen properly, the computation of least fix points can be substantially sped up. If small transition systems result for each τ, reachability analysis may proceed further compared to computing the model fix point directly, and in some cases go to completion by avoiding the memory explosion problem. Intuitively, it is easy to reason about the benefits afforded to invariant checking from these results.

The present invention proposes that, given a sequence of monotonic functionals τ₁, τ₂, . . . τ_ksuch that τ₁≦τ_kfor 0&lt;i&lt;k, the sequence ρ₁, ρ₂, . . . , ρ_kof least fix points defined by &lt;br /&gt;ρ₀=0&lt;br /&gt;ρ_i<i>=μX.ρ</i>_i−1<i>Vτ</i>_i(<i>X</i>), 0<i>&lt;i≦k</i>&lt;br /&gt; monotonically converges to ρ=μX.τ_k(X); that is, ρ₀≦ρ₁≦ . . . ≦ρ_k=ρ

The traditional BFS reachability analysis algorithm can be modified to take advantage of hints: first, each hint, in order, is used to constrain the original transition relation, the algorithm is allowed to run normally until all reachable states are reached. The frontier set for each run is either the initial states, for the first hint, or the reached states from the previous run; finally, the original transition relation is restored and runs to completion or is terminated early due to time-space exhaustion. Its frontier set is the set of reachable states produced by the last hint.

Many program analysis techniques work on graphs derived from the program text. Among these, the Control Flow Graph (CFG) is a directed graph that represents the flow of control of a program. Each node represents an assignment or branching statement S_iin a program P. Each directed arc represents flow of control from one node to another. A CFG can be extracted in a single pass traversal over a program. A CFG would be constructed for each Verilog “always” block or each “procedure” in a imperative language. The CFG is the primary data structure and there exist a plethora of efficient algorithms to do graph-based operations (e.g., searches). Preparation of a CFG as a step in the methods of this invention is indicated in <figref idref="DRAWINGS">FIG. 1</figref>.

A control flow graph CFG of a program P with statements S is a directed graph G=(V, E), where:

V=S ∪ {exit,entry,junction} is a finite set of nodes, where

{entry, exit, junction} are distinguished entry, exit, and junction nodes, respectively, and

E⊂V×V is a control flow relation, whose elements are directed edges.

Intuitively, edges are constructed in the normal way from statement S₁to S₂by tracing the sequential execution flow of a program. Generally, edges E represent the transfer of control between statements S.

A path p in a CFG is a sequence of nodes v₁, v₂, . . . V_nsuch that n≧0 and (v_i, v_i+1)∈ E for i=1, 2, . . . , n−1.

Control dependence represents the effect of conditional branch statements on the behavior of programs. Given any two statements S₁and S₂in P, statement S₂is control-dependent on S₁if S₁is a conditional branch statement and the control structure of P potentially allows S₁to decide whether S₂will be executed. Control dependence can be defined strictly in terms of a CFG.

S₁is postdominated by S₂in a CFG if all paths from S₁to exit include S₂.

S₂is control dependent on S₁if and only if: <ul id="ul0003" list-style="none"><li id="ul0003-0001" num="0000"><ul id="ul0004" list-style="none"><li id="ul0004-0001" num="0035">1. There exists a path p from S₁to S₂and the path is non-null, such that S₂postdominates every node along the path, and</li><li id="ul0004-0002" num="0036">2. S₁is not postdominated by S₂.</li></ul></li></ul>

If S₂is control dependent on S₁in a CFG, then S₁must have two outgoing edges. Following one of the edges always leads to S₂, and using the other edge there is a path to exit that bypasses S₂. A control dependent edge can be added to the CFG to show the dependence relation. The resulting CFG augmented with the control dependence information is referred to as G_cd=(V,E∪E_cd), where E_cdis the set of control dependence edges. Control dependence is an important concept for it is needed to explain the meaning of a static program slice. A control and data dependence analysis is indicated in <figref idref="DRAWINGS">FIG. 1</figref> between the generation of a CFG and the generation of a PDG.

Attention now turns to a discussion of different types of dependence between statements S in a CFG. Given any two statements S₁and S₂, one or more of the following data dependence relations may hold between them: <ul id="ul0005" list-style="none"><li id="ul0005-0001" num="0000"><ul id="ul0006" list-style="none"><li id="ul0006-0001" num="0039">data dependence representing an assignment of a variable followed by a read access (use) of the same variable (without any intervening assignment of the same variable);</li><li id="ul0006-0002" num="0040">output dependence representing an assignment to a variable by another assignment to the same variable; and antidependence representing a read access (use) of a variable followed by an assignment of the same variable. Only data dependences between statements are considered in this discussion. OUT(S_i) may be the left-hand side variable of S_iand IN(S_i) may be the set of right-hand side variables of S_i, such that for any two statements S₁and S₂in a CFG, the data dependence is defined as follows:</li></ul></li></ul>

S₂is data dependent on S₁if and only if: <ul id="ul0007" list-style="none"><li id="ul0007-0001" num="0000"><ul id="ul0008" list-style="none"><li id="ul0008-0001" num="0042">1. ∃x εIN(S₂).x=OUT(S₁); and</li><li id="ul0008-0002" num="0043">2. the value x in S₁is used to compute the value of the left-hand side of S₂.</li></ul></li></ul>

The resulting CFG augmented with the data dependence information is referred to as G_dd=(V, E ∪ _Edd.). Data dependence information is used to identify strongly connected components (SCCs) that may exist for a trace of the execution flow of a program.

A Program Dependence Graph (PDG) derived from the program text is a lossless transformation of the original program. It is possible to go back and forth from one to the other. The PDG is used as an intermediate representation. The PDG, which represents significant information regarding the control and data dependencies of a program, can be defined in terms of the CFG; PDG=(V, E ∪ E_cd∪E_dd.

A goal of this invention is to statically (and cheaply) determine pertinent information of a program that would otherwise be ascertained during run-time. More specifically, it is desired to calculate the run-time behavior of a program without having to run it on all input data, and while guaranteeing termination of the analysis. Abstract interpretation provides the necessary framework in which the operational semantics of a program is defined by a transition relation η over a set of program states σ. This framework aims at computing safe approximations of fixed points of continuous functions over complete lattices. From the usual CFG operational semantics, a collecting semantics is derived automatically by attaching to each program point or CFG edge a set of contexts (states) that flow to that point during execution. The collecting semantics summarizes real run-time behavior, whereas abstract semantics is to compute properties for the program points that describe the concrete context sets. The abstract semantics does so by executing the CFG with abstract values that represent context properties.

Cousot and Cousot, in an article published in <i>Proceedings of the ACM Symposium on the Principles of Programming Languages, </i>1977, introduced a standard lattice of integer intervals as an abstract domain for data-flow analysis of programs with variables assuming integer values.

Abstract domain/of integer intervals may be defined as: &lt;br /&gt;<i>I={[a, b]|a, bεZ, a≦b}∪{[a, +∞</i>)|<i>a ε Z}∪{</i>(−∞, <i>b]|bεZ}∪{</i>(−∞, +∞)}∪{⊥}&lt;br /&gt; where the ordering ≦ is the natural ordering on the integers.

The ordering relation ≦_Ion I is defined by the following rules: <ul id="ul0009" list-style="none"><li id="ul0009-0001" num="0000"><ul id="ul0010" list-style="none"><li id="ul0010-0001" num="0049">1. for any x ε I, ⊥≦_Ix≦_I(−∞, +∞), <img file="US7246331B2_D0002.tif" /></li><li id="ul0010-0002" num="0050">2. for any a, b, c, d ε Z, [a, b]≦_I[c, d]<img file="US7246331B2_D0003.tif" /> c≦a, <img file="US7246331B2_D0004.tif" /> b≦d,</li><li id="ul0010-0003" num="0051">3. for any b, d ε Z, (−∞, b]≦_I(−∞, d]<img file="US7246331B2_D0005.tif" /> b,</li><li id="ul0010-0004" num="0052">4. for any a, b, d εZ, [a, b]≦_I(−∞, d]<img file="US7246331B2_D0006.tif" /> b≦d,</li><li id="ul0010-0005" num="0053">5. for any a, c ε Z, [a, +∞)≦_I[c, +∞)<img file="US7246331B2_D0007.tif" /> c≦a,</li><li id="ul0010-0006" num="0054">6. for any a, b, c ε Z, [a, b]≦_I[c, +∞)<img file="US7246331B2_D0008.tif" /> c≦a. &lt;br /&gt; (I, ≦_I) is a complete lattice that enjoys a Galois insertion with (P (Z), <u style="single">⊂</u>), which is determined by the following mapping: </li></ul></li></ul>

<maths id="MATH-US-00001" num="00001"><math overflow="scroll"><mtable><mtr><mtd><mrow><mrow><msub><mi>α</mi><mi>I</mi></msub><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow><mo>=</mo><mrow><mo>{</mo><mtable><mtr><mtd><mrow><mo>[</mo><mrow><mi>a</mi><mo>,</mo><mi>b</mi></mrow><mo>]</mo></mrow></mtd><mtd><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mi>min</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow></mrow><mo>=</mo><mrow><mrow><mi>a</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>and</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mi>max</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow></mrow><mo>=</mo><mi>b</mi></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mo>(</mo><mrow><mrow><mo>-</mo><mi>∞</mi></mrow><mo>,</mo><mi>b</mi></mrow><mo>]</mo></mrow></mtd><mtd><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mo>∄</mo><mrow><mrow><mi>min</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>and</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mi>max</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow></mrow></mrow></mrow><mo>=</mo><mi>b</mi></mrow></mtd></mtr><mtr><mtd><mrow><mo>[</mo><mrow><mi>a</mi><mo>,</mo><mrow><mo>+</mo><mi>∞</mi></mrow></mrow><mo>)</mo></mrow></mtd><mtd><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mi>min</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow></mrow><mo>=</mo><mrow><mi>a</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>and</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mo>∄</mo><mrow><mi>max</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow></mrow></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mo>(</mo><mrow><mrow><mo>-</mo><mi>∞</mi></mrow><mo>,</mo><mrow><mo>+</mo><mi>∞</mi></mrow></mrow><mo>)</mo></mrow></mtd><mtd><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mo>∄</mo><mrow><mrow><mi>min</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>and</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mrow><mo>∄</mo><mrow><mi>max</mi><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow></mrow></mrow></mrow></mrow></mtd></mtr></mtable></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mrow><msub><mi>γ</mi><mi>I</mi></msub><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow><mo>=</mo><mrow><mo>{</mo><mtable><mtr><mtd><mrow><mo>{</mo><mrow><mrow><mi>z</mi><mo>∈</mo><mi>Z</mi></mrow><mo>|</mo><mrow><mi>a</mi><mo>≤</mo><mi>z</mi><mo>≤</mo><mi>b</mi></mrow></mrow><mo>}</mo></mrow></mtd><mtd><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>x</mi></mrow><mo>=</mo><mrow><mo>[</mo><mrow><mi>a</mi><mo>,</mo><mi>b</mi></mrow><mo>]</mo></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mo>{</mo><mrow><mrow><mi>z</mi><mo>∈</mo><mi>Z</mi></mrow><mo>|</mo><mrow><mi>z</mi><mo>≤</mo><mi>b</mi></mrow></mrow><mo>}</mo></mrow></mtd><mtd><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>x</mi></mrow><mo>=</mo><mrow><mo>(</mo><mrow><mrow><mo>-</mo><mi>∞</mi></mrow><mo>,</mo><mi>b</mi></mrow><mo>]</mo></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mo>{</mo><mrow><mrow><mi>z</mi><mo>∈</mo><mi>Z</mi></mrow><mo>|</mo><mrow><mi>a</mi><mo>≤</mo><mi>z</mi></mrow></mrow><mo>}</mo></mrow></mtd><mtd><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>x</mi></mrow><mo>=</mo><mrow><mo>[</mo><mrow><mi>a</mi><mo>,</mo><mrow><mo>+</mo><mi>∞</mi></mrow></mrow><mo>)</mo></mrow></mrow></mtd></mtr><mtr><mtd><mi>Z</mi></mtd><mtd><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>x</mi></mrow><mo>=</mo><mrow><mo>(</mo><mrow><mrow><mo>-</mo><mi>∞</mi></mrow><mo>,</mo><mrow><mo>+</mo><mi>∞</mi></mrow></mrow><mo>)</mo></mrow></mrow></mtd></mtr></mtable></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mrow><msub><mi>β</mi><mi>I</mi></msub><mo>⁡</mo><mrow><mo>(</mo><mi>X</mi><mo>)</mo></mrow></mrow><mo>=</mo><mrow><mo>{</mo><mtable><mtr><mtd><mrow><mrow><mo>⊥</mo><mrow><msub><mi>β</mi><mi>I</mi></msub><mo>⁢</mo><mi>x</mi></mrow></mrow><mo>=</mo><mi>x</mi></mrow></mtd></mtr><mtr><mtd><mrow><mrow><mrow><mi>x</mi><mo>⁢</mo><mstyle><mspace width="0.3em" height="0.3ex" /></mstyle><mo>⁢</mo><msub><mi>β</mi><mi>I</mi></msub></mrow><mo>⊥</mo></mrow><mo>=</mo><mi>x</mi></mrow></mtd></mtr><mtr><mtd><mtable><mtr><mtd><mrow><mrow><mrow><mo>[</mo><mrow><msub><mi>a</mi><mn>1</mn></msub><mo>,</mo><msub><mi>b</mi><mn>1</mn></msub></mrow><mo>]</mo></mrow><mo>⁢</mo><mstyle><mspace width="0.3em" height="0.3ex" /></mstyle><mo>⁢</mo><mrow><msub><mi>β</mi><mi>I</mi></msub><mo>⁡</mo><mrow><mo>[</mo><mrow><msub><mi>a</mi><mn>2</mn></msub><mo>,</mo><msub><mi>b</mi><mn>2</mn></msub></mrow><mo>]</mo></mrow></mrow></mrow><mo>=</mo><mrow><mo>[</mo><mrow><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><msub><mi>a</mi><mn>2</mn></msub></mrow><mo>&lt;</mo><mrow><msub><mi>a</mi><mn>1</mn></msub><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>then</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mstyle><mtext>-</mtext></mstyle><mo>⁢</mo><mi>∞</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>else</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><msub><mi>a</mi><mn>1</mn></msub></mrow></mrow><mo>,</mo></mrow></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mstyle><mspace width="12.5em" height="12.5ex" /></mstyle><mo>⁢</mo><mrow><mrow><mi>if</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><msub><mi>b</mi><mn>2</mn></msub></mrow><mo>&gt;</mo><mrow><msub><mi>b</mi><mn>1</mn></msub><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>then</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mstyle><mtext>+</mtext></mstyle><mo>⁢</mo><mi>∞</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><mi>else</mi><mo>⁢</mo><mstyle><mspace width="0.8em" height="0.8ex" /></mstyle><mo>⁢</mo><msub><mi>b</mi><mn>1</mn></msub></mrow></mrow><mo>]</mo></mrow></mtd></mtr></mtable></mtd></mtr></mtable></mrow></mrow></mtd></mtr></mtable></math></maths>

If Z and I are posets, and γ_Iand α_Iare monotonic functions such that ∀ z ε Z.z≦_Iγ_I(α_I(z)) and ∀ i ε I.α_Iγ_I(i))=i, then the quadruple (γ_I, I, Z, α_I) is a Galois insertion.

The fix point computations for the interval lattice I may in theory require an infinite number of iterations. A speedup technique has been proposed that uses the widening operator β_Ito transform infinite iterative computations to finite but approximated ones.

The hints generated to help symbolic traversal of a model graph should select subsets of transitions that allow reachability analysis to visit sets of states with many elements and compact representations. Since these representations are usually Binary Decision Diagrams (BDD), it may be said simply that an objective is to have many states with small BDDs. When a model has several major modes of operation, for instance it can execute a set of instructions, enabling one mode at the time is often effective in keeping the BDD sizes under control. The approach of this invention to producing hints automatically is based on identifying the different modes of operation from the Control Flow Graph (CFG) of the model, and prioritizing them according to their dependencies and their promise to reduce time and memory requirements. The process can be divided in three major phases (see <figref idref="DRAWINGS">FIG. 1</figref>):

From the program text a CFG is extracted and from it a reduced program dependency graph (PDG);

From the CFG a list of candidate subprograms is compiled; and

Using the PDG, candidates are sorted according to their dependencies and usefulness. Hints are generated from the best candidates.

These three phases will now be described in more detail.

The program that defines the model to be analyzed is translated into a CFG, which is augmented with data dependency information to produce a PDG. Since the analysis is conservative, some data dependency arcs in the PDG are false, that is, do not correspond to real data dependencies in the program. Since more data dependency arcs result in fewer degrees of freedom for the prioritization of modes of operation, it is desirable to remove as many false arcs as possible, without incurring excessive costs in the process. Each data dependency arc is tested in turn to determine whether the definition at the tail of the arc can actually reach the usage at its head by augmenting the program with token variables that are set to specific values when assignments to the variables of interest occur. The program slice corresponding to the token variable of the usage variable is extracted from the PDG. The check whether the definition can reach the usage is thus translated into the check for an invariant on the token variable of the usage variable.

Specifically, suppose that the dependency of use S₁:x:=v₁from definition S₂:y:=x is investigated. Two token variables t₁and t₂are added to the program by making the following changes.

Assignments t₁:=0 and t₂:=0 are added to the beginning of the program.

S₁is changed to x:=v₁; t₁:=1.

Every other assignment to x:=v is changed to x:=v; t₁:=0.

S₂is changed to y:=x; t₁:=t₂.

If in the program slice for t₂no state is reachable in which t₂=1, then the data dependency arc from S₁to S₂is removed. Note that we are only interested in direct dependencies. For instance, consider S₁:x:=2, S₂: y:=x, and S₃: x:=x+1. If S₃is always executed between S₁and S₂, the dependency arc between S₂and S₁is removed. However, the dependencies of S₃on S₁, and of S₂on S₃imply, by transitivity, the one of S₂on S₁.

Though program parsing or slicing may greatly reduce the cost of checking the t₂=0 invariant relative to reachability analysis of the full model, this is not always the case; hence, each model checking run is allotted a short time to complete. If it does not finish, a less accurate, but less expensive test is applied. The augmented program slice is analyzed with abstract interpretation. If also abstract interpretation fails to complete within the allotted time, the arc is (conservatively) retained.

The modified PDG with (some) false data dependencies removed is one of the two inputs to the final step of our procedure that outputs a list of hints. The other input is a list of subgraphs of the CFG, each corresponding to a mode of operation. The subgraphs are identified by a procedure based on the enumeration of the spanning trees of a graph such as that of <figref idref="DRAWINGS">FIG. 2</figref>. The graph obtained from the CFG by removing the back arcs is a polar graph. Since the graph is polar, there is exactly one path in each spanning tree connecting the poles of the graph. All other paths correspond to dead ends. This path is augmented with all the back arcs that connect its nodes to produce a candidate subgraph.

The enumeration of the spanning trees is augmented so as to take into account input dependencies and feasibility of paths. When a candidate subgraph is generated, the path enabling conditions are tested for joint satisfiability.

The CFG of a reasonably complex model may have many feasible spanning trees. Producing one hint from each of them would lead to too many hints, many of which would not contribute enough states to pay for themselves. Therefore, the set of candidates produced by the enumeration procedure is pared down. The selection of the best candidates is heuristic. Two criteria are currently suggested. The first favors those subgraphs with more states reached during abstract interpretation of the corresponding subprograms. The second criterion favors those subgraphs that result in smaller BDDs for the transition relations for the corresponding models. Ideally, a criterion is desired that accounts for both the number of states and the BDD sizes. However, it is difficult to estimate accurately both without going all the way to guided search. The pruning process eliminates all candidates that prove inferior according to at least one heuristic.

The final step of the procedure sorts the list of candidates using the information on data dependencies provided by the PDG. One hint is then produced from each candidate subgraph by extracting its path enabling predicate. The path enabling predicate of a path is the conjunction of the predicates of all choice nodes along the path. The order in which hints are applied may greatly influence their effectiveness. This is particularly the case when there are data dependencies between the variables occurring in different subprograms. Suppose subprograms P₁and P₂are such that variable x is assigned in P₁by an input statement, while in P₂it is assigned a constant value v. Suppose also that x is used in an assignment y:=x in P₂, and that that is the only assignment to y. Then, if the hint extracted from P₂is applied before the hint derived from P₁, all the states reached after the two hints have been applied have y=v, whereas, if the order of application is reversed, there will be reachable states for each possible value of y.

In general, there will be cyclic dependencies among subprograms. Hence, the procedure is as follows. A Subprogram Dependency Graph (SDG) is formed with one node for each subprogram. Each node of the SDG is the set of nodes in the PDG that make up the corresponding subprogram. An arc connects nodes u and v of the SDG if there exists an arc (a,b) in the PDG such that a E u and b E v. The ordering of the candidate subprograms is obtained from the SDG. In particular the strongly connected components (SCCs) of the SDG define a preorder on the subprograms: We say that u_<img file="US7246331B2_D0009.tif" /> v if there is a path from u to v in the SDG. The final order ≦ is always a refinement of this preorder in the following sense: if u_<img file="US7246331B2_D0010.tif" /> v and v not_<img file="US7246331B2_D0011.tif" /> u, then u≦v. However, an arbitrary total order that refines the preorder may not work well, if there are just a few large SCCs.

The problem of deriving a total order from the preorder defined by the the SDG is decomposed into two subproblems. The first is the one of linearizing the partial order defined by the SCC quotient graph of the SDG. The second is to find total orders for the nodes of each SCC. The total order of the subprograms results from combining the solutions of these two subproblems in the obvious way.

Any topological sort of the nodes of the SCC quotient graph would satisfy the definition of order refinement. However, different orders result in BDDs of different sizes. It is normally advantageous to keep subprograms adjacent in the order if the operate on common variables. Therefore, to sort the SCCs of the SDG a depth-first search from the source nodes of the SCC quotient graph is performed.

The sorting of the nodes of an individual SCC is based on identifying a starting node, and then enumerating the elementary circuits of the SCC. As enumerate elementary circuits are enumerated from the designated start node, nodes are added to the total order as they appear in some elementary circuit. Reliance is placed on the fact that the enumeration algorithm outputs short circuits first. Short circuits are identified with with tight interaction, and therefore those nodes that have tighter interaction with the start node are put earlier in the order. The start node is selected based on the ease with which the variables in it can be controlled via primary inputs. To see why this factor plays an important role, consider, for instance, three an assignment x:=y+z, where y depends on other variables, whereas z is read from an external input. During reachability analysis, for any value of x, and any value of z there is value of z such that x=y+z. (Assuming signed integers.) Hence, the dependency on y, while present, is neutralized by the dependency on z.

This technique attempts to efficiently and effectively identify computational paths in a program that contribute most favorably to the speed-up of symbolic traversal while keeping the intermediate BDDs small. The fact that a program can be viewed as separate subprograms, updating each program variable, is used to advantage. Dividing a program into intermingling subprograms is similar to the partitioned transition relation method. This information is helpful, but alone does not lead to significant improvement; the inter-subprogram relationships (variable dependencies) is the culprit. Partitioning the subprograms into the equivalence classes, the cyclic variable data dependencies, produces the best result. Reachability analysis is a least fix point computation over the transition system defined by the original program, so it can easily be concluded that dividing and operating on a programs individual parallel fix points would be superior. In addition, not all subprogram SCCs are equal. When a SCC is found to be dependent on the input variable(s), the SCC saturates faster and produces smaller intermediate BDDs. These SCCs are favored whenever they are found during analysis.

An expression of the steps of methods in accordance with this invention may be characterized as: <ul id="ul0011" list-style="none"><li id="ul0011-0001" num="0000"><ul id="ul0012" list-style="none"><li id="ul0012-0001" num="0081">Parse input source and create CFG;</li><li id="ul0012-0002" num="0082">Perform control and data dependence analysis on CFG;</li><li id="ul0012-0003" num="0083">Generate PDG;</li><li id="ul0012-0004" num="0084">Eliminate infeasible data dependency paths from PDG using abstract interpretation (integer interval abstract domain) if model checking of subprogram reachability property timeouts;</li><li id="ul0012-0005" num="0085">Extract data dependency SCCs from the PDG—if intractable, reduce every instance of a variable to a single instance and repeat once;</li><li id="ul0012-0006" num="0086">If previous step was successful, perform input data analysis on SCCs using abstract interpretation (simple abstract domain) or else quit.</li><li id="ul0012-0007" num="0087">Perform abstract interpretation (integer interval abstract domain) on all subprograms consisting only the variables contained in a SCCs;</li><li id="ul0012-0008" num="0088">Eliminate SCCs whose abstract interpretation results are contained in an input data dependent SCC abstract interpretation result, but add its decision predicates to the input data dependent asbtract interpretation SCC decision set; and</li><li id="ul0012-0009" num="0089">Generate hints from remaining SCCs using the decision sets of each SCC following the partial ordering on the subprogram SCCs.</li></ul></li></ul>

During the determination of hints, a goal is to retrieve pertinent information (valid paths, over-approximate reachable states, etc.) from the original program text by utilizing the smallest subset of the original program text during the analysis while achieving the same results. Program slicing allows efficient and effective achievement of this goal. Program slicing is a technique used during static program analysis to identify all statements that might affect the value of a given variable occurrence. The statements selected constitute a subprogram with respect to the variable occurrence. For a statement S_iin a PDG, the static program slice with respect to S_iis the set of statements S₁, S₂, S₃, . . . in the PDG that can reach S_ivia a path of flow or control dependence edges. The program slice for a set of statements S is simply the union of each statement S_iprogram slice. Moreover, a program slice exhibits the same behavior as the original program for the variables of interest for the same input data. Program slicing or parsing is employed during infeasible path analysis and valid computational paths to minimize the size of the original source used to verify these properties; such as, “whether or not there exists a path such that the value assigned to S₁at location x is used by S₂at location y?”.

The naive approach to determining the computational paths in a program is to generate all possible paths in the programs CFG. This would result in up to 2ⁿcomputational paths, where n is the number of directed acyclic paths in the CFG or the number of decisions in the program text. Here, the set of computational paths is limited to the paths that arise from the cyclic dependency relationship between the program variables and the partitioning of the original program over its input space. These paths represent the possible fix point computations that are active during reachability analysis. By determining these paths early the inter-computational interactions that cause the intermediate BDD explosion can be prevented. Conceptually a program may be thought of as a collection of subprograms, each computing values for some or all the program variables. Several subprograms may compute values of the same variable and overlap one another. The more complex the control structure or number of decisions, the more complex the intermingling of the subprograms. Static program slicing isolates all possible subprograms computing a particular variable and its control and data dependencies.

For a program P and its associated CFG, there exists for each path in the computation tree a corresponding path in the CFG. Many paths in the computation tree may map to the same path in the CFG and that there may exist paths in the CFG that do not correspond to computation tree paths. For example, consider a boolean predicate that, because of previous computation, always evaluates to the constant true. The computation tree would have no paths where this predicate evaluates false, but the CFG may represent both possible conditional edges emanating from the node representing the conditional predicate. Thus, the CFG approximates the computation tree by representing additional behaviors, which do not correspond to any program execution. Such spurious executions are called infeasible paths. It can be said that the CFG overestimates program behavior. In previous discussion, the naive approach to defining a program slice would entail finding all nodes whose execution could possible affect the value of a variable at some node. This over approximation introduces infeasible paths in the subprogram produced by the program slice.

Isolating the source of the fix points in a program (subprogram) is key to keeping the intermediate BDDs small. The set of program variables are not all interdependent and an ordering among the equivalence classes of the variables may be obtained by partitioning the variables. Restricting fix point computations (reachability analysis) to each partition and arranging these computations to follow the implied partial ordering will yield greater efficiency than the naive approach. More specifically, for any PDG and its associated data dependency graph, it is possible to easily extract the strongly connected components (SCCs) graph [elementaryCircuits]. The SCC graphs can be collapsed into a single node resulting in a topological sort of the partial ordering formed by these nodes. This order is used to determine the order of the final hints produced.

The input data dependency analysis performed on the final set of computational paths with cyclic dependencies is to determine whether the variables included in a SCC are input dependent. A input dependent SCC will saturate faster and produce smaller BDDs. This method favors input dependent SCCs over non-input dependent SCCs for the same variable IDs.

The technique here described has been implemented on a 400 MHz Pentium IV machine with 500 MB of RAM running Linux. The results are reported in the Table below.

<tables id="TABLE-US-00001" num="00001"><table frame="none" colsep="0" rowsep="0"><tgroup align="left" colsep="0" rowsep="0" cols="6"><colspec colname="1" colwidth="35pt" align="left" /><colspec colname="2" colwidth="21pt" align="center" /><colspec colname="3" colwidth="42pt" align="center" /><colspec colname="4" colwidth="42pt" align="center" /><colspec colname="5" colwidth="35pt" align="center" /><colspec colname="6" colwidth="42pt" align="center" /><thead><row><entry namest="1" nameend="6" align="center" rowsep="1" /></row><row>&lt;entry /&gt;&lt;entry /&gt;<entry>Reachable</entry>&lt;entry /&gt;&lt;entry /&gt;&lt;entry /&gt;</row><row><entry>Circuit</entry><entry>Ffs</entry><entry>states</entry><entry>Times</entry><entry>in</entry><entry>seconds</entry></row><row><entry namest="1" nameend="6" align="center" rowsep="1" /></row></thead><tbody valign="top"><row>&lt;entry /&gt;&lt;entry /&gt;&lt;entry /&gt;<entry>BFS</entry><entry>Manual</entry><entry>Invention</entry></row><row>&lt;entry /&gt;&lt;entry /&gt;&lt;entry /&gt;&lt;entry /&gt;<entry>Hints</entry><entry>technique</entry></row><row><entry>CRC</entry><entry>32</entry><entry>4.295e+09</entry><entry>Memory</entry><entry>0.17</entry><entry>0.17</entry></row><row>&lt;entry /&gt;&lt;entry /&gt;&lt;entry /&gt;<entry>out</entry></row><row><entry>BPB</entry><entry>36</entry><entry>6.872e+10</entry><entry>193.79</entry><entry>1.04</entry><entry>52.77</entry></row><row><entry>Rotator</entry><entry>64</entry><entry>1.845e+19</entry><entry>Memory</entry><entry>0.17</entry><entry>0.17</entry></row><row>&lt;entry /&gt;&lt;entry /&gt;&lt;entry /&gt;<entry>out</entry></row><row><entry>Vsa</entry><entry>66</entry><entry>1.625e+14</entry><entry>6974.7 </entry><entry>111.8 </entry><entry>175.34</entry></row><row><entry namest="1" nameend="6" align="center" rowsep="1" /></row></tbody></tgroup></table></tables>

Four circuits having Verilog source files and which did not require intertask support were used in the implementations. CRC computes a 32-bit cyclic redundancy code of a stream of bytes. BPB is a branch prediction buffer that predicts whether a branch should be taken depending on the correctness of the previous predictions. Rotator is a barrel shifter sandwiched between registers. Vsa is a very simple non-pipelined microprocessor that executes 12-bit instructions—ALU operations, loads, stores, conditional branch—in five stages: fetch, decode, execute, memory access, and write-back. It has four registers, with one always set to zero.

The table shows the comparison of reachability analysis with hints generated by the inventive technique against BFS runs and manual hints. Columns <b>1</b>, <b>2</b>, and <b>3</b> give the name of the circuit, number of flip-flops (state variables) and number of reachable states of the circuit. Columns <b>4</b>, <b>5</b> and <b>6</b> compare run times for reachability analysis for BFS, manual hints, and hints obtained using the technique of this invention, respectively. The circuits in this table are mid-sized, but two of these circuits—CRC and Rotator—run out of memory for BFS. The inventive and manual hints were able to provide dramatic improvements to the traversal of these circuits, enabling completion times of a few seconds. With the remaining circuits in BPB and Vsa demonstrate 1–2 orders of magnitude improvement.

In this disclosure it has been shown that state traversal guided by algorithm generated hints can substantially speed up reachability analysis. Orders-of-magnitude improvement have been obtained is several cases, and visible gains have been achieved in most experiments that have been run. The hints prescribe constraints for the input and state variables of the system. Deriving the hints requires some knowledge of the circuit organization and behavior, at the level a verification engineer needs to devise simulation stimuli or properties to be checked. Simple heuristics often allow one to find hints that are effective for both properties that fail and properties that pass.

In the drawings and specifications there has been set forth a preferred embodiment of the invention and, although specific terms are used, the description thus given uses terminology in a generic and descriptive sense only and not for purposes of limitation.