Property specific testbench generation framework for circuit...

Details Property specific testbench generation framework for circuit... Property specific testbench generation framework for circuit...

2005-12-13

2005-12-13

Follansbee, John (Department: 2154)

Data processing: structural design, modeling, simulation, and em

Simulating electronic device or electrical system

Circuit simulation

C703S015000, C703S016000, C716S030000

Reexamination Certificate

active

06975976

ABSTRACT:
Simulation continues to be the primary technique for functional validation of designs. It is important that simulation vectors be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The focus of this work is to generate property-specific testbenches that are targeted either at proving the correctness of a property or at finding a bug. It is based on performing property-specific analysis on iteratively less abstract models of the design in order to obtain interesting paths in the form of a Witness Graph, which is then targeted during simulation of the entire design. This testbench generation framework will form an integral part of a comprehensive verification system currently being developed.

REFERENCES:
patent: 5953519 (1999-09-01), Fura
patent: 6182258 (2001-01-01), Hollander
patent: 6185726 (2001-02-01), Chou
patent: 6233540 (2001-05-01), Schaumont et al.
patent: 6243852 (2001-06-01), Yoshikawa
patent: 6321363 (2001-11-01), Huang et al.
patent: 6477683 (2002-11-01), Killian et al.
Gupta et al., “Toward formalizing a validation methodology using simulation coverage,” Design Automation Conference, 1997. Proceedings of the 34th , Jun. 9-13, 1997 pp. 740-745.
Fallah et al., “Simulation Vector Generation from HDL Descriptions for Observability-Enhanced Statement Coverage,” Proc. 36 Design Automation Conf., 1999, pp. 158-167.
Ganai et al., “Enhancing Simulation with BDDs and ATPG,” Proc. Design Automation Conference, 1999, pp. 385-390.
Geist et al., “Coverage-directed test generation using symbolic techniques,” In Proceedings of the International Conference on Formal Methods in CAD, pp. 143-158, Nov. 1996.
F. Balarin, et al., “An iterative approach to language containment,” In Proceedings of the International Conference on Computer-Aided Verification, vol. 697 of Lecture Notes in Computer Science, pp. 29-40, 1993.
R. K. Brayton et al., “VIS: A system for verification and synthesis”, In R. Alur and T. Henzinger, editors, Proceedings of the International Conference on Computer-Aided Verification, vol. 1102, pp. 428-432. Springer-Verlag, Jun. 1996.
R. E. Bryant, “Graph-based algorithms for Boolean function manipulation”, IEEE Transactions on Computers, C-35(8):677--691, Aug. 1986.
J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, “Symbolic model checking for sequential circuit verification”, IEEE Transactions on Computer-Aided Design, 13(4):401-424, Apr. 1994.
A. K. Chandra, et al., “Avpgen—a test case generator for architecture verification”, IEEE Transaction on VLSI Systems, 6(6), Jun. 1995.
E. M. Clarke, 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.
E. M. Clarke, et al., “Counterexample-guided abstraction refinement”, In Proceedings of the International Conference on Computer-Aided Verification, vol. 1855 of Lecture Notes in Computer Science, pp. 154-169, 2000.
F. Fallah, et al., “Functional vector generation for HDL models using linear programming and 3-Satisfiability”, In Proceedings of the Design Automation Conference, pp. 528-533, San Francisco, CA, Jun. 1998.
M. Ganai, et al., “Augmenting simulation with symbolic algorithms”, In Proceedings of the Design Automation Conference, Jun. 1999.
D. Geist, et al., “Coverage-directed test generation using symbolic techniques”, In Proceedings of the International Conference on Formal Methods in CAD, pp. 143-158, Nov. 1996.
R. C. Ho, et al., “Architecture validation for processors”, In Proceedings of the 22nd Annual International Symposium on Computer Architecture, Jun. 1995.
Y. Hoskote, et al., “Coverage estimation for symbolic model checking”, In Proceedings of the Design Automation Conference, pp. 300-305, Jun. 1999.
Y. Hoskote, et al., “Automatic extraction of the control flow machine and application to evaluating coverage of verification vector”, In Proceedings of the International Conference on Computer Design, pp. 532-537, Oct. 1995.
C.-Y. Huang, et al., “Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques”, In Proceedings of the Design Automation Conference, pp. 118-123, 2000.
C. N. Ip, et al. “Using symbolic analysis to optimize explicit reachability analysis”, In Proceedings of Workshop on High Level Design Validation and Test, 1999.
S. Katz, et al., “Have I Written Enough Properties? —a method of comparison between specification and implementation”, In Proceedings of Correct Hardware Design and Verification Methods (CHARME), vol. 1703 of Lecture Notes In Computer Science, pp. 280-297, Sep. 1999.
A. Kuehlmann, et al., “Probabilistic state space search”, In Proceedings of the International Conference on Computer-Aided Design, 1999.
W. Lee, et al., “Tearing based abstraction for CTL model checking”, In Proceedings of the International Conference on Computer-Aided Design. pp. 76-81, San Jose, CA, Nov. 1996.
J. Lind-Nielsen, et al., “Stepwise CTL model checking of state/event systems”, In Proceedings of the International Conference on Computer-Aided Verification, vol. 1633 of Lecture Notes in Computer Science, pp. 316-327. Springer-Verlag, 1999.
D. E. Long, Model Checking, Abstraction and Modular Verification, PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, Jul. 1993.
A. Pardo, et al., “Automatic abstraction techniques for propositional μ-calculus model checking”, In Proceedings of the International Conference on Computer Aided Verification, vol. 1254 of Lecture Notes in Computer Science, pp. 12--23, Jun. 1997
R. Sumners, et al., “Improving witness search using orders on states”, In Proceedings of the International Conference on Computer Design, pp. 452--457, 1999.
Synopsys, Inc. VERA System Verifier, http://www.synopsys.com/products/vera/vera.html.
TransEDA, Inc. Verification Navigator, http://www.transeda.com.
Verisity Design, Inc. Specman Elite, http://www.verisity.com/html/specmanelite.html.
K. Wakabayashi, “C-based Synthesis Experiences with a Behavior Synthesizer “Cyber””, In Proceedings of the Design Automation and Test in Europe (DATE) Conference, pp. 390-393, 1999.
C. Han Yang, et al., David L. Dill, “Validation with guided search of the state space”, In Proceedings of the Design Automation Conference, Jun. 1998.
J. Yuan, et al., “On combining formal and informal verification”, In Proceedings of the International Conference on Computer-Aided Verification, vol. 1254 of Lecture Notes in Computer Science, pp. 376-387, Jun. 1997.

Affiliated with

Also associated with

Rating

Property specific testbench generation framework for circuit... 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 specific testbench generation framework for circuit..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Property specific testbench generation framework for circuit... will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3466959