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?
Best Answer
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.