Abstract:
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)