China
Africa
Explore chapters and articles related to this topic
Formal Property Verification
Published in Louis Scheffer, Luciano Lavagno, Grant Martin, EDA for IC System Design, Verification, and Testing, 2018
The Boolean satisfiability problem (SAT) is to determine whether there exists a truth assignment that makes a given Boolean formula true (or equivalently, whether there exists an input pattern that makes the output of a given Boolean circuit one). The first algorithm to solve this classic NP-complete problem was described in 1960 [76], and since then many improvements have been made. The success of recent SAT solvers such as Chaff [39] and Grasp [40] in solving very large problem instances prompted interest in using SAT solvers for model checking. In 1999, the notion of bounded model checking (BMC) using a SAT solver was introduced [41]. As in SMC, the transitions of the system and property automata are characterized by Boolean formulas. By unfolding this representation (i.e., making k consecutive copies, corresponding to consecutive time frames) the question of existence of a counter-example of k steps can be posed as a SAT problem. This made it possible to exploit recent advances in SAT solvers to find counterexamples to properties for systems much larger than can be handled by SMC (typically up to a few thousand registers).
Formal Property Verification
Published in Luciano Lavagno, Igor L. Markov, Grant Martin, Louis K. Scheffer, Electronic Design Automation for IC System Design, Verification, and Testing, 2017
Limor Fix, Ken McMillan, Norris Ip, Leopold Haller
The Boolean satisfiability problem (SAT) seeks to determine whether there exists a truth assignment that makes a given Boolean formula true (or equivalently, whether there exists an input pattern that makes the output of a given Boolean circuit one). The first algorithm to solve this classic NP-complete problem was described in 1960 [76], and since then many improvements have been made. The success of SAT solvers such as Chaff [39], GRASP [40], and MiniSat [113] in solving very large problem instances prompted interest in using SAT solvers for model checking. In 1999, the notion of bounded model checking (BMC) using a SAT solver was introduced [41]. As in SMC, the transitions of the system and property automata are characterized by Boolean formulas. By unfolding this representation (i.e., making k consecutive copies, corresponding to consecutive time frames), the question of existence of a counterexample of k-steps can be posed as a SAT problem. This made it possible to exploit advances in SAT solvers to find counterexamples to properties for systems much larger than can be handled by SMC (typically up to a few thousand registers).
On black-box optimization in divide-and-conquer SAT solving
Published in Optimization Methods and Software, 2021
O. S. Zaikin, S. E. Kochemazov
A Boolean variable x is a variable that can take only two values , often represented by respectively. A literal is either a Boolean variable or its negation . A sequence of literals connected by logical ‘or’, eg , is called a disjunction or a clause. It takes the value of if and only if any of the literals takes this value. A conjunction (logical ‘and’) of clauses is called a Conjunctive Normal Form (CNF). Any Boolean formula can be represented in CNF [59]. The Boolean satisfiability problem (SAT) in its decision variant is then formulated as follows: for a CNF C over Boolean variables from set , to answer the question whether there exists such an assignment of variables from X that once each variable is set to , the CNF C becomes . If such an assignment exists, then it is called satisfying assignment and C is called satisfiable. If there are no assignments satisfying the formula, then the formula is called unsatisfiable.