A Semantics-based Translation Method for Automated Verification of SystemC TLM Designs

SystemC has become a de-facto standard language for SoC and ASIP designs. The verification of implementation with SystemC is the key to guarantee the correctness of designs and prevent the errors from propagating to the lower levels. In this project, we attempt translate SystemC programs to formal models and use existing model checkers to implement the verification. The method we proposed is based on a semantic translation method which translates sequential execution statements described as software character to parallel execution ones which are more closely with the implementation of hardware. This kind of conversion is inevitable to verify hardware designs but is overlooked in related works. The main contribution of this work is a translation method which can preserve the semantic consistency while building SMV model for SystemC design. We present the translation rules and implement a prototype tool which supports a subset of SystemC to demonstrate the effectiveness of our method.