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 temporal logic. The approach is particularly suitable for, but not restricted to, models at a high abstraction, such as transaction-level. The efficiency of the approach is illustrated by experiments.

• Type: Conference
• Year: 2006
• Where: DATE
• Authors: Daniel Karlsson, Petru Eles, Zebo Peng
• Keywords: Approach Translates Systemc, DATE 2006, Effective Approach, Hardware, SystemC Designs