research-article

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

Authors:

Buse Ustaoglu,

Sebastian Huhn,

Daniel Große,

Rolf DrechslerAuthors Info & Claims

GLSVLSI '18: Proceedings of the 2018 Great Lakes Symposium on VLSI

Pages 479 - 482

https://doi.org/10.1145/3194554.3194643

Published: 30 May 2018 Publication History

Get Access

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 verification package SAT-Lancer. 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 SAT-instances.

References

[1]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. 1999. Symbolic model checking without BDDs. In TACAS. 193--207.

Digital Library

Google Scholar

[2]

John D. Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang. 2008. A Practical Reconfigurable Hardware Accelerator for Boolean Satisfiability Solvers DAC. 780--785.

Digital Library

Google Scholar

[3]

M. Davis, G. Logeman, and D. Loveland. 1962. A Machine Program for Theorem Proving. Comm. of the ACM Vol. 5 (1962), 394--397.

Digital Library

Google Scholar

[4]

M. Davis and H. Putnam. 1960. A computing procedure for quantification theory. J. ACM Vol. 7 (1960), 506--521.

Digital Library

Google Scholar

[5]

R. Drechsler, M. Fr"anzle, and R. Wille. 2015. Envisioning self-verification of electronic systems ReCoSoC.

Google Scholar

[6]

R. Drechsler, H. M. Le, and M. Soeken. 2014. Self-verification as the key technology for next generation electronic systems SBCCI. 1--4.

Digital Library

Google Scholar

[7]

N. Eén and N. Sörensson. 2004. An extensible SAT solver. In Theory and Applications of Satisfiability Testing (LNCS), Vol. Vol. 2919. 502--518.

Google Scholar

[8]

K. Gulati, M. Waghmode, S. P. Khatri, and W. Shi. 2008. Efficient, scalable hardware engine for Boolean satisfiability and unsatisfiable core extraction. IET Computers Digital Techniques Vol. 2, 3 (2008), 214--229.

Crossref

Google Scholar

[9]

T. Ivan and E. M. Aboulhamid. 2013. An Efficient Hardware Implementation of a SAT Problem Solver on FPGA DSD. 209--216.

Digital Library

Google Scholar

[10]

Christoph Lüth, Martin Ring, and Rolf Drechsler. 2017. Towards a Methodology for Self-Verification. In ICRITO.

Google Scholar

[11]

Walden C. Rhines. 2016. Design Verification Challenges: Past, Present and Future DVCon US Keynote Address.

Google Scholar

[12]

M. Safar, M. W. El-Kharashi, M. Shalan, and A. Salem. 2011. A reconfigurable, pipelined, conflict directed jumping search SAT solver DATE. 1--6.

Google Scholar

[13]

J. Thong and N. Nicolici. 2013. FPGA acceleration of enhanced boolean constraint propagation for SAT solvers ICCAD. 234--241.

Digital Library

Google Scholar

[14]

J. Thong and N. Nicolici. 2015. SAT solving using FPGA-based heterogeneous computing ICCAD. 232--239.

Digital Library

Google Scholar

Cited By

View all

Shirinzadeh FDeb AShirinzadeh SKole ADatta KDrechsler R(2024)In-Memory SAT-Solver for Self-Verification of Programmable Memristive Architectures2024 37th International Conference on VLSI Design and 2024 23rd International Conference on Embedded Systems (VLSID)10.1109/VLSID60093.2024.00070(384-389)Online publication date: 6-Jan-2024
https://doi.org/10.1109/VLSID60093.2024.00070
Jha CQayyum KÇağlar Coşkun KSingh SHassan MLeupers RMerchant FDrechsler R(2024) veriSIMPLER : An Automated Formal Verification Methodology for SIMPLER MAGIC Design Style Based In-Memory Computing IEEE Transactions on Circuits and Systems I: Regular Papers10.1109/TCSI.2024.342468271:9(4169-4179)Online publication date: Sep-2024
https://doi.org/10.1109/TCSI.2024.3424682
Chen YChen SLin S(2023)SMT Solver With Hardware AccelerationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.320955042:6(2055-2068)Online publication date: 1-Jun-2023
https://dl.acm.org/doi/10.1109/TCAD.2022.3209550
Show More Cited By

Index Terms

SAT-Lancer: A Hardware SAT-Solver for Self-Verification
1. Hardware
  1. Hardware validation
    1. Functional verification

Recommendations

Size complexity of rotating and sweeping automata

We examine the succinctness of one-way, rotating, sweeping, and two-way deterministic finite automata (1DFAs, RDFAs, SDFAs, 2DFAs) and their nondeterministic and randomized counterparts. Here, a SDFA is a 2DFA whose head can change direction only on the ...
A Self-Testing Group-Parity Prediction Checker and Its Use for Built-In Testing

