Database of Case Studies Achieved Using CADP

Verification of an Asynchronous Network-on-Chip

Organisation: INRIA Rhône-Alpes / VASY (FRANCE)
CEA/Léti - Minatec (GRENOBLE, FRANCE)

Method: CHP (Communicating Hardware Processes)
LOTOS
mu-calculus

Tools used: CADP (Construction and Analysis of Distributed Processes)
CHP2LOTOS

Domain: Hardware Design.

Period: 2005-2006

Size: Up to 1200 of CHP, 3600 lines of LOTOS, 750 lines of SVL, and 19 concurrent processes.

Description: 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:
  1. First, applying the idea of data independence, the potential state space is reduced from 10^25 to 5*10^16 states by setting parts of the flits to a fixed bit pattern. To further reduce the state space to a manageable size, several scenarios (sequences of 4 flits) are carefully chosen according to the properties to be verified (e.g., data integrity and correct routing of flits/packets).
    These two reductions were obtained by introducing additional CHP processes, called "traffic generators", which restrict the environment of the input controller by providing meaningful inputs only. Applying the CHP2LOTOS translator [Salaun-Serwe-05] to the CHP description of the input controller connected to each traffic generator, we produced a set of LOTOS specifications in less than one second.
  2. Second, for each LOTOS specification, the corresponding state space is generated compositionally using a generic SVL script (41 steps); for a typical scenario, the generated state space had 1,300 states and 3,116 transitions, and the largest intermediate state space had 295,893 states and 812,283 transitions.
  3. Third, seven properties, such as absence of deadlocks, correctness of the communication protocol, integrity of the transmitted data, and correctness of flit/packet routing, are verified using BISIMULATOR, BCG_MIN, and EVALUATOR. These verification steps were automated using an SVL script.
This allowed to exhibit a routing error in the CHP description. Although this error had been already found (and fixed) manually during the synthesis of the circuit (it required more than 500,000 steps to replay the error in a native simulator for CHP), the approach based on translation to LOTOS and CADP allowed to detect the error automatically in less than 15 minutes.

Conclusions: 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.

Publications: [Salaun-Serwe-05] 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
Contact:
Wendelin Serwe
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
38330 Montbonnot Saint-Martin
FRANCE
Tel: +33 (0)4 76 61 53 52
Fax: +33 (0)4 76 61 52 52
Email: [email protected]
Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Fri Jul 20 18:02:10 2018.

Back to the CADP case studies page