CheckSyC: An Efficient Property Checker for RTL SystemC Designs
Daniel J. Grosse, Rolf Drechsler · 2005
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.