Formal Verification of SystemC Designs Using a Petri-Net Based Representation

This paper presents an effective approach to formally verify SystemC designs. The approach translates SystemC models into a Petri-Net based representation. The Petri-net model is then used for model checking of properties expressed in a timed formal verification SystemC designs Petri-net model model checking timed temporal logic . The approach is particularly suitable for, but not restricted to, models at a high level of abstraction, such as transaction-level. The efficiency of the approach is illustrated by experiments