Measure of analysis performed in property checking

Details Measure of analysis performed in property checking Measure of analysis performed in property checking

2008-01-08

2008-01-08

Chang, Jack (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000

Reexamination Certificate

active

07318205

ABSTRACT:
The amount of analysis performed in determining the validity of a property of a digital circuit is measured concurrent with performance of the analysis, and provided as an output when a true/false answer cannot be provided e.g. when stopped due to resource constraints. In some embodiments, a measure of value N indicates that a given property that is being checked will not be violated within a distance N from an initial state from which the analysis started. Therefore, in such embodiments, a measure of value N indicates that the analysis has implicitly or explicitly covered every possible excursion of length N from the initial state, and formally proved that no counter-example is possible within this length N.

REFERENCES:
patent: 5465216 (1995-11-01), Rotem et al.
patent: 5724504 (1998-03-01), Aharon et al.
patent: 6102959 (2000-08-01), Hardin et al.
patent: 6192505 (2001-02-01), Beer et al.
patent: 6292765 (2001-09-01), Ho et al.
patent: 6311293 (2001-10-01), Kurshan et al.
patent: 6356858 (2002-03-01), Malka et al.
patent: 6457162 (2002-09-01), Stanion
patent: 6539523 (2003-03-01), Narain et al.
patent: 6728939 (2004-04-01), Johannsen
patent: 6848088 (2005-01-01), Levitt et al.
patent: 7020856 (2006-03-01), Singhal et al.
P.A. Abdulla, P. Bjesse, and N. Een. “Symbolic Reachability Analysis Based on SAT Solvers,” TACAS '00, 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer-Verlag, 2000, pp. 411-425.
A PhD thesis by K. L. McMillan entitled “Symbolic model checking—an approach to the state explosion problem”, Carnegie Mellon University, 1992, pp. 1-212.
E. M. Clarke, E. A. Emerson and A. P. Sistla entitled “Automatic verification of finite-state concurrent systems using temporal logic specifications” published in ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986.
Hoskote, Y. V., et al., “Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors”, International Conference on Computer Design: VLSI in Computers & Processors, Oct. 2-4, 1995, pp. 532-537.
Martin Davis, George Longemann, and Donald Loveland, “A machine program for theorem-proving” in Communications of the ACM, 5(7):394-397, Jul. 1962.
C. Maxfield, EEdesign, “Why properties are important”, May 12, 2002 (10:20AM), URL: http://www.eedesign.com/story/OEG20020515S0033, pp. 1-5.
R. Goering & M. Santarini, EE Times, “Tool vendors attach verification logjam”, Mar. 4, 2002 (7:29 AM), URL: http://www.eedesign.com/story/OEG20020304S0018, pp. 1-4.
A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures Instead of BDDs,” Proceedings of the Design Automation Conference (DAC '99), Jun. 1999.
A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs,” Proceedings of Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 1579, LNCS, 1999.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang, “Symbolic model checking: 1020 states and beyond”, published in Information and Computation, vol. 98, No. 2, Jun. 1992.
Yatin Hoskote, Timothy Kam, Pei-Hsin Ho, and Xudong Zhao, “Coverage Estimation for Symbolic Model Checking” , published in Proceedings of DAC 1999 (Best Paper Award), pp. 300-305.
Jerry R. Burch and David L. Dill , “Automatic Verification of Pipelined Microprocessor Control”, published in the proceedings of International Conference on Computer-Aided Verification, LNCS 818, Springer-Verlag, Jun. 1994, pp. 1-17.
David Dill, Andreas Drexler, Alan Hu and C. Han Yang , “Protocol Verification as a Hardware Design Aid” published in Proceedings of the International Conference on Computer Design, Oct. 1992, pp. 1-4.
Moundanos, D., “Abstraction Techniques for Validation Coverage Analysis and Test Generation”, Believed to be prior to Jun. 2002, pp. 1-35.
Devadas, S., et al., “An Observability-Based Code Coverage Metric for Functional Simulation”, IEEE/ACM International Conference on Computer-Aided Design, Nov. 10-14, 1996, pp. 418-425.
Geist, D., et al., “Coverage-Directed Test Generation Using Symbolic Techniques”, Formal Methods in Computer-Aided Design, First International Conf., FMCAD 96, Palo Alto, CA, Nov. 6-8, 1996, pp. 142-159.
M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver”, in 38th Design Automation Conference (DAC '01), Jun. 2001, pp. 530-535.
A. Kuehlmann, M. Ganai & V. Paruthi, “Circuit-Based Boolean Reasoning”, Proceedings of the Design Automation Conference (DAC'01), Jun. 2001, 8 pages.
A. Kuehlmann, V. Paruthi, F. Krohm, & M. Ganai, Robust Boolean Reasoning for Computer-Aided Design of Integrated Circuits and Systems, vol. 21, No. 12, Dec. 2002, pp. 1377-1394.
M. Ganai, & A. Aziz, “Improved SAT-Based Bounded Reachability Analysis”, Proceedings of the 15thInternational Conference on VLSI Design (VLSID '02), Mar. 2002, 6 pages.
E. Clarke, A. Biere, R. Raimi & Y. Zhu, “Bounded Model Checking Using Satisfiability Solving”, Formal Methods in System Design vol. 19 Issue I, Jul. 2001, by Kluwer Academic Publishers, pp. 1-20.
C. Kern & M. Greenstreet, “Formal Verification in Hardware Design: A Survey”, ACM Trans. On Design Automation of Electronic Systems, vol. 4, pp. 1-61, Apr. 1999, available on the Internet at http://citeseer.nj.nec.com/kern99formal.html.
R. C. Ho, C. Han Yang, M. A. Horowitz & D. L. Dill, “Architecture Validation for Processors”, Proceedings 22ndAnnual International Symposium on Computer Architecture, pp. 404-413, Jun. 1995.
R. C. Ho, & M. A. Horowitz, “Validation Coverage Analysis for Complex Digital Designs”, Proceedings 1996 IEEE/ACM International Conference on Computer-Aided Design, pp. 146-151, Nov. 1996.
J. Gu, P.W. Purdom, J. Franco & B.W. Wah, “Algortihms for the Satisfiability (SAT) Problem: A Survey”, DIAMACA Series on Discrete Mathematics and Theoretical Computer Science 35: 0-131, American Mathematical Society, 1997, available on the Internet at http://Citeseer.nj.nec.com/56722.html.

Affiliated with

Also associated with

Rating

Measure of analysis performed in property checking does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Measure of analysis performed in property checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Measure of analysis performed in property checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-2801267