I should probably tag this as “paging @mattvenn”… I know it’s of interest to at least one other person on here though, so I’ll make it a normal post.
I’ve been watching some of Matt’s formal verification videos on YouTube, and I’ve been trying to work out what relationship there is, if any, between what FPGA people call “formal verification” and what software people call “formal methods”.
“Formal methods” is a bit of a catch-all term for everything ranging from advanced type systems to full automated proof systems, but I guess a common characteristic of all these methods is that you choose some sort of logic model for the programming language you write programs in, and you develop proof techniques that allow you to prove certain properties of your programs. The strongest example I know of is the Coq system, which has a ridiculously powerful type system where, more or less, if you can write a program with the right type, you’ve automatically proved the properties you encode in the type.
So, there are obvious parallels to the kind of formal verification you do in Verilog. But the proof model used in things like Yosys seems quite weak compared to that in tools like Coq: bounded search + induction with bounded chains of states (plus stuff I don’t know about, probably). Is that just a matter of what’s practical for digital design?
I know that there’s at least one group using Coq for hardware verification (https://github.com/sifive/kami), but is there any more theoretical overlap? (Selfishly: overlap I can use to leverage my rather small knowledge of software formal methods to improve my entirely negligible knowledge of hardware formal verification…)