Publikation
SAT can Ensure Polynomial Bounds for the Verification of Circuits with Limited Cutwidth
Luca Müller; Rolf Drechsler
In: 27th Euromicro Conference Series on Digital System Design (DSD). Euromicro Conference on Digital System Design (DSD-2024), August 28-30, Paris, France, 2024.
Zusammenfassung
As hardware designs are getting more complex,
verification becomes ever more important to prevent producing
chips which do not behave according to their specification. This
increasing complexity also impacts the verification process, resulting
in a longer time-to-market. Ensuring that the verification
itself can be conducted efficiently helps facing these challenges.
Additionally, taking the efficient verification into consideration
during the design phase further enables the optimization of the
whole process.
In this paper, we present a SAT-based verification flow and
how it can ensure polynomial bounds for the verification of
circuits with limited cutwidth. To demonstrate our approach, the
flow is applied to three different adder architectures. Addition is
one of the most essential operations in digital computations and
the simplicity of its circuit realizations makes it a good starting
point to explore their efficient verification using SAT. We provide
theoretical proofs that SAT can be used for Polynomial Formal
Verification (PFV) of circuits with limited cutwidth. We then show
that for the considered adder circuits, a linear time complexity of
the verification process can be ensured and confirm our findings
by experimental evaluation with our own SAT solver.