| Method for optimizing integrated circuit device design and service -> Monitor Keywords |
|
|
  Method for optimizing integrated circuit device design and serviceUSPTO Application #: 20060085782Title: Method for optimizing integrated circuit device design and service Abstract: Improved analysis and refinement of integrated circuit device design and other programs is facilitated by methods in which an original program is partitioned into subprograms representing valid computational paths; each subprogram is refined when cyclic dependencies are found to exist between the variables; 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 for program refinement. (end of abstract) Agent: International Business Machines Corporation - Tucson, AZ, US Inventor: David Ward USPTO Applicaton #: 20060085782 - Class: 716018000 (USPTO) Related Patent Categories: Data Processing: Design And Analysis Of Circuit Or Semiconductor Mask, Circuit Design, Logical Circuit Synthesizer The Patent Description & Claims data below is from USPTO Patent Application 20060085782. Brief Patent Description - Full Patent Description - Patent Application Claims
FIELD AND BACKGROUND OF INVENTION [0001] This invention relates to integrated circuit design techniques. [0002] 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. [0003] 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. [0004] 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. [0005] 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. [0006] 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 [0007] 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 [0008] 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: [0009] FIG. 1 is a schematic illustration of the steps of a method in accordance with this invention; and [0010] FIG. 2 is a illustrative representation of BDDs. DETAILED DESCRIPTION OF INVENTION [0011] 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. [0012] 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 FIG. 1. [0013] 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. [0014] 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, Principles of Program Analysis, 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. AEXP::=n|var|a1+a2|a1-a2 BEXP::=true|false|a1=a2|a1<a2|a1.ltoreq.a2|a1>a2|a1.gtoreq.a2|-b|b1- b2 S::=var:=a|S.sub.1; S.sub.2|read x if b then S.sub.1 else S.sub.2|b do S.sub.1 skip [0015] 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 .sigma. is a mapping from variables to values (integers), that can be reached after a number of transitions. Each transition has the form (S, .sigma.).fwdarw..rho. where .rho. is either an intermediate state (S', .sigma.') or the final state .sigma.'. The rules for the transition are as follows: [0016] 1. The var:=a rule updates the state with the value of the right-hand side. [0017] 2. The if . . . rule selects the true or false alternative, depending on the value of the condition without changing the value of state (S.sub.1, .sigma.) if true, or (S.sub.2, .sigma.) otherwise. [0018] 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, .sigma.)) [0019] 4. The S.sub.1;S.sub.2 sequence rules: one, when the first statement S.sub.1 in a sequence goes to an intermediate statement and state (S.sub.1';S.sub.2, .sigma.'(which is the case for the if . . . , while . . . , S.sub.1;S.sub.2); two, when the first statement terminates immediately (S.sub.2, .sigma.') (which is the case for the var:=a and skip). [0020] 5. The skip rule does nothing--no change to state. [0021] Given a set of hints .tau..sub.1, .tau..sub.2, . . . .tau..sub.k (where each .tau. 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 .tau., 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. [0022] The present invention proposes that, given a sequence of monotonic functionals .tau..sub.1, .tau..sub.2, . . . .tau..sub.k such that .tau..sub.1.ltoreq..tau..sub.k for 0<i<k, the sequence .rho..sub.1, .rho..sub.2, . . . , .rho..sub.k of least fix points defined by .rho..sub.0=0 .rho..sub.i=.mu.X..rho..sub.i-1 V.tau..sub.i(X), 0<i.ltoreq.k monotonically converges to .rho.=.mu.X..tau..sub.k(X); that is, .rho..sub.0.ltoreq..rho..sub.1.ltoreq. . . . .ltoreq..rho..sub.k=.rho. [0023] 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. [0024] 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.sub.i in 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 invetion is indicated in FIG. 1. A control flow graph CFG of a program P with statements S is a directed graph G=(V, E), where: Continue reading... Full patent description for Method for optimizing integrated circuit device design and service Brief Patent Description - Full Patent Description - Patent Application Claims Click on the above for other options relating to this Method for optimizing integrated circuit device design and service patent application. ###  How KEYWORD MONITOR works... a FREE service from FreshPatents1. Sign up (takes 30 seconds). 2. Fill in the keywords to be monitored. 3. Each week you receive an email with patent applications related to your keywords. Start now! - Receive info on patent apps like Method for optimizing integrated circuit device design and service or other areas of interest. ### Previous Patent Application: Library for computer-based tool and related system and method Next Patent Application: Multi-process display method in debugger system Industry Class: Data processing: design and analysis of circuit or semiconductor mask ### FreshPatents.com Support Thank you for viewing the Method for optimizing integrated circuit device design and service patent info. IP-related news and info Results in 3.33536 seconds Other interesting Feshpatents.com categories: Tyco , Unilever , Warner-lambert , 3m |
||
