Formal verification of Soc transactional models
Matthieu MOY
STMicroelectronics - Verimag
Centre équation - 2 avenue de Vignate, 38610 Gières, FRANCE

Transaction Level Modeling (TLM) has been proposed recently, as a complement to traditional RTL modeling. Some languages like SystemC 2.0 and SystemVerilog offer a support for TLM modeling. TLM allows for early development of the embedded software, and early analysis of the system architecture. We describe a formal verification method based on model-checking and abstract interpretation, able to extract information from a SystemC design, and to verify code-reachability properties. We also describe the prototype implementation.

Slides (.pdf)