Hardware Verification using Monadic Second-Order Logic

Forfattere

  • David A. Basin
  • Nils Klarlund

DOI:

https://doi.org/10.7146/brics.v2i7.19509

Resumé

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 based
on 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 to
identify 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, mathematical
induction.

Downloads

Publiceret

1995-01-07

Citation/Eksport

Basin, D. A., & Klarlund, N. (1995). Hardware Verification using Monadic Second-Order Logic. BRICS Report Series, 2(7). https://doi.org/10.7146/brics.v2i7.19509

Nummer

Nr. 7 (1995): RS-07 Hardware Verification using Monadic Second-Order Logic

Sektion

Artikler

Licens

Authors who publish with this journal agree to the following terms:

    1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.

    1. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.

  1. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).