Verifying SystemC TLM Peripherals using Modern C++ Symbolic Execution Tools
TimeThursday, July 14th3:50pm - 4:10pm PDT
Location3000, Level 3
Event Type
Research Manuscript
Design Verification and Validation
DescriptionIn this paper we propose an effective approach for verification of real-world SystemC TLM peripherals using modern C++ symbolic execution tools. Therefore, we designed a lightweight SystemC peripheral kernel that is tailored for 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 threads with normal function calls which can be handled much more efficiently by KLEE. Our experiments using a RISC-V specific interrupt controller demonstrate the scalability and bug hunting effectiveness of our approach.