INRIA Rhône-Alpes / VASY (FRANCE)
CEA/Léti - Minatec (GRENOBLE, FRANCE)
CHP (Communicating Hardware Processes)
CADP (Construction and Analysis of Distributed Processes)
Up to 1200 of CHP, 3600 lines of LOTOS, 750 lines of SVL, and 19
In the currently predominating synchronous approach to hardware
design, a global clock is used to synchronise all parts of a circuit.
Unfortunately, the global clock requires significant chip space and
power. Asynchronous design methodologies avoid the notion of global
clock: the different parts of an asynchronous circuit or a GALS
(Globally Asynchronous, Locally Synchronous) architecture evolve
concurrently at different speeds, with no constraints on communication
delays. The advantages of asynchronous hardware design include reduced
power consumption, enhanced modularity, and increased performance.
However, few formal verification techniques are currently available
for asynchronous hardware designs.
Hardware process calculi, such as CHP (Communicating Hardware Processes), DI-Algebra, Balsa, or Haste (formerly Tangram), allow to describe asynchronous hardware designs as concurrent processes communicating via handshake synchronisations. In these languages, there is no global clock, but each process might have its own local clock as in GALS architectures. This case-study illustrates the formal verification of a CHP specification of a communication interconnect, which routes packets (consisting of several 34-bit flits) between the components of a NoC (Network-on-Chip) designed by the CEA/Léti laboratory and described in CHP.
For each component, the interconnect has one communication node, consisting of five input and five output controllers. Each input controller dispatches incoming flits to one out of four output controllers, and each output controller arbitrates between four input controllers.
The compositional verification of an input controller uses the following steps:
Translating CHP descriptions into LOTOS enables the use of CADP for
the verification of asynchronous hardware designs. The approach has
been used successfully on an asynchronous network-on-chip, where it
allowed to exhibit a routing problem in the CHP description.
Gwen Salaün and Wendelin Serwe.
"Translating Hardware Process Algebras into Standard Process Algebras
- Illustration with CHP and LOTOS". In Proceedings of the 5th
International Conference on Integrated Formal Methods IFM 2005
(Eindhoven, The Netherlands), LNCS vol. 3771, pp. 287-306,
November - December 2005.
Available on-line from http://cadp.inria.fr/publications/Salaun-Serwe-05.html
[Salaun-Serwe-Thonnart-Vivet-07] Gwen Salaün, Wendelin Serwe, Yvain Thonnart, and Pascal Vivet. "Formal Verification of CHP Specifications with CADP - Illustration on an Asynchronous Network-on-Chip". In Proceedings of the 13th IEEE International Symposium on Asynchronous Circuits and Systems ASYNC 2007 (Berkeley, California, USA), IEEE Computer Society Press, March 2007.
Available on-line from http://cadp.inria.fr/publications/Salaun-Serwe-Thonnart-Vivet-07.html
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
38330 Montbonnot Saint-Martin
Tel: +33 (0)4 76 61 53 52
Fax: +33 (0)4 76 61 52 52
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|