Publication

SAT-Lancer: A Hardware SAT-Solver for Self-Verification

Buse Ustaoglu, Sebastian Huhn, Daniel Große, Rolf Drechsler

In: 28th ACM Great Lakes Symposium on VLSI (GLVLSI). ACM Great Lakes Symposium on VLSI (GLSVLSI-2018) May 23-25 Chicago IL United States 2018.

Abstract

To close the ever widening verification gap, new powerful solutions are strictly required. One such promising approach aims in continuing verification tasks after production of a chip during its lifetime. This approach is called self-verification. However, for realizing self-verification tasks on-chip, verification packages have to be developed. In this paper, we propose the verification package SATLancer. SAT-Lancer is a compact Boolean Satisfiability (SAT) solver and has been implemented entirely on HW with the capability of solving any arbitrary SAT-instance. At the heart of SAT-Lancer is a scalable memory model, which can be adjusted to given memory constraints and allows to store the SAT-instance most effectively. In comparison to previous HW SAT-solvers, SAT-Lancer utilizes significant less area and can handle order of magnitude larger SATinstances.

Projekte

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz