|
Título:
|
Formal verification of safety properties in timed circuits
|
|
Autor/a:
|
Peña Basurto, Marco Antonio; Cortadella, Jordi; Kondratyev, Alex; Pastor Llorens, Enric
|
|
Otros autores:
|
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:
|
The incorporation of timing makes circuit verification computationally expensive. This paper proposes a new approach for the verification of timed circuits. Rather than calculating the exact timed stare space, a conservative overestimation that fulfills the property under verification is derived. Timing analysis with absolute delays is efficiently performed at the level of event structures and transformed into a set of relative timing constraints. With this approach, conventional symbolic techniques for reachability analysis can be efficiently combined with timing analysis. Moreover the set of timing constraints used to prove the correctness of the circuit can also be reported for backannotation purposes. Some preliminary results obtained by a naive implementation of the approach show that systems with more than 10/sup 6/ untimed states can be verified. |
|
Abstract:
|
Peer Reviewed |
|
Materia(s):
|
-Àrees temàtiques de la UPC::Enginyeria electrònica::Microelectrònica::Circuits integrats
-Asynchronous circuits
-Electronic circuit design
-Formal verification
-Safety
-Circuits
-Timing
-State-space methods
-Delay effects
-Computer architecture
-Logic
-Lakes
-Drives
-Circuits asíncrons
-Circuits electrònics -- Disseny i construcció |
|
Derechos:
|
|
|
Tipo de documento:
|
Artículo - Versión publicada
Objeto de conferencia |
|
Editor:
|
Institute of Electrical and Electronics Engineers (IEEE)
|
|
Compartir:
|
|
