They're the Same Picture: A Software-Verification Flow Adapted for Hardware Verification

Explore a 15-minute conference talk from ACM SIGPLAN that delves into adapting software verification techniques for hardware verification. Learn how researchers from Imperial College London and Chalmers University of Technology have applied the functional-programming-based software verification flow from the CakeML project to Verilog hardware verification. Discover the similarities and differences between software and hardware verification, and gain insights into the potential for increased technology transfer between these traditionally separate fields. The talk covers topics such as the KML ecosystem, synthesis tools, simulation-synthesis mismatches, and the formalization of Pro Standards. Understand how this innovative approach, implemented using the HOL4 interactive theorem prover, aims to bridge the gap between software and hardware verification methodologies.

Intro
Context
Motivation
Flow
Synthesis tools
Software verification flow
KML ecosystem
The flow
Hardware verification
Differences
Simulationsynthesis mismatches
Why Verilog
Formalizing Pro Standards
Formal Semantic Visualization
Conclusion