Verification using simultaneous and inductive SAT algorithms

Details Verification using simultaneous and inductive SAT algorithms Verification using simultaneous and inductive SAT algorithms

2006-10-30

2010-06-01

Lin, Sun J (Department: 2825)

Computer-aided design and analysis of circuits and semiconductor

Nanotechnology related integrated circuit design

C716S030000

Reexamination Certificate

active

07730436

ABSTRACT:
A simultaneous satisfiability algorithm, or SSAT, allows simultaneous checks to be made efficiently for a number of literals, x1, . . . ,xnwhether x1is true under any satisfying assignments of a formula (written in conjunctive normal form) built from the variables of these literals and other variables (or, equivalently whether x1is a logical consequence of the formula). Thus, several related satisfiability checks are performed simultaneously in SSAT. Temporal induction algorithms allow the verification of the sequential behavior of finite state machines, e.g., hardware. Temporal induction algorithms may employ a SSAT solver to perform simultaneous model checking of several invariant (or safety) properties efficiently. These SSAT-based temporal induction algorithms are double-incremental, such that all learned clauses in the SSAT solver are re-used both across verified properties as well as across time frames.

REFERENCES:
Biere A., A. Cimatti, E. Clarke, Y. Zhu,Symbolic model checking without BDDs, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1999.
Biere, A., A. Cimatti, E. Clark, O. Strichman, Y. Zhu,Bounded Model Checking, Chapter in Advances in Computers, vol. 58, 2003.
Bryant, R.E.,Graph-based algorithms for Boolean function manipulation, IEEE Trans. Computers, C-35(8), 1986.
Davis M., G. Logemann, D. Loveland,A machine program for theorem proving. In Communications of the ACM, (5):394-397, 1962.
Davis M., H. Putnam,A computing procedure for quantification theory, J. ACM, vol. 7, 1960.
Eén, N., N. Sörensson,Temporal induction by incremental SAT solving, International Workshop on Bounded Model Checking, BMC 2003.
Fraer, R., S. Ikram, G. Kamhi, T. Leonard, A. Mokkedem,Accelerated verification of RTL assertions based on satisfiability solvers, HLDVT, 2002.
Goldberg, E., Y. Novikov,An efficient learning procedure for multiple implication check. In Design, Automation, and Test in Europe, 2001.
Gomes C.P., B. Selman, H. Kautz,Boosting combinatorial search through randomization, National Conference on Artificial Intelligence, 1998.
Kuehlmann A., M.K. Ganai, V. Paruthi,Circuit-based Boolean reasoning, DAC 2001.
Khasidashvili, Z., M. Skaba, D. Kaiss, Z. Hanna,Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints, ICCAD'04, 2004.
Lynce I., J. Marques-Silva,Building state-of-the-art SAT solvers, European Conference on Artificial Intelligence (ECAI), 2002.
Marques-Silva, J.P., K.A. Sakallah,Robust search algorithm for test pattern generation, IEEE Fault-Tolerant Computing Symposium, 1997.
Marques-Silva, J.P., K.A. Sakallah, GRASP:A search algorithm for propositional satisfiability, IEEE Transactions on Computers, vol. 48, 1999.
McMillan, K.L.,Symbolic Model Checking, Kluwer, 1993.
Nadel A.,Backtrack search algorithms for propositional satisfiability: Review and Innovations, Master Thesis, The Hebrew University of Jerusalem, Nov. 2002.
Prasad M., A. Biere, A. Gupta,A survey of recent advances in SAT-based formal verification, Int. Journal on Software Tools for Technology Transfer (STTT), vol. 7, No. 2, 2005.
Sheeran, M., S. Singh, G. Stalmarck,Checking safety properties using induction and a SAT-solver, FMCAD, 2000.
Strichman, O.,Accelerating bounded model checking of safety properties, Formal Methods in System Design, vol. 24, 2004.
Zabih R., D.A. McAllester,A rearrangement search strategy for determining propositional satisfiability, National Conference on Artificial Intelligence, 1988.
Zhang, L., C.F. Madigan, M.H. Moskewicz, S. Malik,Efficient conflict driven learning in a Boolean satisfiability solver. International Conference on Computer-Aided Design (ICCAD'01), 2001.
Whittemore, J., K. Kim, K. Sakallah,SATIRE: A new incremental satisfiability engine, DAC, 2001.
Jun Gu, Paul W. Purdom, John Franco, Benjamin W. Wah,Algorithms for the satisfiability(SAT)problem: A survey, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1996.

Affiliated with

Also associated with

Rating

Verification using simultaneous and inductive SAT algorithms does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Verification using simultaneous and inductive SAT algorithms, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verification using simultaneous and inductive SAT algorithms will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-4212864