An Executable Semantics of SystemC Transaction Level Models and Its Applications with VERDS

Transaction level modeling (TLM) is a high-level approach to modeling digital systems where details of communication are separated from the details of computation. In SystemC transaction level models, modules communicate through function calls provided by channels, which include primitive channels and hierarchical channels. This work extends the semantics of simple SystemC models in previous work to support the key concepts of SystemC transaction level models and presents a tool to transform SystemC source codes in TLM-1.0 to transition systems for the purpose of verification on symbolic model checker VERDS. Our approach is demonstrated through a case study of an abstract bus implemented in TLM-1.0 of SystemC.