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.


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.


2018GLSVLSI_SAT-Lancer.pdf (pdf, 638 KB)

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