Fully automatic verification and error detection for parameterized iterative sequential circuits

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

The paper shows how iterative parametric sequential circuits, which are most relevant in practice, can be verified fully automatically. Key observation is that monadic second-order logic on strings provides an adequate level for hardware specification and implementation. This allows us to apply the corresponding decision procedure and counter-model generator implemented in the Mona verification tool, which, for the first time, yields 'push-button' verification, and error detection and diagnosis for the considered class of circuits. As illustrated by means of various versions of counters, this approach captures hierarchical and mixed mode verification, as well as the treatment of varying connectivity in iterative designs.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 2nd International Workshop, TACAS 1996, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
PublisherSpringer Verlag
Pages258-277
Number of pages20
ISBN (Print)3540610421, 9783540610427
DOIs
Publication statusPublished - 1996
Externally publishedYes
Event2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1996 - Passau, Germany
Duration: 27 Mar 199629 Mar 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1055
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1996
Country/TerritoryGermany
CityPassau
Period27/03/9629/03/96

Fingerprint

Dive into the research topics of 'Fully automatic verification and error detection for parameterized iterative sequential circuits'. Together they form a unique fingerprint.

Cite this