|
Abstract:
|
Reducing the verification of a property in a system to a decision
problem in some logic is a common practice in formal
verification. Decision procedures can then be used to automate the
solution of the verification task at hand. In this talk we describe
efficient decision procedures, their implementation and use in formal
verification. The main focus is on decision procedure for
propositional satisfiability. We outline a "modern" implementation of
the Davis-Logemann-Loveland (DLL) algorithm for propositional
satisfiability (SAT). The effectiveness of the approach was tested by
developing SIMO, a C++ prototype SAT solver based on DLL, which showed
a great potential for bug-finding in hardware designs at an industrial
setting. The production version, SIM, is comparable to current
state-of-the-art solvers and we plan to use it for increasing the
capacity of existing hardware verification techniques.
|