Publication
Towards Lightweight Satisfiability Solvers for Self-Verification
Fritjof Bornebusch; Robert Wille; Rolf Drechsler
In: 7th International Symposium on Embedded Computing and System Design. International Symposium on Electronic System Design (ISED-17), 7th, December 18-20, Durgapur, India, 2017.
Abstract
Solvers for Boolean satisfiability (SAT solvers) are
essential for various hardware and software verification tasks
such as equivalence checking, property checking, coverage
analysis, etc. Nevertheless, despite the fact that very power-
ful solvers have been developed in the recent decades, this
progress often still cannot cope with the exponentially increas-
ing complexity of those verification tasks. As a consequence,
researchers and engineers are investigating complementarily
different verification approaches which require changes in the
core methods as well. Self-verification is such a promising
approach where e.g. SAT solvers have to be executed on the
system itself. This comes with hardware restrictions such as
limited memory and motivates lightweight SAT solvers. This
work provides a case study towards the development of such
solvers. To this end, we consider several core techniques of SAT
solvers (such as clause learning, Boolean constraint propaga-
tion, etc.) and discuss as well as evaluate how they contribute to
both, the run-time performance but also the required memory
requirements. The findings from this case study provide a basis
for the development of dedicated, i.e. lightweight, SAT solvers
to be used in self-verification solutions.