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.
Document type :
Theses
Logic in Computer Science [cs.LO]. Université Grenoble Alpes, 2015. English
Liste complète des métadonnées

Cited literature [122 references]  Display  Hide  Download

https://hal.inria.fr/tel-01258784
Contributor : Abderahman Kriouile <>
Submitted on : Monday, January 25, 2016 - 10:44:46 PM
Last modification on : Monday, February 8, 2016 - 10:54:25 AM
Document(s) archivé(s) le : Friday, November 11, 2016 - 4:51:50 PM

Identifiers

  • HAL Id : tel-01258784, version 2

Collections

Citation

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

Share

Metrics

Record views

322

Files downloads

173