What is “formal verification” of hardware?

By xiean ·
Tags: Off Topic
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(http://www.kynix.com/Detail/1157032/ALU100-L.html). 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?
Thank you if any of you can help.

This conversation is currently closed to new comments.

Thread display: Collapse - | Expand +

All Answers

Share your knowledge

Related Discussions

Related Forums