Publication
Symbolic Execution of Unmodified SystemC Peripherals
Aaron Rudkowski; Sallar Ahmadi-Pour; Rolf Drechsler
In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV). ITG/GMM/GI-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV), March 11-12, Rostock, Germany, 2025.
Abstract
In the modern hardware design process, the ever-increasing complexity of designs poses a challenge. An important
step in the workflow is the verification, which aims to identify errors early on. To this end, executable models of the
design, called Virtual Prototypes (VPs), allow early and continuous verification. Current symbolic execution-based
approaches rarely consider the characteristic differences of peripherals, and none consider cross-level verification of these.
Additionally, SystemC, though a popular hardware modelling language, is either not targeted, or replaced by a heavily
limited kernel implementation. We propose the first symbolic execution engine capable of verifying unmodified SystemC
peripherals. Our tool leverages the threading behaviour specified in the SystemC standard for a light-weight PThread
support. The evaluation of a RISC-V Platform Level Interrupt Controller (PLIC) shows our approach’s effectiveness in
multiple verification scenarios.