Formal verification of safety properties in timed circuits
Document typeConference report
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Rights accessOpen Access
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.
CitationPeña, M. [et al.]. Formal verification of safety properties in timed circuits. A: International Symposium on Advanced Research in Asynchronous Circuits and Systems. "Sixth International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 2000): April 2-6, 2000, Eilat, Israel: proceedings". Institute of Electrical and Electronics Engineers (IEEE), 2000, p. 2-11.
- Departament de Ciències de la Computació - Ponències/Comunicacions de congressos [1.154]
- ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals - Ponències/Comunicacions de congressos 
- CAP - Grup de Computació d'Altes Prestacions - Ponències/Comunicacions de congressos 
- Departament d'Arquitectura de Computadors - Ponències/Comunicacions de congressos [1.699]
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