Model checking on TLM-2.0 IPs through automatic TLM-to-RTL synthesis

Transaction-level modeling (TLM) is the leading design style to deal with the increasing complexity of modern embedded systems. TLM provides designers with high-level interfaces and communication protocols for abstract modeling and efficient simulation of system platforms. The Open SystemC Initiative (OSCI) has recently released the TLM-2.0 standard for facilitating the interchange of models between suppliers and users, and thus encouraging the use of virtual platforms for fast simulation prior to the availability of register-transfer level (RTL) code. On the other hand, verification of TLM IPs still relies on simulation-based techniques since formal verification methodologies (such as model checking) and tools are not mature enough to be applied at TLM level. In this paper, we propose a methodology to apply existing RTL model checkers for verifying TLM IPs. The methodology relies on the automatic synthesis of the TLM IP models into equivalent RTL descriptions, in order to verify the TLM properties through the equivalent RTL model of the IPs.