Formal Methods for Hardware Software Integration on RISC V Embedded Systems

on YouTube ↗19m

" summary

A complete digital stack — pipeline RISC‑V CPU plus software image — runs on an FPGA implementation connected to an Ethernet controller and a power switch to toggle a light via UDP packets; the system is written in Bedrock2 and verified in Coq. Specifications are regular‑expression logs and parameterized interfaces; proofs include compiler correctness and invariant preservation. The toolchain exhaustively verifies behavior for all inputs, parameters and steps, the Coq theorem proves the observed log matches the regex, and the device behaves as specified on hardware.

AI-written summary · about

" chapters (8)

1. 0:00The role of interfaces
2. 2:28Prototype system overview
3. 4:47Specifying system behavior
4. 7:48Formal verification with Coq
5. 10:14Proof mechanics and invariants
6. 12:56Parameterizing specifications
7. 15:12Engineering tradeoffs
8. 17:26Context and conclusion

" related talks

• 11mFast Virtual Platforms for Custom RISC-V ProcessorsZdenek Prikryl, Lukas Jünger · RISC-V at embedded world 2024
• 24mUniversal Tools for Acceleration, Timing, Integration & Machine EnhancementHasjim 'futaris' Williams · linux.conf.au 2020
• 13mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2022
• 16mIntroduction to RISC-V Processor VerificationLarry Lapides · embedded world 2023
• 16mEfficient debug and trace of RISC-V systems: a hardware/software co-design approachOana Alexandra Lazar, Henrique Mendes, Angelo Maldonado-Liu · RISC-V Summit Europe 2025
• 21mA Comparative Analysis of RISC-V Architecture Based on the RISC-V SoC DV ExperienceMoonki Jang · RISC-V Summit North America 2023
• 21mThe New Verification Ecosystem that Supports RISC-V Verification fo...Lee Moore, John Sotiropoulos · RISC-V Summit 2022
• 14mDemo: More Than Point Tools: RISC-V SolutionsLarry Lapides · RISC-V Summit North America 2025