Verifying SystemC TLM Peripherals using Modern C++ Symbolic Execution Tools

  • Pascal Pieper (Speaker)
  • Große, D. (Speaker)
  • Rolf Drechsler (Speaker)
  • Vladimir Herdt (Speaker)

Activity: Talk or presentation › Contributed talk › science-to-science

Description

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.
Period14 Jul 2022
Event titleDesign Automation Conference 2022
Event typeConference
LocationUnited StatesShow on map

Fields of science

  • 202017 Embedded systems
  • 202005 Computer architecture
  • 102005 Computer aided design (CAD)
  • 102 Computer Sciences
  • 102011 Formal languages

JKU Focus areas

  • Digital Transformation

Documents & Links