European Design and Automation Association
Embedded electronic devices are often highly safety critical, such as in automotive and avionics applications or medical equipment. It is both very error-prone and time-consuming to design these complex systems. 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 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.