S.: An Approach for the Verification of SystemC Designs Using AsmL

Abstract. The spectacular advancement in microelectronics resulted in the creation of new system level design languages, such as SystemC, which put fourth new design and verification challenges. In this paper, we present an approach verifying SystemC designs using model check-ing and assertion based verification. Such verification is enabled through two transformations from SystemC to AsmL (the Abstract State Ma-chines Language) and vice-versa. The soundness of these transforma-tions, proved using abstract interpretation, guarantees the correctness of the model checking results and the validity of the generated assertion monitors (to be checked by simulation). We illustrate our approach on the SystemC/AsmL modeling and verification of the widely used Accel-erated Graphics Port (AGP) standard. The verified AGP model can be either refined to implement an AGP core or used to validate existent compatible device.