CrosSym: Cross-Level Verification of SystemC Peripherals using Symbolic Execution

Modern hardware design is challenged by the ever-increasing complexity of designs. An important step is hardware verification, where Virtual Prototypes (VPs) can be used for a cross-level verification throughout the refinements. Peripherals are relevant targets, because they characteristically implement a wide range of integral tasks. Symbolic execution is a popular verification method, but has been applied to SystemC peripherals only once, and never for a cross-level verification. We propose CrosSym, the first method to verify peripherals at both Register Transfer Level (RTL) and Transaction Level Modelling (TLM) abstraction with symbolic execution, explicitly supporting cross-level. Our extensive evaluation explores (1) the performance costs of two abstraction levels, (2) our approach’s suitability for a full verification, using three peripherals, (3) it’s bug finding capabilities by killing over 1500 mutants in under 15 min. In the latter, most scenarios found 97+% of the observable mutations.