1 Search Results for "Wedler, Markus"

Document

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

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

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

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.

Cite as

Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz. Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@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/entities/document/10.4230/DagSemProc.09461.4},
  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}
}

Refine by Author
1 Dreyer, Alexander
1 Greuel, Gert-Martin
1 Kunz, Wolfgang
1 Pavlenko, Evgeny
1 Seelisch, Frank
Show More...

Refine by Classification

Refine by Keyword
1 Quantifier Free logic over fixed sized bitvectors; Computer Algebra
1 SAT modulo Theory

Refine by Type
1 document

Refine by Publication Year
1 2010

1 Search Results for "Wedler, Markus"

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

Abstract

Cite as

Thanks for your feedback!

Could not send message