|
Title:
|
A case study for the verification of complex timed circuits: IPCMOS
|
|
Author:
|
Peña Basurto, Marco Antonio; Cortadella, Jordi; Pastor Llorens, Enric; Smirnov, Alexandre
|
|
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:
|
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. |
|
Abstract:
|
Peer Reviewed |
|
Subject(s):
|
-Àrees temàtiques de la UPC::Enginyeria electrònica::Microelectrònica::Circuits integrats
-Logic design
-Integrated circuits
-Computer aided software engineering
-Timing
-Pipelines
-Delay
-Clocks
-Pulse circuits
-Automata
-Computer architecture
-Explosions
-Encoding
-Estructura lògica
-Circuits integrats |
|
Rights:
|
|
|
Document type:
|
Article - Published version
Conference Object |
|
Published by:
|
Institute of Electrical and Electronics Engineers (IEEE)
|
|
Share:
|
|
