Publication
CrosSym: Cross-Level Verification of SystemC Peripherals using Symbolic Execution
Karl Aaron Rudkowski; Sallar Ahmadi-Pour; Rolf Drechsler
In: 28th International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS). IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS), May 5-7, 2025.
Abstract
Modern hardware design is challenged by the everincreasing 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 crosslevel. 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.