Since 2014
Hardware Verification using Monadic Second-Order Logic
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Hardware Verification using Monadic Second-Order Logic
|
|
| Creator |
Basin, David A.
Klarlund, Nils |
|
| Description |
We show how the second-order monadic theory of strings can be used to specify hardware components and their behavior. This logic admits a decision procedure and counter-model generator basedon canonical automata for formulas. We have used a system implementing these concepts to verify, or find errors in, a number of circuits proposed in the literature. The techniques we use make it easier toidentify regularity in circuits, including those that are parameterized or have parameterized behavioral specifications. Our proofs are semantic and do not require lemmas or induction as would be needed when employing a conventional theory of strings as a recursive data type.Keywords: Monadic second order logic, automatic theorem proving, hardware verification, mathematicalinduction.
|
|
| Publisher |
Aarhus University
|
|
| Contributor |
—
|
|
| Date |
1995-01-07
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion — |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/19509
10.7146/brics.v2i7.19509 |
|
| Source |
BRICS Report Series; No 7 (1995): RS-07 Hardware Verification using Monadic Second-Order Logic
BRICS Report Series; No 7 (1995): RS-07 Hardware Verification using Monadic Second-Order Logic 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/19509/17131
|
|
| Rights |
Copyright (c) 2014 BRICS Report Series
|
|