4

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?

Shashank V M
  • 2,279
  • 13
  • 47
Niklas Rosencrantz
  • 1,694
  • 6
  • 33
  • 62

2 Answers2

6

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.

jbord39
  • 4,320
  • 1
  • 17
  • 25
  • 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? – Niklas Rosencrantz Jan 30 '17 at 16:58
  • 3
    @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) – jbord39 Jan 30 '17 at 17:05
  • 4
    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. – Dmitry Grigoryev Feb 03 '17 at 11:59
  • 2
    @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. – jbord39 Feb 04 '17 at 21:03
  • 1
    @DmitryGrigoryev: Not to mention that any decent compiler is going to be running verification under the covers the whole time anyway. It doesn't change my answer: the compiler is going to check itself against the RTL constantly. Maybe you don't run it as a seperate step at the end: regardless the explanation of what formal verification is remains. One industry example is Conformal by Synopsys. Heres a wiki article for your ignorance: https://en.wikipedia.org/wiki/Formal_equivalence_checking – jbord39 Feb 06 '17 at 18:08
  • jbord39, I don't know which TX company you are working for, but some other companies (in TX) do perform full-scale CPU verification. And even SoC. There are farms of computers and farms of custom-made FPGAs, and floors with hundreds of entry-level H1B designers who write and execute formal verification scripts. The scripts compare the output of RTL synthesis with DESIRED output per architectural SPECIFICATIONs, and flags IP blocks that do not perform, whether it is a RTL error or compiler bug. – Ale..chenski Feb 06 '17 at 18:16
  • @AliChen: Oh wow, you mean they are performing the full CPU verification flat (as in flattening out any hierarchical modules that had previously been verified). Do they go down to the gate level or transistor level... seems like an insane amount of memory required either way. – jbord39 Feb 06 '17 at 18:18
  • @jbord39, don't be ridiculous, obviously not at transistor level. I am not sure how flat the models are, I think they go only to the library level for particular manufacturing node, and custom IP macroblocks. But you are right, it is insanely massive and impractically slow, even with debug-accelerated timing. – Ale..chenski Feb 06 '17 at 18:43
  • 1
    It's misleading to say "Formal verification is state-point mapping done to ensure a schematic matches verilog or RTL model of the module" - that's equivalence checking, a *kind* of formal verification. Formal verification is also used for property checking of RTL Designs. – Shashank V M Aug 08 '21 at 12:26
  • 1
    I also agree that this answer is misleading. LEC and FV are not same. You talk about LEC. – Mitu Raj Aug 08 '21 at 19:11
-1

How to learn practical Formal Verification

I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the tutorials from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did as a senior year engineering undergraduate. The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles. Note that the open-source version of Symbiotic EDA does not support most SVA constructs.

Equivalence Checking Vs. Formal Verification

The other answer has mentioned formal equivalence checking, which is a kind of formal verification that checks 2 designs which may or may not be at the same abstraction level for logical / functional equivalency. For example, you can do RTL versus RTL formal equivalence checking or RTL versus gate-level netlist formal equivalence checking. Equivalence checking is one of the most common formal verification based techniques used in the semiconductor industry. Low-power formal verification and property checking are other kinds of formal verification. I have worked with property checking, so I can write a little about it.

Property Checking

Property checking is a technique where you specify properties, and the solver proves these properties are held true, either for all time i.e. induction, or for a certain number of cycles i.e. bounded model checking. 2 kinds of properties are specified: assumptions and assertions. Assumptions are properties which the solver assumes and assertions are the properties the solver needs to prove. So the problem of proving properties is represented as a SAT (Satisfiability, i.e. Boolean Satisfiability) problem, which is then solved by SAT solvers.

Limitations of Property Checking

  1. SAT is NP Complete i.e. no known polynomial time algorithm to solve this problem exists. So one might expect formal verification to be slow. Yes, formal verification can be slow for large designs and the tool can "choke" when the complexity of the proofs is high, due to the system running out of memory. The good news is there are clever techniques like blackboxes, cut-points and abstractions that can be applied by the one doing formal verification to speeden the verification process and reduce memory consumption. Adding a sufficient number of assumptions restricts the solver to check a smaller search space, and increases the probability of converging to a solution.
  2. The Incompleteness Theorem: The conclusion that has to be drawn from this theorem is that it is not possible to build a formal system that can be guaranteed to verify the correctness of any specifications. Tools that can solve most problems found in the real world do exist and are useful.
  3. Correctness and completeness of properties: The onus of the correctness and completeness of properties specified is on the one writing the properties. Writing correct properties is not very easy and it takes time to learn to write assertions.

