0
\$\begingroup\$

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?

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

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.

\$\endgroup\$
  • \$\begingroup\$ 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? \$\endgroup\$ – Niklas Rosencrantz Jan 30 '17 at 16:58
  • 2
    \$\begingroup\$ @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) \$\endgroup\$ – jbord39 Jan 30 '17 at 17:05
  • 2
    \$\begingroup\$ 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. \$\endgroup\$ – Dmitry Grigoryev Feb 3 '17 at 11:59
  • 1
    \$\begingroup\$ @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. \$\endgroup\$ – jbord39 Feb 4 '17 at 21:03
  • \$\begingroup\$ @DmitryGrigoryev: Thanks for the downvote but I can assure you that you are wrong. No one is going to "skip running verification" because "we know the compiler works", or they would be "fired". Maybe on FPGA's but when you are going to litho this stuff it is too costly of a mistake and too simple of a check. On top of that I never specifically mentioned synthesized logic: most logic I work with is custom so formal verification is always expected. I understand that maybe you are a tool-kiddy (Quartus probably?) but some engineers do real work. \$\endgroup\$ – jbord39 Feb 6 '17 at 18:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.