Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Beyond the finite in automatic hardware verification

Basin, David A. and Klarlund, Nils

MPI-I-96-2-009. October 1996, 51 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
We present a new approach to hardware verification based on describing
circuits in Monadic Second-order Logic MSL. We show how to use
this logic to represent generic designs like n-bit adders, which are
parameterized in space, and sequential circuits, where time is an
unbounded parameter. MSL admits a decision procedure, implemented in
the MONA tool, which reduces formulas to canonical automata.

The decision problem for MSL is non-elementary decidable and
thus unlikely to be usable in practice. However, we have used
MONA to automatically verify, or find errors in, a number of
circuits studied in the literature. Previously published machine
proofs of the same circuits are based on deduction and may involve
substantial interaction with the user. Moreover, our approach is
orders of magnitude faster for the examples considered. We show why
the underlying computations are feasible and how our use of
MONA generalizes standard BDD-based hardware reasoning.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-96-2-009.ps474 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Basin, David A. and Klarlund, Nils},
  TITLE = {Beyond the finite in automatic hardware verification},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-96-2-009},
  MONTH = {October},
  YEAR = {1996},
  ISSN = {0946-011X},