|
Title:
|
Verification of asynchronous circuits by BDD-based model checking of Petri nets
|
|
Author:
|
Roig Mansilla, Oriol; Cortadella, Jordi; Pastor Llorens, Enric
|
|
Other authors:
|
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. Departament d'Arquitectura de Computadors; Universitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals; Universitat Politècnica de Catalunya. CAP - Grup de Computació d'Altes Prestacions |
|
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. |
|
Abstract:
|
Peer Reviewed |
|
Subject(s):
|
-Àrees temàtiques de la UPC::Enginyeria electrònica::Microelectrònica::Circuits integrats
-Asynchronous circuits
-Petri nets
-Logic circuits
-Model check
-Boolean function
-Excitation function
-Binary decision diagram
-Symbolic model check
-Circuits asíncrons
-Petri, Xarxes de
-Circuits lògics |
|
Rights:
|
|
|
Document type:
|
Article - Submitted version
Conference Object |
|
Published by:
|
Springer
|
|
Share:
|
|
