What is formal verification of hardware?

Question

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?

Answer 1

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.

Answer 2

How to learn practical Formal Verification

I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the tutorials from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did as a senior year engineering undergraduate. The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles. Note that the open-source version of Symbiotic EDA does not support most SVA constructs.

Equivalence Checking Vs. Formal Verification

The other answer has mentioned formal equivalence checking, which is a kind of formal verification that checks 2 designs which may or may not be at the same abstraction level for logical / functional equivalency. For example, you can do RTL versus RTL formal equivalence checking or RTL versus gate-level netlist formal equivalence checking. Equivalence checking is one of the most common formal verification based techniques used in the semiconductor industry. Low-power formal verification and property checking are other kinds of formal verification. I have worked with property checking, so I can write a little about it.

Property Checking

Property checking is a technique where you specify properties, and the solver proves these properties are held true, either for all time i.e. induction, or for a certain number of cycles i.e. bounded model checking. 2 kinds of properties are specified: assumptions and assertions. Assumptions are properties which the solver assumes and assertions are the properties the solver needs to prove. So the problem of proving properties is represented as a SAT (Satisfiability, i.e. Boolean Satisfiability) problem, which is then solved by SAT solvers.

Limitations of Property Checking

1. SAT is NP Complete i.e. no known polynomial time algorithm to solve this problem exists. So one might expect formal verification to be slow. Yes, formal verification can be slow for large designs and the tool can "choke" when the complexity of the proofs is high, due to the system running out of memory. The good news is there are clever techniques like blackboxes, cut-points and abstractions that can be applied by the one doing formal verification to speeden the verification process and reduce memory consumption. Adding a sufficient number of assumptions restricts the solver to check a smaller search space, and increases the probability of converging to a solution.
2. The Incompleteness Theorem: The conclusion that has to be drawn from this theorem is that it is not possible to build a formal system that can be guaranteed to verify the correctness of any specifications. Tools that can solve most problems found in the real world do exist and are useful.
3. Correctness and completeness of properties: The onus of the correctness and completeness of properties specified is on the one writing the properties. Writing correct properties is not very easy and it takes time to learn to write assertions.

Suggestions for property checking

1. For a large design, it is recommended to break the problem of verifying the design into smaller, provable properties that verify the entire design. This enables the tool to use a Divide-and-Conquer approach to generate the proofs. For example, RISC-V Formal uses a set of simple properties to prove ISA compliance of RISC-V processors.
2. It is also recommended to start with Bounded model checking and then try Induction proofs. This is because bounded model checking is easier to run and debug.

Is formal verification worth it?

1. Formal verification is a somewhat challenging field, but the effort is worth it because some bugs like the Pentium Floating point division bug will most likely escape random testing, since the probability of the occurences leading to the detection of some bugs in random testing is extremely small.
2. You can't verify that your design does not hang (enter a deadlock) at some point of time using constrained random, since there are only so many cycles you can run the simulation for. Formal verification can potentially prove the correctness of the logic design at the Register Transfer Level and gate level for infinite cycles.

In the end, it's not magic, and it has its limitations like any other technology. But it is a powerful technique that leverages cutting-edge research done in mathematics, computer science and formal logic.