Skip to Main content Skip to Navigation
New interface

Formal Methods for Functional Verification of Cache-Coherent System-on-Chip

Abderahman Kriouile 1, 2 
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : State-of-the-art System-on-Chip (SoC) architectures integrate many different components, such as processors, accelerators, memories, and I/O blocks. Some of those components but not all may have caches. Because the effort of validation with simulation-based techniques, as currently used in industry, grows exponentially with the complexity of the SoC, this thesis investigates the use of formal verification techniques in this context. More precisely, we use the CADP toolbox to develop and validate a generic formal model of an SoC compliant with the recent ACE specification proposed by ARM to implement system-level cache coherency. We use a constraint-oriented specification style to model the general requirements of the specification. We verify system properties on both the constrained and unconstrained model to detect the cache coherency corner cases. We take advantage of the parametrization of the proposed model to produce a comprehensive set of counterexamples of non-satisfied properties in the unconstrained model. The results of formal verification are then used to improve the industrial simulation-based verification techniques in two aspects. On the one hand, in order to generate clever semi-directed test cases from temporal logic properties, we propose a two-step approach. One step consists in generating system-level abstract test cases using model-based testing tools of the CADP toolbox. The other step consists in refining those tests into interface-level concrete test cases that can be executed at RTL level with a commercial Coverage-Directed Test Generation tool. On the other hand, we suggest to use the formal model to assess the sanity of an interface verification unit. We found that our approach helps in the transition between interface-level and system-level verification, facilitates the validation of system-level properties, and enables early detection of bugs in both the SoC and the commercial test-bench.
Complete list of metadata

Cited literature [122 references]  Display  Hide  Download
Contributor : Abderahman KRIOUILE Connect in order to contact the contributor
Submitted on : Monday, January 25, 2016 - 10:44:46 PM
Last modification on : Wednesday, July 6, 2022 - 4:14:43 AM
Long-term archiving on: : Friday, November 11, 2016 - 4:51:50 PM


  • HAL Id : tel-01258784, version 2


Abderahman Kriouile. Formal Methods for Functional Verification of Cache-Coherent System-on-Chip. Logic in Computer Science [cs.LO]. Université Grenoble Alpes, 2015. English. ⟨NNT : ⟩. ⟨tel-01258784v2⟩



Record views


Files downloads