Data processing: structural design – modeling – simulation – and em – Simulating electronic device or electrical system – Circuit simulation
Reexamination Certificate
1999-06-20
2002-11-19
Teska, Kevin J. (Department: 2123)
Data processing: structural design, modeling, simulation, and em
Simulating electronic device or electrical system
Circuit simulation
C703S002000, C716S030000, C716S030000, C716S030000
Reexamination Certificate
active
06484134
ABSTRACT:
FIELD OF THE INVENTION
The present invention is related to computer-aided design (CAD), and more particularly to property coverage in formal verification of integrated circuits.
BACKGROUND INFORMATION
One of the problems with modem logic design is the verification that the design actually works in the way it was intended to work. Undetected errors in the logic design may cause costly redesigns, or even loss of consumer confidence in the product if the product has been released on the market.
Model checking is one method of verifying designs. Model checking is a formal verification (FV) technology for property verification. A property specifies the desired values of particular circuit signals at various points in time in relation to other signals. Given a model of a design and some desired properties, a model checker like Symbolic Model Verifier (SMV) verifies whether the model satisfies all the desired properties under all possible input sequences. The properties are specified in a property specification language such as Computation Tree Logic (CTL). Although model checking is an exhaustive FV technique, a bug can escape the model checking effort if the properties specified by the user do not check for the erroneous behavior caused by the bug. Such erroneous behavior usually occurs in some obscure corner case that has been missed by the user. This is quite common when the specification has to be manually decomposed into a set of smaller, more tractable properties that are verifiable by the model checker. To reduce bug escapes, the user needs to continuously strengthen existing properties and specify new properties, without knowing if the additional verification is insufficient or redundant.
Logic simulation is another method of verifying designs. In existing simulation-based verification methodologies, coverage metrics are used to improve the quality of a test suite and estimate the progress of the verification task. For example, a common coverage metric for simulation is “code coverage”, which measures the fraction of hardware description language (“HDL”) statements exercised during simulation. An “observability based code coverage” enhances this metric by factoring potential error propagation to observability points. “Transition coverage” is another metric for control state machines. Such coverage metrics are effective in reducing bug escapes by pointing out coverage holes in the test suite.
However, the existing coverage metrics for simulation do not apply directly to model checking, e.g., a naive interpretation of the code coverage or transition coverage metric on a model checking task gives a meaningless coverage of 100% for every property. Logic simulation is dynamic and its coverage is driven by input simulation vectors, whereas model checking is static without any notion of circuit execution. Unlike logic simulation, the likelihood of having a bug escape detection in a model checking effort depends solely on the quality of the properties verified. Therefore, what is needed is a coverage metric that estimates the “completeness” (i.e. the quality) of a set of properties against which the design has been verified.
For example, consider the CTL formula for count, a modulo-5 counter, with stall and reset as external inputs:
AG[((-stall&Lgr;-reset&Lgr;(count=C)&Lgr;(C<5))→AX(count=C+1)]
This formula specifies that if the stall and reset signals are deasserted and the counter value is less than 5, then the counter increments by 1 in the next step. The model checker explores the entire reachable state space to verify the property. However, in reality, it ascertains the correctness of the condition on count (that it increments correctly) only in those states that are immediate successors of states satisfying the antecedent. The actual checking of the correctness condition on the model state space is thus constrained by the CTL formula. Thus, this property cannot be said to provide 100% coverage. This example illustrates the need to define a coverage measure for formally verified properties.
For this and other reasons, there is a need for the present invention.
SUMMARY OF THE INVENTION
One aspect of the present invention is a method of measuring coverage of a formal verification property. The method includes receiving a model of a logic design wherein the model has a plurality of states. The method also includes receiving a property verified for the model of the logic design and receiving one or more observed signals for the property. The method further includes providing a set of covered states in which checking a value of the one or more observed signals is sufficient to determine the validity of the verified property.
A further aspect of the present invention is an alternate method of measuring coverage of a formal verification property. The method includes receiving a model of a logic design wherein the model has a plurality of states. The method also includes receiving a property verified for the model of the logic design and receiving one or more observed signals for the property. The method further includes providing a set of covered states for the observed signal of the property, wherein the set of covered states comprise each one of the states in which changing a value of the observed signal in the state causes the property to fail.
REFERENCES:
patent: 6074426 (2000-06-01), Baumgartner et al.
patent: 6157901 (2000-12-01), Howe
patent: 6212669 (2001-03-01), Jain
patent: 0862128 (1998-09-01), None
Fallah et al, “OCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional Verification”, Proceedings of the 35th Design Automation Conference, pp. 152-157 (Jun. 1998).*
Moundanos et al, “Abstraction Techniques for Validation Coverage Analysis and Test Generation”, IEEE Transactions on Computers, vol. 47 No. 1, pp. 2-14 (Jan. 1998).*
Swamy, “Formal Verification of Digital Systems”, Proceedings of the Tenth International Conference on VLSI Design, pp. 213-217 (Jan. 1997).*
Pixley et al, “Commercial Design Verification: Methodology and Tools”, Proceedings of the International Test Conference, pp. 839-848 (Oct. 1996).*
Grinwald, R., et al., “User Defined Coverage—A Tool Supported Methodology for Design Verification”, Proceedings of the 35th Design and Automation Conference, San Francisco, CA, 15-19, (Jun., 1998).
Moundanos, D., et al., “Using Verification Technology for Validation Coverage Analysis and Test Generation”, Proceedings of the 16th IEEE VLSI Test Symposium, Monterey, CA, 254-259, (Apr., 1998).
Bryant, R.E., “Graph-Based Algorithms for Boolean Function Manipulation”,IEEE Transactions on ComputersC-35 (8), 677-691, (Aug. 1986).
Cheng, K., et al., “Automatic Functional Test Generation Using the Extended Finite State Machine Model”, Proceedings of the 30th Design Automation Conference, Conference held at the Dallas Convention Center, Dallas, Texas, 86-91, (Jun. 14-18, 1993).
Cho, H., et al., “Redundancy Identification/Removal and Test Generation for Sequential Circuits Using Implicit State Enumeration”,IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12 (7), 935-945, (Jul. 1993).
Clarke, E.M., et al., “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications”,ACM Transactions on Programming Languages and Systems, 8 (2), 244-263, (Apr. 1986).
Devadas, S., et al., “An Observability-Based Code Coverage Metric for Functional Simulation”, Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, Conference held in San Jose, CA, 418-425, (Nov. 10-14, 1996).
Ho, P., et al., “Formal Verification of Pipeline Control Using Controlled Token Nets and Abstract Interpretation”, Proceedings of the ICCAD International Conference on Computer-Aided Design, Conference held in San Jose, CA, 529-536, (Nov. 8-12, 1998).
Ho, R.C., et al., “Architecture Validation for Processors”, Proceedings of the 22nd Annual International Symposium on Computer Architecture, Symposium held in Santa Margherita Ligure, Italy, 404-41
Broda Samuel
Intel Corporation
Schwegman Lundberg Woessner & Kluth P.A.
Teska Kevin J.
LandOfFree
Property coverage in formal verification does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Property coverage in formal verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Property coverage in formal verification will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2992204