CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
about 3200 lines of LNT code
up to 100 million states and 350 million transitions
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.
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
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
[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
Verification Solutions Team
12, rue Jules Horowitz
38019 Grenoble Cedex
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|