Verification of asynchronous circuits by BDD-based model checking of Petri nets

View/Open
Cita com:
hdl:2117/133572
Document typeConference report
Defense date1995
PublisherSpringer
Rights accessOpen Access
Abstract
This paper presents a methodology for the verification of speed-independent asynchronous circuits against a Petri net specification. The technique is based on symbolic reachability analysis, modeling both the specification and the gate-level network behavior by means of boolean functions. These functions are efficiently handled by using Binary Decision Diagrams. Algorithms for verifying the correctness of designs, as well as several circuit properties are proposed. Finally, the applicability of our verification method has been proven by checking the correctness of different benchmarks.
CitationRoig, O.; Cortadella, J.; Pastor, E. Verification of asynchronous circuits by BDD-based model checking of Petri nets. A: International Conference on Application and Theory of Petri Nets. "Application and Theory of Petri Nets 1995, 16th International Conference: Turin, Italy, June 26-30, 1995: proceedings". Berlín: Springer, 1995, p. 374-391.
ISBN978-3-540-49408-9
Publisher versionhttps://link.springer.com/chapter/10.1007/3-540-60029-9_50
Collections
- Departament de Ciències de la Computació - Ponències/Comunicacions de congressos [1.138]
- ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals - Ponències/Comunicacions de congressos [309]
- CAP - Grup de Computació d'Altes Prestacions - Ponències/Comunicacions de congressos [697]
- Departament d'Arquitectura de Computadors - Ponències/Comunicacions de congressos [1.656]
Files | Description | Size | Format | View |
---|---|---|---|---|
oriol95bC.pdf | 212,3Kb | View/Open |
All rights reserved. This work is protected by the corresponding intellectual and industrial
property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public
communication or transformation of this work are prohibited without permission of the copyright holder