Database of Case Studies Achieved Using CADP

CC-NUMA Cache Coherency Protocol.

Organisation: INRIA Rhone Alpes / DYADE (Bull-INRIA Joint Venture for Advanced Research)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)
TGV (Test Generation with Verification technology)

Domain: Hardware Design.

Period: 1998.

Size: 2,000 lines of code (50% for the data part, 50% for the control part).

Description: This end-to-end industrial case-study concerns the automatic generation of test suites for the cache coherency protocol of Bull's CC-NUMA (Cache-Coherent Non Uniform Memory Architecture) multiprocessor architecture. Bull's CC-NUMA consists of a scalable interconnection of modules, the memory being distributed among different modules. The key feature of Bull's architecture is its distributed directory-based cache coherency protocol, which uses a Presence Cache and a Remote Cache in each module.

A formal specification in LOTOS of Bull's CC-NUMA cache coherency protocol (for two modules) has been produced, checked using the CADP verification tools, and subsequently used as the reference model of the system.

The test purposes of the cache coherency protocol (defined in the test plan of the architecture) have been formally described as finite-state automata represented in ALDEBARAN format. From these test purposes and the LOTOS specification of the protocol, the corresponding abstract test cases (i.e., independent from any testing environment) have been automatically generated using TGV.

In order to use the abstract test cases produced by TGV in Bull's testing environment, a new tester package has been developed, which connects TGV to the Synopsys VHDL testing environment. Using this new tester package, the abstract test suites of the CC-NUMA cache coherency protocol have been successfully executed in Bull's testing environment.

Conclusion: Description languages like LOTOS appear to be well-suited for the specification of hardware entities (processors, memory controllers, bus arbiters, etc.) and their interconnections, which are better modelled by interactions between LOTOS processes rather than infinite FIFO queues as in SDL.

Furthermore, this study demonstrates that tools designed for protocol conformance testing can be efficiently used to generate executable tests for hardware concurrent systems.

Publications: [Kahlouche-Viho-Zendri-98] Hakim Kahlouche, Cesar Viho, and Massimo Zendri. "An Industrial Experiment in Automatic Generation of Executable Test Suites for a Cache Coherency Protocol". In: Proceedings of the International Workshop on Testing of Communicating Systems IWTCS'98 (Tomsk, Russia), September 1998.

Available on-line at:

[Kahlouche-Viho-Zendri-99] Hakim Kahlouche, Cesar Viho, and Massimo Zendri. "Hardware Testing using a Communication Protocol Conformance Testing Tool" In: Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'99 (Amsterdam, The Netherlands), March 1999.

Available on-line at:
Massimo Zendri
INRIA Rhone-Alpes / Dyade
655, avenue de l'Europe
F-38330 Montbonnot Saint-Martin
Tel: +33 4 76 61 53 79
Fax: +33 4 76 61 52 52

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Mon Apr 18 14:50:14 2022.

Back to the CADP case studies page