Title :
Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs
Author :
Urdahl, Joakim ; Stoffel, Dominik ; Kunz, Wolfgang
Author_Institution :
Dept. of Electr. & Comput. Eng., Univ. of Kaiserslautern, Kaiserslautern, Germany
Abstract :
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.
Keywords :
graph colouring; integrated circuit design; system-on-chip; RT-level circuit designs; SoC; abstract description; graph coloring; path predicate abstraction; register transfer level; sound system-level models; stuttering bisimulation; system-on-chip; theorem proving; Abstracts; Color; Concrete; Integrated circuit modeling; Logic gates; Standards; System-on-chip; Abstraction; formal verification; property checking; system-level design;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2013.2285276