Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP

Abderahman Kriouile and Wendelin Serwe

Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2013 (Madrid, Spain)

Abstract: System-on-Chip (SoC) architectures integrate now many different components, such as processors, accelerators, memory, and I/O blocks, some but not all of which may have caches. Because the validation effort with simulation-based validation techniques, as currently used in industry, grows exponentially with the complexity of the SoC, we investigate in this paper the use of formal verification techniques. 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 coherency.

15 pages

PDF

PostScript

Slides of A. Kriouile's lecture at FMICS'2013:

PDF