Deductive Verification of Parameterized Embedded Systems modeled in SystemC

on YouTube ↗21m

" summary

Provides an automated SystemC→PVL encoding that maps SystemC processes to PVL threads, modules to shared data classes, and simulates the SystemC scheduler, events and a global lock for single-threaded execution semantics, and connects to the VerCors deductive verifier. Introduces the RASI reachable abstract states invariant to capture global timing and interprocess dependencies automatically instead of an eight‑hour manual invariant, demonstrates three case studies including an automotive ABS which verifies in about 3 hours while small examples finish under a minute.

AI-written summary · about

" chapters (8)

1. 0:00Deductive verification intro
2. 2:32SystemC and Vore fundamentals
3. 5:43Transforming SystemC to PVL
4. 9:17Functional vs global properties
5. 13:50Automating invariant generation
6. 15:13Case studies and evaluation
7. 16:58Summary and future work
8. 18:22Q&A

" related talks

• 16mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2023
• 13mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2022
• 13mEarly RISC-V Software Verification with SIM-VLukas Jünger · embedded world 2023
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 17mDemo: RISC-V Models for Verification, Software Development and Architectural Explor...Larry Lapides · RISC-V Summit 2022
• 09mExploring RISC-V architectures with VPSim, a virtual prototyping environmentLilia Zaourar · RISC-V Summit Europe 2024
• 20mEarly performance estimation using virtual prototypes and open-source SWRocco Jonack · ORConf 2023
• 21mCloud-based Verification of Open Source RISC-V Cores Using the Metrics Cloud Platform and Codasip SweRV Support PackageRoddy Urquhart, Dan Ganousis · RISC-V Global Forum 2020