# What is “formal verification” of hardware?

I read that testing and verification are different but in what way? I read that somebody writes theory to prove that the hardware is "correct" but how is that done? I tried reading Wikipedia and googling about it but I either end up in too advanced research (HOL4 and theoretical proofs) or brands, standards or outdated deprecated hardware abstraction layer ("HAL") that seems to be not used in general anymore.

I have created a 4-bit ALU (with Quartus) that actually works if I load the FPGA with the ALU. I used the logical primitives and wrote tests for the ALU. Now I want to learn more and understand the difference between testing and verifying in general and how to prove that an actual hardware is working correctly.

I see that ML is used in projects using HOL theorem prover. Is that something within my reach of understanding and handling if I am intermediate programmer and engineer? I know mathematics and programming but I'm not good at physics.

My ALU worked and I could test it in Quartus but I don't know what "formal verification" is. Can I do it and if yes, how and what should I learn?

I tried the proof assistant Isabelle and writing trivial theorems with HOL that I could compile and get the expected output. I don't have much experience with ML but I think I could use it since I have experience writing C, assembly and machine code.

Can you help me find what to read or answer what I should learn and study?

• Since you mention Isabelle, have you taken their intensive course – Dmitry Grigoryev Feb 3 '17 at 12:29
• @DmitryGrigoryev Thanks for mentioning it. I'm reading it now. – Niklas Feb 3 '17 at 16:50

Formal verification is state-point mapping done to ensure a schematic matches verilog or RTL model of the module. This means that for every set of inputs and states defined in the RTL model, the design is checked against the schematic to ensure that for those same inputs and states, the outputs are the same. It is a bit more cumbersome than other verification methods because it does not scale as well for large inputs and circuits, and it requires that internal state nodes also match (you could probably hack the verification config files or play with some internal settings to ignore internal state points but that is a lot more work).

Other types of verification could be symbolic (pushing through tokens representing boolean valuse or high-z states) or in some cases just testing with a large enough set of test vectors to ensure some %-age coverage for all possible cases.

• Thank you for the answer. Now I wonder if we write a verification that tests all possible inputs for a hardware, then we have covered all the cases and can we then say that we have "proved our VHDL" or "proved the Verilog" or whatever the HDL might be? Could there also be a verification similar to an inductive proof where you prove part of the design (a base-case) and then prove that adding the parts proves the theorem, then could we make an inductive proof instead of verifying all possible cases? – Niklas Jan 30 '17 at 16:58
• @DacSaunders: That would probably be considered test vector %-age coverage. And for your second question: yes. For example an entire CPU is way too large to verify at once. Instead individual modules are verified in the most stringent possible way. This bubbles up to the higher levels of abstraction (but I am less familiar with those as I work at the transistor level) – jbord39 Jan 30 '17 at 17:05
• Formal verification certainly doesn't compare VHDL or RTL to synthesized schematic. If the two sides don't match, the recommended course of action is to dump the HDL compiler you're using and get a better one. – Dmitry Grigoryev Feb 3 '17 at 11:59
• @Dmitry Grigoryev: yes, they do. Sure you would blame the hdl compiler but it is still a billion dollar mistake when making CPUs. They will just run it to cover their asses. Plus sometimes latches are inferred and there are corner cases that need to be considered. You might just do FPGA design -- please don't assume that everyone else does. Not to mention any eco work post synthesis that needs to be verified. – jbord39 Feb 4 '17 at 21:03
• @DmitryGrigoryev: Not to mention that any decent compiler is going to be running verification under the covers the whole time anyway. It doesn't change my answer: the compiler is going to check itself against the RTL constantly. Maybe you don't run it as a seperate step at the end: regardless the explanation of what formal verification is remains. One industry example is Conformal by Synopsys. Heres a wiki article for your ignorance: en.wikipedia.org/wiki/Formal_equivalence_checking – jbord39 Feb 6 '17 at 18:08