System- versus RT-Level Verification of Systems-on-Chip by Compositional Path Predicate Abstraction
Joakim Urdahl, Dominik Stoffel, Wolfgang Kunz · 2014
A formal methodology for system verification of System-on-Chip (SoC) designs is proposed. It ensures that system- level models are created which are sound abstractions of the concrete implementations at the Register Transfer Level (RTL). For each SoC module at the RTL an abstract description is obtained by path predicate abstraction. Path predicate abstraction is introduced based on the notion of operational graph coloring. It is shown to what extent the proposed abstraction mechanism is related to the notion of a stuttering bisimulation employed in the field of theorem proving. The proposed methodology, however, does not rely on theorem proving but is entirely based on standard techniques of property checking. Path predicate abstraction leads to time-abstract models that can be composed into abstract system models. Since path predicate abstraction leads to time-abstract system models there is the challenge to deal with the concurrency between the individual RTL components. We propose a compositional scheme describing the communi- cation between SoC modules independently of their individual processing speed. The composed abstract system is modeled as an asynchronous composition and can be verified using the SPIN model checker. We demonstrate the practical feasibility of our approach by two comprehensive, industrial case studies.