Induction-Based Formal Verification of SystemC TLM Designs

In this paper we present a formal verification approach for SystemC TLM designs. The approaches allows to check expressive properties and uses induction to cope with the large state space of abstract SystemC programs. The technique is tightly integrated with our SystemC-to-C transformation and generation of monitoring logic to form a complete and efficient method. Properties specifying both hardware and software aspects, e.g. pre- and post-conditions as well as temporal relations of transactions and events, can be specified. As shown by experiments our inductive technique gives significant speed-ups in comparison to simple methods.