RWTH Aachen University
SystemC is widely used in hardware/software codesign. Although it is also used for the design of safety-critical applications, existing formal verification techniques for SystemC are still hardly used in industrial practice. The main reasons for this are scalability issues, the lacking support for many practically relevant SystemC language constructs, and that counter-examples are not always easy to use for debugging. In this paper, the authors present an approach for the formal verification of SystemC designs using the BLAST model checker.