Verification of Generic VHDL Designs and Their Translation to Rocq

on YouTube ↗31m

" summary

Pipeline VHDL designs translate to executable Rocq functions while keeping generics uninstantiated, with automated checks that detect combinatorial loops, missing or multiple assignments, out‑of‑range integers, array-index errors and overflows for some parameter valuations. The tool uses GHDL parsing, solves edge existence with SMT queries, computes a single topological order valid for all generic instantiations, and emits generic Rocq functions. Pipeline circuits get verified by register removal, netlist unrolling and equivalence checking via ABC/Yosys; applied to an IEEE‑754 FPU case study.

AI-written summary · about

" chapters (15)

1. 0:00Hardware verification with Rocq
2. 1:52Approaches to hardware verification
3. 2:56Trade-offs in formal verification
4. 3:40Combinational VHDL to Rocq
5. 9:19Generic designs in translation
6. 13:33Simplifying VHDL signals for Rocq
7. 16:43Validating VHDL assumptions
8. 19:09Translation simplicity vs proof effort
9. 20:14Toolchain and linting
10. 20:56Reducing pipelines to combinational
11. 23:47Establishing pipeline equivalence
12. 26:13Case study: generic FPU verification
13. 27:04Q&A: pipeline verification
14. 28:49Q&A: signal value restrictions
15. 30:13Q&A: output depth uniformity