TY - GEN
T1 - Fully automatic verification and error detection for parameterized iterative sequential circuits
AU - Margaria, Tiziana
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1996.
PY - 1996
Y1 - 1996
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84958745469&partnerID=8YFLogxK
U2 - 10.1007/3-540-61042-1_49
DO - 10.1007/3-540-61042-1_49
M3 - Conference contribution
AN - SCOPUS:84958745469
SN - 3540610421
SN - 9783540610427
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 258
EP - 277
BT - Tools and Algorithms for the Construction and Analysis of Systems - 2nd International Workshop, TACAS 1996, Proceedings
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Verlag
T2 - 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1996
Y2 - 27 March 1996 through 29 March 1996
ER -