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…)
Just to add an extra point to your definition: Formal Verification and Formal methods are static styles of verification. The design isn’t run, instead we make inferences and proofs about the designs with various types of tools. An example of a common static checker for software would be checking that all the function calls and returns are of the correct type.
Regarding
I asked our CTO Claire for a comment:
Yosys is just the front-end of SymbiYosys flows. The actual work is done by various model checkers and constraint solvers, depending on the [engines] configuration in SBY files. For example, the “smtbmc” engine using an SMT solver (such as Yices or Boolector) to construct either a bounded model check or k-induction proof over a given design. The “abc pdr” engine also performs an unbounded proof, but instead of plain k-induction it uses the IC3/PDR algorithm to automatically find relevant invariants. The newer version of “btor” engines are interfacing to btor-based hw model checkers, such as btormc and cosa2.
All the engines within SymbiYosys are employing fully “automatic” SAT/SMT based methods. There have been experiments with using Yosys as front-end to interface with proof assistance like coq or isabelle/hol. But no user-facing product with a tutorial and recommended work flows have been built around this yet.
So you can choose from a range of engines to apply your proof, but it is up to you to write the formal properties that prove your design is safe, or live - or whatever you are trying to verify.
With FPGAs, we typically use either immediate assertions or SystemVerilog assertion language (SVA). SVA is much more powerful, but only available in the licensed version of the tools.
You’d either write your own properties, or you could use verification IP - like a set of properties that proves the DUT behaves properly on a bus like AXI or Wishbone.
Hope that helps? Happy to keep discussing this further.
Matt
That’s a good point, and it’s an important distinction to make. It’s extra-confusing on the software side, because there are formal methods that look very much like execution of code under different semantics to normal. Confuses me anyway…
Thanks!
I think I understand that. I guess the strongest distinction in this context is between the “fully automatic SAT/SMT solvers” and proof assistants, which really are assistants and involve a lot of human ingenuity to generate proofs. That feels like it might be less useful for hardware work anyway.
That is helpful! Thank you. I take three things from it: 1. This stuff is complicated, both on the hardware side and the software side. 2. There’s no sneaky quick way to learn about hardware formal verification. 3. The hardware and software sides are doing very similar things, but using different language to talk about them, and different tools, even though a lot of the tools come out of the same kinds of research. A quick bit of searching only turned up one group that talked about working on methods for both hardware and software (Specification and Verification Center), so I guess there really isn’t all that much overlap.
Anyway, thanks again for taking the time to answer.
One of my aims with Symbiotic EDA is to challenge some Formal stereotypes - so on that note…
It definitely can be, and is if you want to Formally verify an entire processor. However it is quite straight forward to use the Open Source tools with some verification IP to do something that sounds complex. For example GitHub - SymbioticEDA/riscv-formal: RISC-V Formal Verification Framework is VIP that can be used to prove the correctness of a RISCV processor. A simplification in this VIP is that it is only a bounded proof (rather than a full proof using induction).
No, but I am running short courses to get people up to speed doing useful stuff: https://bit.ly/seda-intro-signup. One of my favourite examples from the course I also cover in one of my videos. This proves the memory accesses of a 10 stage pipeline is safe from memory corruption with a single assertion. Not so hard to be able to make these useful, powerful and quick proofs.
Yes. And as far as I know, they often use the same back end solvers to do the work. A big part of my learning process was understanding how the solvers are put to work to make the proofs.