Towards Formal Verification of Real-World SystemC TLM Peripheral Models - A Case Study

Hoang M. Le, Vladimir Herdt, Daniel Große, Rolf Drechsler

In: Design, Automation and Test in Europe (DATE). Design, Automation & Test in Europe (DATE) March 14-18 Dresden Germany Seiten 1160-1163 2016.


SystemC-basedVirtual Prototypes(VPs) serve asreference models for various activities in the modern design flowand therefore, the functional correctness of each individual com-ponents and the VPs as a whole should be subjected to rigorousformal verification. In the last few years, notable progress onSystemC formal verification has been made. This paper presentsa case study on applying a recent approach to formally verifyTLM peripheral models. To the best of our knowledge, this is thefirst formal verification case study targeting this important classof VP components. First, we show how to bridge the gap betweenthe industry-accepted modeling pattern for TLM peripheralmodels and the semantics currently supported by SystemC formalverification approaches. Then, we report verification results forthe interrupt controller of the LEON3-based SoCRocket VP usedby the European Space Agency and reflect on our experiencesand lessons learned in the process.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence