A case study for the verification of complex timed circuits: IPCMOS
Document typeConference report
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Rights accessOpen Access
The verification of a n-stage pulse-driven IPCMOS pipeline, for any n>0, is presented. The complexity of the system is 32n transistors and delay information is provided at the level of transistor The correctness of the circuit highly depends on the timed behavior of its components and the environment. To verify the system, three techniques have been combined: (1) relative-timing-based verification from absolute timing information, (2) assume-guarantee reasoning to verify untimed abstractions of timed components and (3) mathematical induction to verify pipelines of any length. Even though the circuit can interact with pulse-driven environments, the internal behavior between stages commits a handshake protocol that enables the use of untimed abstractions. The verification not only reports a positive answer about the correctness of the system, but also gives a set of sufficient relative-timing constraints that determine delay slacks under which correctness can be maintained.
CitationPeña, M. [et al.]. A case study for the verification of complex timed circuits: IPCMOS. A: Design, Automation and Test in Europe Conference and Exhibition. "2002 Design, Automation and Test in Europe Conference and Exhibition: March 4-8, 2002, Paris, France: proceedings". Institute of Electrical and Electronics Engineers (IEEE), 2002, p. 44-51.
- Departament de Ciències de la Computació - Ponències/Comunicacions de congressos [1.104]
- 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.541]
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