Database of Case Studies Achieved Using CADP

Formal Analysis of the ACE Cache Coherency Protocol

Organisation: STMicroelectronics (FRANCE)
CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)

Method: LNT
MCL

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

Domain: Hardware Design

Period: 2012-2014

Size: about 3200 lines of LNT code
up to 100 million states and 350 million transitions

Description: System-level cache coherency is a major challenge faced in the current system-on-chip architectures, because of their increasing complexity (mainly due to the significant number of computing units). As an alternative to current simulation-based validation, formal verification is investigated. This approach is illustrated on the ACE (AXI Coherency Extensions) cache coherency protocol, a system-level coherency protocol recently proposed by ARM.

A first step is the development of a formal LNT model of a system consisting of an ACE-compliant cache coherent interconnect, processors, and a main memory. The model is parametric and can be instantiated with different configurations (number of processors, number of cache lines, number of memory lines) and different sets of supported elementary ACE operations (currently, a representative subset of 15 operations), including an abstract operation that represents any other ACE operation. The global requirements of the ACE specification are handled using a constraint oriented programming style, i.e., by representing each global requirement as a dedicated process observing the global behaviour and inhibiting incorrect executions.

The second step is the generation of the LTSs corresponding to several configurations. Two liveness properties in MCL express that each read (respectively write) transaction is executed until its termination. Two further properties express cache coherence and data integrity. These required to transform state-based properties into action-based properties, by adding information about the cache state to actions executed by the cache. For all considered configurations, all these properties were checked using parametric SVL scripts (about 100 lines) and EVALUATOR. For some scenarios without the processes representing the global requirements, EVALUATOR generated counterexamples for the cache coherence and data integrity.

Conclusions: The LNT model has been found valuable by STMicroelectronics architects, because it enables interactive and backtrackable step-by-step system-level simulation (using the OCIS tool) of all ACE-compliant behaviors.

Publications: [Kriouile-Serwe-13] Abderahman Kriouile and Wendelin Serwe. "Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip". Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2013), volume 8187 of Lecture Notes in Computer Science, pages 108-122, Springer-Verlag, September 2013.
Available on-line from
http://cadp.inria.fr/publications/Kriouile-Serwe-13.html

[Kriouile-Serwe-15] Abderahman Kriouile and Wendelin Serwe. "Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip". Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume 9035 of Lecture Notes in Computer Science, pages 708-722, Springer-Verlag, April 2015.
Available on-line from
http://cadp.inria.fr/publications/Kriouile-Serwe-15.html

Contact:
Abderahman Kriouile
Verification Solutions Team
STMicroelectronics
12, rue Jules Horowitz
B.P. 217
38019 Grenoble Cedex
FRANCE
E-mail: Abderahman.Kriouile@st.com
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