Suggestions for property checking

  1. For a large design, it is recommended to break the problem of verifying the design into smaller, provable properties that verify the entire design. This enables the tool to use a Divide-and-Conquer approach to generate the proofs. For example, RISC-V Formal uses a set of simple properties to prove ISA compliance of RISC-V processors.
  2. It is also recommended to start with Bounded model checking and then try Induction proofs. This is because bounded model checking is easier to run and debug.

Is formal verification worth it?

  1. Formal verification is a somewhat challenging field, but the effort is worth it because some bugs like the Pentium Floating point division bug will most likely escape random testing, since the probability of the occurences leading to the detection of some bugs in random testing is extremely small.
  2. You can't verify that your design does not hang (enter a deadlock) at some point of time using constrained random, since there are only so many cycles you can run the simulation for. Formal verification can potentially prove the correctness of the logic design at the Register Transfer Level and gate level for infinite cycles.

In the end, it's not magic, and it has its limitations like any other technology. But it is a powerful technique that leverages cutting-edge research done in mathematics, computer science and formal logic.

Shashank V M
  • 2,279
  • 13
  • 47
  • 1
    "Formal verification...proves the entire design is bug-free" No, I don't think so. It shows that two representations of a design will behave in the same way, or are equivalent in some sense. The fact that this question has so little activity should tell you something about the importance of formal verification to real-world engineers, as opposed to academics. – Elliot Alderson Aug 08 '21 at 16:52
  • 1
    I am not a verification engineer, so my knowledge is limited in this realm. In 2019, when I attended DVcon, Intel claimed that they use ONLY formal verification to prove their designs, and it stirredd some debates as well. I am not sure how formal verification alone can prove a whole complex design especially on control paths. I guess this is still an unexplored area as many of the verification engineers are still on Testbench based verification which is quite time consuming like 10 times slower. – Mitu Raj Aug 08 '21 at 19:06
  • 3
    @ElliotAlderson is incorrect regarding the use of formal in industry, but I would caution that proving an entire design is bug free for infinite cycles is overstating formal's ability. Formal is _phenomenal_ for finding shallow bugs and regression testing. You can increase your search depth with assumes and tricks, but you are also limited by your computing resources. Deeper bugs are still found by directed tests, and the two approaches are complementary. Both, of course, rely on how good your assertions are as well. – awjlogan Aug 10 '21 at 11:56
  • An important point here is that the "design" of a complex VLSI design doesn't end at the gate-level or even transistor-level definition. The creation of the actual physical definition...the mask layouts...provides plenty of opportunities to introduce "bugs" that won't be detected by formal verification. – Elliot Alderson Aug 10 '21 at 12:00
  • 5
    It depends on your regulatory environment. Put some hardware in a Class III FDA device, and then tell me verification isn't a real world thing. – Scott Seidman Aug 10 '21 at 12:34
  • @ShashankVM - I think you've misunderstood what I was getting at, probably badly phrased on my part. Once you proven an assertion, it holds for all cycles, of course. What I meant, and apologies if I was unclear, is that you can't write a sequence of "infinite" length and expect to always prove the whole sequence. – awjlogan Aug 10 '21 at 13:04
  • 1
    @ShashankVM - yes, I know this. My point is you can't write an arbitrary length sequence and expect it to always be solved. An approach is to break a sequence into multiple assertions and prove each step, thus turning it into an assumption for the next assertion in the chain. – awjlogan Aug 10 '21 at 13:17
  • 1
    @ShashankVM - essentially, I'm trying to say you to that your answer implies that formal is the solution for _all_ verification problems. It, like any technique, has limitations/disadvantages and knowing what they are is just as important as knowing what the advantages are. – awjlogan Aug 10 '21 at 13:20
  • 1
    But you did not confine your **answer** to FPGAs. You generalized to "the semiconductor industry" and talked about "RISC-V processors" and "the Pentium Floating point division bug". A requirement for communication in engineering is that your writing must be unambiguous and precise. Never assume that the reader just "knows what you mean"; make it crystal clear with your words. – Elliot Alderson Aug 10 '21 at 16:51
  • 1
    @ShashankVM - it's not just slow, it can be _impossible_ given finite resources. – awjlogan Aug 12 '21 at 10:15
  • 1
    @ShashankVM - getting there. It's not just memory usage, the engine just might not be able to prove or CEX an assertion. And, as I said, it obviously depends on your _assertions_ being correct as well... :) – awjlogan Aug 14 '21 at 12:38