A Practical Approach to the Formal Verification of SoCs with Symbolic Model-Checking

Emil Dumitrescu (1, 2)

1 AMPERE - Ampère
2 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time

The successful application of model-checking to industrial designs calls for a minimal set of efficiency criteria. This work addresses these issues, based on the linear-time model-checking verification of an instruction cache controller designed by ST Microelectronics.

Mots clés: Systèmes sur une puce; Systèmes embarqués; Vérification formelle

Domaines: Automatique / Robotique; Systèmes embarqués

Emil Dumitrescu. A Practical Approach to the Formal Verification of SoCs with Symbolic Model-Checking. 2003. ⟨hal-00419534⟩