Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs

A formal methodology for system verification of system-on-chip (SoC) designs is proposed. It ensures that system-level models are created that 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 system models that can be composed into abstract system models. We demonstrate the practical feasibility of our approach by two comprehensive industrial case studies.