Comparing Methods for the Cross-Level Verification of SystemC Peripherals with Symbolic Execution

TL;DR

The paper tackles the problem of cross-level verification of SystemC peripherals within virtual prototypes by proposing two opposing strategies: CrosSym, which replaces the SystemC kernel to enable symbolic execution, and SEFOS, which extends the symbolic execution engine to work with the original SystemC kernel. It provides a unified verification workflow, application-specific optimizations, and a detailed feature comparison, including an array minimization technique in SEFOS. Through extensive evaluation on four peripherals and bus-interface tests, it demonstrates that both approaches can identify errors and achieve cross-level verification with competitive runtimes, while SEFOS offers broader SystemC compatibility at the expense of higher memory and startup overhead. The work shows that cross-level symbolic verification of peripherals is feasible beyond Transaction Level Modelling (TLM) and lays groundwork for future scalability enhancements such as loop summarization and improved handling of asynchronous waiting.

Abstract

Virtual Prototypes (VPs) are important tools in modern hardware development. At high abstractions, they are often implemented in SystemC and offer early analysis of increasingly complex designs. These complex designs often combine one or more processors, interconnects, and peripherals to perform tasks in hardware or interact with the environment. Verifying these subsystems is a well-suited task for VPs, as they allow reasoning across different abstraction levels. While modern verification techniques like symbolic execution can be seamlessly integrated into VP-based workflows, they require modifications in the SystemC kernel. Hence, existing approaches modify and replace the SystemC kernel, or ignore the opportunity of cross-level scenarios completely, and would not allow focusing on special challenges of particular subsystems like peripherals. We propose CrosSym and SEFOS, two opposing approaches for a versatile symbolic execution of peripherals. CrosSym modifies the SystemC kernel, while SEFOS instead modifies a modern symbolic execution engine. Our extensive evaluation applies our tools to various peripherals on different levels of abstractions. Both tools' extensive sets of features are demonstrated for (1) different verification scenarios, and (2) identifying 300+ mutants. In comparison with each other, SEFOS convinces with the unmodified SystemC kernel and peripheral, while CrosSym offers slightly better runtime and memory usage. In comparison to the state-of-the-art, that is limited to Transaction Level Modelling (TLM), our tools offered comparable runtime, while enabling cross-level verification with symbolic execution.

Figures (5)

• Figure 1: Verification Workflow
• Figure 2: SystemC Thread Creation (PThread module)
• Figure 3: SystemC Threading (PThread module)
• Figure 4: Symbolic Execution Engine States
• Figure 5: Interaction of Symbolic Inputs and SystemC Signals