Efficient SAT-based unbounded symbolic model checking
AssigneeNEC Laboratories America, Inc.
InventorsMalay Ganai, Aarti Gupta, Pranav Ashar
Life of this patent
Estimating the term…
Abstract
An efficient approach for SAT-based quantifier elimination and pre-image computation using unrolled designs that significantly improves the performance of pre-image and fix-point computation in SAT-based unbounded symbolic model checking.
Claims29
A computer-implemented method of solving a SAT-based quantifier elimination problem, said method comprising the following steps:
- enumerating, as a result of a series of calls to a SAT solver, satisfying solutions for a given Boolean formula;
- cofactoring the given Boolean formula with a satisfying minterm over the variables to be quantified, in order to capture one or more satisfying states enumerated by the SAT solver, and to additionally capture some satisfying states that cannot be captured by a cube and that have not yet been enumerated by the SAT solver;
- and
- representing, a suitably efficient representation of the captured states.
A computer implemented method for computing backward reachable states iteratively, said method comprising the steps of:
- a) unrolling a design, successively in a step-by-step manner;
- b) calculating, a pre-image across multiple time frames in the unrolled design in each of the successive steps;
- c) updating, a set of backward reachable states, starting from a given set of target states, in each of the successive steps;
- and
- d) repeating, the steps a-c until a suitable termination criterion on the backward reachable states is obtained.
A computer implemented method for computing backward reachable states iteratively, said method comprising the steps of:
- a) calculating, a pre-image across a single time frame of a design in each of the successive steps;
- said calculating step including:
- enumerating, as a result of a series of calls to a SAT solver, satisfying solutions for a given Boolean formula;
- cofactoring the given Boolean formula with a satisfying minterm over the variables to be quantified, in order to capture one or more satisfying states enumerated by the SAT solver, and to additionally capture some satisfying states that cannot be captured by a cube and that have not yet been enumerated by the SAT solver;
- and
- representing, a suitably efficient representation of the captured states;
- b) updating, a set of backward reachable states, starting from a given set of target states, in each of the successive steps;
- and
- c) repeating, the steps a-b until a suitable termination criterion on the backward reachable states is obtained.
Dependencies are inferred from the claim text.