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?