Towards lightweight satisfiability solvers for self-verification

Fritjof Bornebusch, Robert Wille, Rolf Drechsler

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

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 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.

Original languageEnglish
Title of host publication2017 7th International Symposium on Embedded Computing and System Design, ISED 2017
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1-5
Number of pages5
ISBN (Electronic)9781538630327
DOIs
StatePublished - 2 Jul 2017
Externally publishedYes
Event7th International Symposium on Embedded Computing and System Design, ISED 2017 - Durgapur, India
Duration: 18 Dec 201720 Dec 2017

Publication series

Name2017 7th International Symposium on Embedded Computing and System Design, ISED 2017
Volume2018-January

Conference

Conference7th International Symposium on Embedded Computing and System Design, ISED 2017
Country/TerritoryIndia
CityDurgapur
Period18/12/1720/12/17

Fingerprint

Dive into the research topics of 'Towards lightweight satisfiability solvers for self-verification'. Together they form a unique fingerprint.

Cite this