The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Validation de Spécifications de Circuits Asynchrones: Méthodes et outils
Asynchronous designs aim at answering the increasingly complex problems (clock distribution, energy, modularity) encountered by synchronous circuit designers. Asynchronous circuits, contrary to synchronous circuits, are not ordered by a global clock. Even medium size asynchronous circuits may display a complex behavior, due to the combinational explosion in the chronology of events that may happen. It is thus essential to apply rigorous design and validation methods. This thesis addresses the analysis and the automatic validation of asynchronous circuit specifications written in the CHP language, before their synthesis with the TAST asynchronous design flow developed by the CIS group at TIMA. Two approaches are proposed. The first adapts symbolic model checking, originally dedicated to synchronous circuits, to the verification of asynchronous circuits: circuit specifications are translated into a pseudo-synchronous VHDL model and then verified by industrial symbolic model checking tools. In the second approach, the semantics of CHP, originally given in terms of Petri nets, is reformulated in terms of Extended Labelled Transition Systems, and circuit specifications are validated by enumerative model checking methods. To improve the performance of the enumerative approach and address the state explosion problem, a number of automatic reduction and abstraction techniques were developed and implemented.
A copy is held
pdf, 3.1 MB. Not published — it may be under
copyright. The facts and links here are.
@phdthesis{boubekeur2004validation,
title = {Validation de Spécifications de Circuits Asynchrones: Méthodes et outils},
author = {Menouer Boubekeur},
year = {2004},
school = {Université Joseph-Fourier, Grenoble I},
}