max planck institut
informatik
informatik
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.
Acknowledgement:
References to related material:
| To download this research report, please select the type of document that fits best your needs. | Attachement Size(s): |
|---|---|
| 474 KBytes | |
| Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView | |
BibTeX