|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: http://cadp.inria.fr/publications/Kahlouche-Viho-Zendri-98.html [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: http://cadp.inria.fr/publications/Kahlouche-Viho-Zendri-99.html |
| Contact: | Massimo Zendri INRIA Rhone-Alpes / Dyade 655, avenue de l'Europe F-38330 Montbonnot Saint-Martin FRANCE Tel: +33 4 76 61 53 79 Fax: +33 4 76 61 52 52 E-mail: [email protected] |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page