Our forums are currently in maintenance mode and the ability to post is disabled. We will be back up and running as soon as possible. Thanks for your patience!



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