Data processing: structural design – modeling – simulation – and em – Modeling by mathematical expression
Reexamination Certificate
1999-07-02
2003-07-08
Broda, Samuel (Department: 2123)
Data processing: structural design, modeling, simulation, and em
Modeling by mathematical expression
C703S014000, C703S015000, C703S016000, C716S030000, C716S030000, C716S030000, C716S030000
Reexamination Certificate
active
06591231
ABSTRACT:
BACKGROUND OF THE INVENTION
This invention relates to computer aided circuit design.
A circuit may be described as a set of definitions, with each definition specifying a gate of the circuit. For most circuits, the induced dependency graph of such a set of definitions is acyclic. That is, the circuit contains no feedback loops (without clocked delay elements) which may cause uncertainty in the state that the system must take on or, indeed, may cause the circuit to not settle to any stable state. In reviewing the set of definitions that together define a circuit, an individual definition or (more typically) a collection of definitions may be found to be semantically cyclic, or syntactically cyclic. A definition is syntactically cyclic when a variable p is expressed in terms of itself, or in terms of at least one other variable, q, that is effectively expressed in terms of p. A semantically cyclic definition is one that, for at least one valuation (e.g. with a specific valuation of one or more external variables of the circuit), a syntactically acyclic condition does not exist.
Syntactic cyclic definitions occur in many contexts in digital designs. S. Malik in “Analysis of cyclic combinational circuits”,
IEEE Transactions on Computer
-
Aided Design,
1994, points out that it is often desirable to re-use functional units by connecting them in cyclic fashion through a routing mechanism, and L. Stok in “False loops through resource sharing”, in
International Conference on Computer
-
Aided Design,
1992, notes that such definitions often arise in the output of synthesis programs. In these cases, the intention is that the routing mechanisms can be controlled through external inputs, so that any “semantically” cyclic paths are broken for each valuation of the external “free” inputs and clocked delay elements (such as clocked latches).
Semantically cyclic definitions may, for example, occur inadvertently in systems composed of several Mealy machines, from feedback connections between the combinational inputs and outputs.
Verification systems that accept semantically cyclic definitions obviously run the risk of certifying systems that have the unacceptable behavior associated with a cyclic condition. On the other hand, verification systems that prohibit syntactically cyclic definitions reject circuit definitions that might be certified by formal verification as being free from cyclic conditions. Most current design and verification systems either prohibit all syntactically cyclic definitions, or accept only some of the semantically acyclic definitions that could be accepted.
The Esterel compiler appears to be the only known existing system that analyzes definitions for semantic cyclicity, using the notion of “constructivity” proposed by Berry,
The Constrictive Semantics of Esterel,
Draft book, available at ftp://ftp-sop.inria.fr/meije/esterel/papers/constructiveness.ps.gz, 1995, which considers a circuit to be semantically acyclic iff for every external input, a unique value can be derived for each internal wire by a series of inferences on the definition of the circuit (a more precise statement is given below). T. Shiple, “Formal Analysis of Synchronous Circuits”,
PhD dissertation,
University of California, Berkeley, 1996, shows that constructive definitions are precisely those that are well-behaved electrically, for any assignment of delay values, in the up-unbounded inertial delay model defined in by J. A. Brzozowski and C-J. H. Seger in “Asynchronous Circuits”, Springer Verlag, 1994.
The work most related to this disclosure is described in the aforementioned Berry article and the aforementioned Shiple dissertation. Berry proposed the original operational formulation of constructivity (Constructivity) and the computational formulation (Constructivity-FIX), based on work by Malik's aforementioned article. These definitions are based on computational processes—one would prefer a non-computational definition of the concept of “semantic acyclicity”. See also T. Shiple, G. Berry and H. Touati, “Constructive analysis of cyclic circuits”, in
European Design and Test Conference,
1996. The above references employ symbolic, fixpoint-based algorithms to check constructivity. These algorithms are difficult to implement and somewhat inefficient for variables with non-Boolean types.
It is inefficient to check constructivity by enumerating all possible external valuations. Symbolic algorithms for checking constructivity manipulate sets of input valuations, representing them with BDD's. See R. Bryant, “Graph based algorithms for boolean function manipulation”,
IEEE Transactions on Computers,
1986; and G. Berry, “The Constrictive Semantics of Esterel”, Draft book, available at ftp://ftp-sop.inria.fr/meije/esterel/parers/constructiveness.ps.gz, 1995; the Shiple, G. Berry and H. Touati publication; and the Shiple PhD dissertation. This manipulation is based on simultaneous fixpoint equations derived from the circuit definitions and the types of the variables. For variables with k values in their type, these algorithms require k sets of valuations for each variable. Moreover, for arithmetic operations, the fixpoint equations are constructed from partitions (for +) or factorizations (for *) of all numbers in the type. Thus, these algorithms are somewhat inefficient and difficult to implement for variables with non-Boolean types.
SUMMARY OF THE INVENTION
The formulation disclosed herein overcomes the prior art limitations by presenting a simple, non-computational definition of constructivity (Constructivity-SAT) and a symbolic algorithm based on the new formulation that is simple to implement for variables with arbitrary finite types. It is shown that, by simple transformation, one can reformulate constructivity as the satisfiability of a set of equations derived from the definitions, over variable types extended with a value ⊥ (read as “bottom”). This formulation is non-computational and easily extensible to variables with any finite type. The formulation also handles definitions of indexed variables in the same manner. This constructivity check was implemented in COSPAN, which is the verification engine for the commercially available FormalCheck verification tool. The implementation is simple, and experience indicates that it usually incurs negligible overhead.
REFERENCES:
patent: 5491640 (1996-02-01), Sharma et al.
patent: 6012836 (2000-01-01), Mangelsdorf
patent: 6075932 (2000-06-01), Khouja et al.
Malik, “Analysis of Cyclic combinational circuits”, Transactions on computer aided design of Integrated circuits and systems, Jul. 1994.*
Namjoshi et al., “Efficient analysis of cyclic definitions”, Bell Laboratoties, 1999.*
Shiple, “Formal analysis of synchronous circuits”, A dissertation to the University of california, Berkeley, 1996.*
Brzozowski et al., “Asynchronous circuits”, 1996.*
Berry, “The constructive semantics of pure Esterel Draft version 2.0”, May 1996.*
Scott, “A type-theoritical alternative to ISWIM, CUCH OWHY”, Theoretical Computer Science, 1993.*
Bakker et al., “Control Flow Semantics”, MIT, 1996.*
Cousot, “Asynchronous iterative methods for solving a fixed point system of Monotone equations in a complete lattice”, Sep. 1997.*
Katzenelson et al., “S/R: A language for specifying protocols and other coordinating processes”, IEEE, 1986.*
Shiple, T.R. et al., “Constructive Analysis of Cyclic Circuits”, IEEE Catalog No.: 96TB100027, Mar. 1996.*
Srinivasa et al., “Practical analysis of cyclic combinational circuits”, Proceedings of IEEE Custom Integrated Circuits conference, May 1996.
Kurshan Robert Paul
Namjoshi Kedar Sharadchandra
Agere Systems Inc.
Broda Samuel
Ligon John
Thangavelu Kandasamy
LandOfFree
Method for identifying cyclicity in circuit designs does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method for identifying cyclicity in circuit designs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method for identifying cyclicity in circuit designs will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3096707