China
Africa
Explore chapters and articles related to this topic
Equivalence Checking
Published in Louis Scheffer, Luciano Lavagno, Grant Martin, EDA for IC Implementation, Circuit Design, and Process Technology, 2018
Andreas Kuehlmann, Fabio Somenzi
A SAT solver returns an assignment to the variables of a propositional formula that satisfies it if such an assignments exists. A literal is either a variable or its negation, a clause is a disjunction of literals from distinct variables, and a CNF formula is a conjunction of clauses. We shall use the following simple CNF formula as a running example: () (¬a∨b∨c)∧(a∨¬b∨c)∧(¬c∨d)∧(¬c∨¬d)
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
One of the central developments in SMT is the DPLL(T) framework [101,102], which lifts the architecture of modern propositional SAT solvers to incorporate support for first-order theories. The core idea is to split the satisfiability task among two communicating solvers: a SAT solver is used to reason about the propositional structure of the problem and handles basic Boolean operators, while a theory solver reasons about conjunctions of atomic subformulas. The SAT solver represents theory atoms abstractly as Boolean variables and generates candidate truth assignments. The theory solver is used to check whether these candidate assignments are satisfied by some first-order model in the theory. Theory solvers may also communicate inferred truth values to the propositional solver or help learn new propositional information. SMT solvers may combine multiple different theory solvers into a single solver for the combined theory [103,104].
An extensible circuit-based SAT solver
Published in Journal of Experimental & Theoretical Artificial Intelligence, 2020
A conflict driven clause learning (CDCL) SAT solver keeps assigning values to variables until either all clauses are satisfied or a conflict is found, i.e. a literal is assigned opposite values as a result of unit propagation by two different clauses. Here, the assignments made by choice are known as decisions and those by unit propagation as implications. Each decision and its implications are associated with a level called decision level, which is incremented at each decision and decremented as a decision is rolled back. Assignments done at decision level 0 are permanent assignments and cannot be retracted. When a conflict occurs the solver learns a clause from it using a learning strategy by performing a specific set of resolution operations (described below) such that the learnt clause is the final resolvent. It then adds the clause into the theory, undoes all assignments (decisions and implications) up to a certain decision level (backtracks or backjumps) called assertion level (described below) in the reverse chronological order. The above process continues until either a satisfying assignment is found (theory is SAT) or an empty clause is learnt (theory is UNSAT). When an empty clause is learnt the solver backtracks to the decision level zero.