Kevin Marquet and
Matthieu Moy and
Bertrand Jeannet
Efficient Encoding of SystemC/TLM in Promela---Full Version (2010)
Efficient Encoding of SystemC/TLM in Promela---Full Version (2010)
TR-2010-7.pdf
Keywords:
Abstract: To deal with the ever growing complexity of Systems-on-Chip, designers use models early in the design flow. SystemC is a commonly used tool to write such models. In order to verify such models, one thriving approach is to extract a formal semantics, and then to verify this semantics with verification tools. Various encodings of SystemC into formal languages have already been proposed, with different performance implications. In this paper, we investigate a new, automatic, asynchronous means to formalize models. Our encoding supports the concurrency and communication constructs offered by SystemC. We ensure that encoded programs have the same semantics as the original one by model-checking a set of properties. We give experimental results on our formalization and compare with previous works.
