CheckSyC: an efficient property checker for RTL SystemC designs

To cope with the increasing complexity of today´s circuits and systems, new design methodologies are needed. Modeling at higher levels of abstraction and hardware/software integration become more and more important. A language that offers this features is SystemC, a C++ class library. Besides efficient modeling, the correct functional behavior has to be ensured. We present a property checker, CheckSyC, for SystemC descriptions on the register transfer level (RTL). A SystemC design and a temporal property are converted into a satisfiability (SAT) problem. If the SAT problem is unsatisfiable, the property holds. To demonstrate the efficiency of CheckSyC, different designs are studied.