TY - GEN
T1 - Verifying SystemC TLM Peripherals using Modern C++ Symbolic Execution Tools
AU - Pieper, Pascal
AU - Herdt, Vladimir
AU - Große, Daniel
AU - Drechsler, Rolf
PY - 2022/7/10
Y1 - 2022/7/10
N2 - In this paper we propose an effective approach for verification of real-world SystemC TLM peripherals using modern C++ symbolic execution tools. We designed a lightweight SystemC peripheral kernel that enables an efficient integration with the modern symbolic execution engine KLEE and acts as a drop-in replacement for the normal SystemC kernel on pre-processed TLM peripherals. The pre-processing step essentially replaces context switches in SystemC threads with normal function calls which can be handled by KLEE. Our experiments, using a publicly available RISC-V specific interrupt controller, demonstrate the scalability and bug hunting effectiveness of our approach.
AB - In this paper we propose an effective approach for verification of real-world SystemC TLM peripherals using modern C++ symbolic execution tools. We designed a lightweight SystemC peripheral kernel that enables an efficient integration with the modern symbolic execution engine KLEE and acts as a drop-in replacement for the normal SystemC kernel on pre-processed TLM peripherals. The pre-processing step essentially replaces context switches in SystemC threads with normal function calls which can be handled by KLEE. Our experiments, using a publicly available RISC-V specific interrupt controller, demonstrate the scalability and bug hunting effectiveness of our approach.
UR - https://ics.jku.at/files/2022DAC_Verifying-SystemC-TLM-Peripherals-using-SymEx.pdf
U2 - 10.1145/3489517.3530604
DO - 10.1145/3489517.3530604
M3 - Conference proceedings
T3 - Proceedings - Design Automation Conference
SP - 1177
EP - 1182
BT - Design Automation Conference 2022
ER -