Verifying one or more properties of a design using SAT-based...

Details Verifying one or more properties of a design using SAT-based... Verifying one or more properties of a design using SAT-based...

2005-04-29

2010-06-22

Rodriguez, Paul L (Department: 2123)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000, C703S015000

Reexamination Certificate

active

07743350

ABSTRACT:
In one embodiment, a method for satisfiability (SAT)-based bounded model checking (BMC) includes isolating information learned from a first iteration of an SAT-based BMC process and applying the isolated information from the first iteration of the SAT-based BMC process to a second iteration of the SAT-based BMC process subsequent to the first iteration.

REFERENCES:
patent: 7047139 (2006-05-01), Shtrichman
patent: 7346486 (2008-03-01), Ivancic et al.
patent: 2003/0225552 (2003-12-01), Ganai et al.
patent: 2004/0230407 (2004-11-01), Gupta et al.
M. K. Ganai, L. Zhang, P. Ashar, and A. Gupta, “Combining strength of circuit-based and CNF-based algorithms for a high performance SAT solver,” in Design Automation Conference, 2002, pp. 1-4.
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model checking using SAT procedures instead of BDDs,” Proc. of the 36th ACM/IEEE Design Automation Conference, 1999, pp. 317-320.
Strichman, Tuning SAT Checkers for Bounded Model Checking, Jul. 2000, Springer, Proceedings of the 12th International Conference on Computer Aided Verification (CAV), vol. 1855 of Lecture Notes in Computer Science, pp. 480-494.
Kim et al., On Solving Stack-Based Incremental Satisfiability Problems, 2000, Proceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors, pp. 379-382.
Amla et al., Experimental Analysis of Different Techniques for Bounded Model Checking, Proc. of the 9th TACAS, vol. 2619 of LNCS, pp. 34-48, Springer, Apr. 2003, 15 pages.
Bjesse et al., “SAT-Based Verification without State Space Traversal,” Proc. of the 3rd Intl. Conf. on Formal Methods in CAD, vol. 1954 of LNCS, pp. 372-389, Springer, Nov. 2000, 18 pages.
Cabodi et al., Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals, Proc. of the Design Automation and Test in Europe, pp. 898-903, Mar. 2003, 6 pages.
Chauhan et al., “Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis,” Proc. of the 4th Int. Conf. on Formal Methods in CAD, vol. 2517 of LNCS, pp. 33-51, Nov. 2002, 19 pages.
Clarke et al., “Bounded Model Checking Using Satisfiability Solving,” Formal Methods in System Design, pp. 1-20, Jul. 2001, Kluwer Academic Publishers, 20 pages.
Copty et al., “Benefits of Bounded Model Checking in an Industrial Setting,” Proc. of the 13th Intl. Conf. on Computer Aided Verification, vol. 2102 of LNCS, pp. 436-453, Springer, Jul. 2001, 18 pages.
Fallah, “Binary Time-Frame Expansion,” Proc. of the Intl. Conf. on CAD, pp. 458-464, Nov. 2002, 9 pages.
Ganai et al., “Improved SAT-Based Bounded Reachability Anaylsis,” Proc. of the 15th Intl. Conf. on VLSI Design, pp. 729-734, Jan. 2002, 6 pages.
Goldberg et al., “BerkMin: A Fast and Robust Sat-Solver,” Proc. of Design Automation and Test in Europe, pp. 142-149, Mar. 2002, 8 pages.
Goldberg, “Using SAT for Combinational Equivalence Checking,” Proc. odf Design Automation Test in Europe, pp. 114-121, Mar. 2001, 8 pages.
Gupta et al., “Abstraction and BDDs Complement SAT-Based BMC in DiVer,” Proc. of the 15th Conf. on Computer-Aided Verification, vol. 2725 of LNCS, pp. 206-209, Springer, Jul. 2003, 4 pages.
Gupta et al., “Learning from BDDs in SAT-Based Bounded Model Checking,” Proc. of the 40th Design Automation Conf., pp. 824-829, Jun. 2003, 6 pages.
Gupta et al., “Iterative Abstraction Using SAT-Based BMC with Proof Analysis,” Proc. of the Intl. Conf. on CAD, pp. 416-423, Nov. 2003, 8 pages.
Iyer et al., “SATORI-A Fast Sequential SAT Engine for Circuits,” Proc. of the Intl. Conf. on CAD, pp. 320-325, Nov. 2003, 6 pages.
Kuehlmann et al., “Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification,” IEEE Trans. on CAD, 21(12):1377-1394, Dec. 2002, 18 pages.
Marques-Silva et al., “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Trans. on Computers, 48(5):506-521, May 1999, 16 pages.
McMillan, “Symbolic Model Checking: An Approach to the State Explosion Problem,” Kluwer Academic Publishers, 1993.
McMillan, “Interpolation and SAT-Based Model Checking,” Proc. of the 15th Conf. on Computer-Aided Verification, vol. 2725 of LNCS, Springer, Jul. 2003, pp. 1-13.
McMillan, “Automatic Abstraction Without CounterExamples,” Proc. of the 9th TACAS, vol. 2619 of LNCS, Springer, Apr. 2003, pp. 1-17.
Moskewitcz et al, “Chaff: Engineering an Efficient SAT Solver,” Proc. of the 38th Design Automation Conf., p. 530-535, Jun. 2001, 6 pages.
Sentovich et al., SIS: A System for Sequential Circuit Synthesis, Technical Report UCB/ERL M92/41, ERL, College of Engg. U.C. Berkeley, May 1998, pp. 1-45.
Shacham et al., “Tuning the VSIDS Decision Heuristic for Bounded Model Checking,” Proc. of the 4th Intl. Workshop on Microprocessor Test and Verification, pp. 75-79, May 2003.
Sheeran et al., “Checking Safety Properties Using Induction and a SAT-Solver,” Proc. of the 3rd Intl. Conf. on Formal Methods in CAD, vol. 1954 of LNCS, pp. 108-125, Springer, Nov. 2000, 19 pages.
Shtrichman et al, “Accelerating Bounded Model Checking of Safety Formulas,” Formal Methods in System Design, 24(1):5-24, Jan. 2004, Kluwer Academic Publishers, pp. 5-24, 20 pages, Jan. 2004.
The VIS Group, “VIS: A System for Verification and Synthesis,” Proc. of the 8th Intl. Conf. on Computer Aided Verification, vol. 1102 of LNCS, pp. 428-432, Springer, Jul. 1996, 7 pages.
Whittemore et al., “SATIRE: A New Incremental Satisfiability Engine,” Proc. of the 38th Design Automation Conf., pp. 542-545, Jun. 2001, 6 pages.
[http://ee.princeton.edu/˜chaff/zchaff.php,]Dec. 2003, 1 page.
Zhang, “SATO: An Efficient Propositional Prover,” Proc. of the Intl. Conf. on Automated Deduction, pp. 272-275, Jul. 1997, 5 pages.
Arora et al., “Enhancing SAT-Based Bounded Model Checking Using Sequential Logic Implications,” IEEE VLSI Design Conference, pp. 784-787, 4 pages, Jan. 2004.
T.V. Group, “VIS: A System for Verification and Synthesis,” Proc. of the 8th International Conference on Computer Aided Verification, vol. 1102, pp. 428-432, New Brunswick, New Jersey, Springer, Jul. 1996, 7 pages.
Bakoglu, “Circuits, Interconnections, and Packaging for VLSI,” Addison -Wesley Publishing Company, pp. 541 pages, 1990.

Affiliated with

Also associated with

Rating

Verifying one or more properties of a design using SAT-based... does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Verifying one or more properties of a design using SAT-based..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying one or more properties of a design using SAT-based... will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-4162893