The present invention is related to verification of circuit designs. More particularly, the present invention is directed to a method and system for verifying circuit designs through propagation of assertions.
Circuit designers and verification engineers use different methods to verify circuit designs. One common method of verification is the use of simulation. Simulation dynamically verifies a design by monitoring behaviors of the design with respect to simulation test benches. Another method of verification is the use of model checking. Model checking statically verifies properties of a design by analyzing the state space of the design and determining whether a property holds in all reachable states. The properties to verify may be global properties involving signals in widely separated parts of the design, or they may be more local properties that pertain only to single or small number of related modules in the design.
As used herein, the term “module” refers to any part of an integrated circuit design. A module may comprise, for example, one or more functional components or a part of each of one or more functional components. A module is generally parameterized and thus may be instantiated one or more times in an integrated circuit design to describe “instances” of that module. An integrated circuit design in this case is comprised of module instances.
Model checking has potential advantages over simulation. For example, no simulation test bench is required to run model checking. Additionally, model checking, unlike simulation, is exhaustive. On the other hand, model checking, due to computational limitations, generally cannot handle large designs. Hence, designs must often be partitioned into sufficiently small parts in order to model check a given property. Although presently capacity is not an issue for simulation of designs, it is foreseeable that in the future, designs could be of a size that cannot be handled by a simulator as a whole. Model checking is also sensitive to assumptions about the environment of the portion of the design being checked, and is prone to generating false negatives, i.e., reports of failures that cannot actually happen, if sufficient information about the environment is not included in the run.
Properties of a circuit design can be embedded in the design in the form of assertions, i.e., statements that describe expected design behavior. Assertions can be entered by the circuit designer or added by a separate process. These assertions, which relate to either local or global properties, can be used to verify a design using dynamic and/or static techniques. When a simulator is applied to the design, the assertions can be extracted as part of a test bench and used in checking the circuit for assertion violations. When model checking is applied to the design, an assertion can serve as the basis for what is checked.
For model checking of global properties, in which the signals involved may be widely distributed within the design, partitioning is typically driven by data dependencies. For example, COSPAN (Coordination Specification Analysis), a well-established verification system developed by Bell Laboratories in the mid-1980s, uses a method called iterative reduction to focus verification on just the portion of the design required. This method incrementally adds in more and more of the design's behavior in an attempt to eliminate negative results. Because this approach is automatic and follows data dependencies, the boundary of the behavioral region being considered may not be obvious to the user, and it may not coincide with natural boundaries in the design. Additionally, this approach requires having the entire design available in memory, so that incremental portions can be pulled in as needed. Further details regarding this method is disclosed in U.S. Pat. No. 5,691,925, which is hereby incorporated by reference in its entirety.
A different approach may be taken for local property checking as the local properties only apply to a restricted portion of the design. Partitioning for model checking local properties can first be done along module or instance boundaries so that only a portion of the design need be in memory for a given verification run. Such partitions would also follow the natural partitioning present in the design hierarchy, and would be easy for designers and verification engineers to understand. Further details regarding partitioning of a circuit design is disclosed in co-pending U.S. application Ser. No. 10/422,535, filed on Apr. 23, 2003, which is hereby incorporated by reference in its entirety. However, there is still a need for appropriate constraints on the environment of each such partition, in order to avoid false negatives.
Consider a single module of a design, containing embedded assertions. If one of the embedded assertions is strictly dependent upon input ports of the module, or strictly dependent upon outputs of a subordinate instance, then that assertion cannot be checked in the context of the module alone; however, it can be interpreted as an environmental constraint and used as an assumption when checking other assertions in the module. That assertion must be checked in another, or a larger, context, in which the logic driving the signals involved in the assertion is available. This implies that assertions that have been embedded elsewhere, and can be checked in that other context, could potentially be used as assumptions in this module, if they constrain signals that drive inputs to this module.
Thus, instead of incrementally extending a partition to include more behavior that might be necessary to verify a given assertion, the assertions can be proactively redistributed in a design to create local copies in each potential partition, so that any remote assertions likely to be useful as assumptions in a given partition are locally available in each possible partition. Since the assertions in a design are likely to be more concise and focused than the design itself, this approach could be quite effective, provided that enough properties are embedded in the design to capture all the significant behavior of the design.
Several issues need to be considered when propagating assertions in this manner. Since each module in a design may be instantiated many times, and may instantiate other modules many times, there is a need to manage the potential multiplication of assertions when propagating an assertion from a module to the context of each instance of that module or to each module instantiated in that module. Detecting any conflict among propagated assertions and checking for compatibility between propagated assertions (e.g., clock information) and that specified by the user, when both are present, are some other issues that need to be considered.
A further issue that should be considered is the need to avoid circular reasoning, i.e., where an assumption is directly or indirectly used to prove itself. For example, if an assertion A is assumed to be true in order to verify an assertion B, then it would be logically unsound to in addition, assume B to be true in order to verify A. One way to avoid circular reasoning is to check for cycles in the inference tree, and bar any assumption that would close a cycle. For example, in the above example, having used A to verify B, an attempt to then use B to verify A would be barred because A→B→A would close a cycle in the inference tree.
One drawback of the above method is that it is not reproducible if the verification process is started in a different place. For example, the verification process may start with A and verify B using A. At another time, the verification process may start with B and verify A using B. Suppose that A is also verifiable in its own right (without any assumptions), but that fact was not known when B was used to verify A. In the first case, B may be verified using A and then all that's left is to verify A in its own right. If this succeeds, both A and B are verified. In the second case, A is verified using B, and thus A cannot be used to verify B. In this case, if B is not verifiable in its own right, A is conditionally verified and B is unverified. It may be unacceptable to get different verification results for the same design, depending on where in the design the verification process initiates.
The present invention provides a method and system for verifying circuit designs through propagation of assertions. In an embodiment, a plurality of assertions in a circuit design are propagated within the design. The circuit design is then verified using at least one of the propagated assertions as an assumption.
Further details of aspects, objects, and advantages of the invention are described below in the detailed description, drawings, and claims. Both the foregoing general description and the following detailed description are exemplary and explanatory, and are not intended to be limiting as to the scope of the invention.