This correspondence demonstrates a new kind of error-checking scheme for multioutput combinational circuits and its use for a built-in testing method. In the error-checking logic employed, the output from the circuits being checked is partitioned into ...
MDG-SAT: an automated methodology for efficient safety checking

Multiway decision graph (MDG) is a canonical representation of a subset of many-sorted first-order logic. It generalises the logic of equality with abstract types and uninterpreted function symbols. The area of satisfiability (SAT) has been the subject ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

GLSVLSI '18: Proceedings of the 2018 Great Lakes Symposium on VLSI

May 2018

533 pages

ISBN:9781450357241

DOI:10.1145/3194554

General Chair:
Deming Chen
University of Illinois, USA
,
Program Chairs:
Houman Homayoun
George Mason University, USA
,
Baris Taskin
Drexel University, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 May 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Best Poster

Author Tags

Qualifiers

Research-article

Funding Sources

German Federal Ministry of Education and Research (BMBF)
German Research Foundation (DFG)

Conference

GLSVLSI '18

Sponsor:

SIGDA

GLSVLSI '18: Great Lakes Symposium on VLSI 2018

May 23 - 25, 2018

IL, Chicago, USA

Acceptance Rates

GLSVLSI '18 Paper Acceptance Rate 48 of 197 submissions, 24%;

Overall Acceptance Rate 312 of 1,156 submissions, 27%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
222
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)5

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Shirinzadeh FDeb AShirinzadeh SKole ADatta KDrechsler R(2024)In-Memory SAT-Solver for Self-Verification of Programmable Memristive Architectures2024 37th International Conference on VLSI Design and 2024 23rd International Conference on Embedded Systems (VLSID)10.1109/VLSID60093.2024.00070(384-389)Online publication date: 6-Jan-2024
https://doi.org/10.1109/VLSID60093.2024.00070
Jha CQayyum KÇağlar Coşkun KSingh SHassan MLeupers RMerchant FDrechsler R(2024) veriSIMPLER : An Automated Formal Verification Methodology for SIMPLER MAGIC Design Style Based In-Memory Computing IEEE Transactions on Circuits and Systems I: Regular Papers10.1109/TCSI.2024.342468271:9(4169-4179)Online publication date: Sep-2024
https://doi.org/10.1109/TCSI.2024.3424682
Chen YChen SLin S(2023)SMT Solver With Hardware AccelerationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.320955042:6(2055-2068)Online publication date: 1-Jun-2023
https://dl.acm.org/doi/10.1109/TCAD.2022.3209550
Hildebrandt MSchmitz KDrechsler R(2023)Modulares und rekonfigurierbares Systemdesign für UnterwasserfahrzeugeKI-Technologie für Unterwasserroboter10.1007/978-3-031-42369-7_5(65-76)Online publication date: 5-Dec-2023
https://doi.org/10.1007/978-3-031-42369-7_5
Narasimharaju DRao RWaingade AYasin ACiesielski M(2020)Dual Approach to Solving SAT in Hardware2020 15th Design & Technology of Integrated Systems in Nanoscale Era (DTIS)10.1109/DTIS48698.2020.9081088(1-6)Online publication date: Apr-2020
https://doi.org/10.1109/DTIS48698.2020.9081088
Ring MBornebusch FLuth CWille RDrechsler R(2019)Better Late Than Never : Verification of Embedded Systems After Deployment2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE.2019.8714967(890-895)Online publication date: Mar-2019
https://doi.org/10.23919/DATE.2019.8714967
Ustaoglu BHuhn SSill Torres FGrosse DDrechsler R(2019)SAT-Hard: A Learning-Based Hardware SAT-Solver2019 22nd Euromicro Conference on Digital System Design (DSD)10.1109/DSD.2019.00021(74-81)Online publication date: Aug-2019
https://doi.org/10.1109/DSD.2019.00021
Hildebrandt MSchmitz KDrechsler R(2019)Modular and Reconfigurable System Design for Underwater VehiclesAI Technology for Underwater Robots10.1007/978-3-030-30683-0_5(59-69)Online publication date: 24-Oct-2019
https://doi.org/10.1007/978-3-030-30683-0_5
Ring MLüth C(2019)Let’s Prove It Later—Verification at Different Points in TimeSoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_24(454-468)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_24

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Size complexity of rotating and sweeping automata

A Self-Testing Group-Parity Prediction Checker and Its Use for Built-In Testing

MDG-SAT: an automated methodology for efficient safety checking