Towards Lightweight Satisfiability Solvers for Self-Verification
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
International Symposium on Embedded computing & system Design (ISED)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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 powerful
solvers have been developed in the recent decades, this
progress often still cannot cope with the exponentially increasing
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 propagation,
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.
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung
Forschungs-