License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.09461.4
URN: urn:nbn:de:0030-drops-25096
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2509/
Go to the corresponding Portal

Wedler, Markus ; Pavlenko, Evgeny ; Dreyer, Alexander ; Seelisch, Frank ; Stoffel, Dominik ; Greuel, Gert-Martin ; Kunz, Wolfgang

Solving hard instances in QF-BV combining Boolean reasoning with computer algebra

pdf-format:
09461.WedlerMarkus.Paper.2509.pdf (0.7 MB)

Abstract

This paper describes our new satisfyability (SAT) modulo
theory (SMT) solver STABLE for the quantifier-free logic over fixed size
bit vectors. Our main application domain is formal verification
of system-on-chip (SoC) modules designed for complex computational
tasks, for example, in signal processing applications. Ensuring proper
functional behavior for such modules, including arithmetic correctness
of the data paths, is considered a very difficult problem.
We show how methods from computer algebra can be integrated into
an SMT solver such that instances can be handled where the arithmetic
problem parts are specified mixing various levels of abstraction from the
plain gate level for small highly optimized components up to the pure
word level used in high-level specifications. If the arithmetic problem
parts include multiplications such mixed problem descriptions quickly
drive current SMT solvers towards their capacity limits.
High performance data paths are often designed at a level of abstraction
that we call the arithmetic bit level (ABL). We show how ABL information,
if available in an SMT instance, can be used to transform the
decision problem into an equivalent set of variety subset problems. These
problems can be solved efficiently with techniques from computer algebra
based on Gröbner basis theory over finite rings Z/2^n . Sometimes, instances
contain problem parts at a level below the ABL using gate-level
operations. These problem parts, e.g., originate from custom-designed
arithmetic components that are highly optimized using the gate-level
constructs of a hardware description language (HDL). For such cases we
integrate a local ABL extraction technique based on local Reed-Muller
forms.

BibTeX - Entry

@InProceedings{wedler_et_al:DagSemProc.09461.4,
  author =	{Wedler, Markus and Pavlenko, Evgeny and Dreyer, Alexander and Seelisch, Frank and Stoffel, Dominik and Greuel, Gert-Martin and Kunz, Wolfgang},
  title =	{{Solving hard instances in QF-BV combining Boolean reasoning with computer algebra}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2509},
  URN =		{urn:nbn:de:0030-drops-25096},
  doi =		{10.4230/DagSemProc.09461.4},
  annote =	{Keywords: SAT modulo Theory, Quantifier Free logic over fixed sized bitvectors; Computer Algebra}
}

Keywords: SAT modulo Theory, Quantifier Free logic over fixed sized bitvectors; Computer Algebra
Collection: 09461 - Algorithms and Applications for Next Generation SAT Solvers
Issue Date: 2010
Date of publication: 17.03.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI