Skip navigation

What is formal verification? Today, even if you ask experts, you will not get a clear answer.

Here are a few definitions you will find:

  • “formal verification of is the act of proving or disproving the correctness … using formal methodsmathematics.” <wikipedia>
    • “formal methods are particular kind of mathematically-based techniques for verification …” <wikipedia>
  • “Use of various types of logic and mathematical methods to verify the correctness of IC logic…” <edacafe>
  • “Establishing properties of hardware or software designs using logic, rather than (just) testing…” <nist>

None of these definitions is correct, or even meaningful, for that matter. What they are trying to get at is that formal verification is not simulation. There is somehow mathematics involved, but it is not clear how or why this is significant.

The sad part about this is that these definitions largely come from experts in the formal verification world. The fact is researchers don’t really know how to define formal verification in a way that clearly differentiates it from simulation. Considering that most researchers in the area have a theoretical background and tend to look down their noses at simulation as a verification method, this identity crisis is a real problem for them.

The real goal of formal verification is to prove things correct rather than merely to test them. To understand the origin of the crisis, we first have to understand what it means to prove something. There are two fundamental properties of any proof method: soundness and completeness. A proof system is sound if what it proves is also true. For example, we would not want a proof system that proves 2 +2 = 5. A proof system is complete if everything that is true is proven. Suppose we have a correctly working adder. A complete proof would have had to verify correctness for all possible input values since all possible input values result in the correct answer.

Soundness underlies any verification method. Simulation and formal verification are both sound. When university research labs produced with the first practical formal verification method, BDD-based model checking, the early 1990s , it was easy to differentiate formal verification from simulation. Formal verification was complete and simulation was incomplete. But, very quickly it became apparent that these first industry-ready formal verification tools were still far too capacity limited to be useful on real designs.

Semi-formal verification was proposed as the way forward. What is semi-formal verification? It’s formal verification, except its not complete. The idea was to give up on proving things and just focus on finding more bugs. But, simulation is also incomplete. So, what’s the difference between the two? And, can we come up with a better definition of formal verification (including semi-formal verification) that clearly distinguishes it from simulation in a useful way?

The answer comes, somewhat obviously, from the definition of the word formal. Surprisingly, though, the word formal does not refer to the use of mathematics. Here is a definition from Webster’s:

formal: … b) relating to or involving the outward form, structure, relationships, or arrangement of elements rather than content…

In the context of verification, the word formal refers to looking at the structure of the design rather than its behavior. For example, suppose our adder is composed of gates. A formal verification -based proof system would represent the structure of these gates (type and connections) as symbols and create equations describing the relationships between them. The adder would then be represented by one (very large) equation. Then to prove the adder is correct, you could create the equation:

enormous_equation_representing_structure_of_adder = A+B

Then it is a “simple” matter of doing algebraic manipulation to show that both sides of the equation are the same, similar to how one would prove the algebraic identity, “2A – A = A”. Once you were done, you would have a complete proof because the symbols A and B represent all possible values of inputs.

OK, that is more an explanation of how formal verification works than its essence and it doesn’t explain what incomplete formal verification is. The key point here is the use of symbols to represent structure and symbolic manipulation to prove results. If a proof system is using symbols and manipulating them directly, it is formal in some sense. Incomplete formal verification just means that we did not prove it for all possible values of the symbols. For example, suppose for the equation “2A – A = A”, we could only prove it for A>0. This is incomplete because we did not verify the equation for all values. This is still better than simulation because we did prove it for many more values than if we simply tested a large number of values. This is the rationale for semi-formal verification; that it can cover more cases than simulation, but can be incomplete.

But, just saying semi-formal can potentially cover more cases than simulation is still not a clear differentiation from simulation. There has to be something more. The answer lies in the use of symbols and symbolic manipulation. Even if incomplete, a system that uses symbols has an idea of what has been not been proven in addition to what has been proven. This means that an incomplete proof system can give the user information about what was not proven. Simulation-based proof systems only give information on what was proven.

Therefore, a useful definition of these different proof methods is:

  • simulation: sound, incomplete, not aware of what is not proven.
  • semi-formal verification: sound, incomplete, aware of what is not proven.
  • formal verification: sound, complete.
Advertisements

13 Comments

  1. Hi Chris,

    Interesting post. And, at least in my view, indicative of a very serious
    problem.

    This is an issue that I have had to deal with a lot as a phd student,
    attempting to explain my research to different people with widely varying
    backgrounds, and over time I’ve formed a somewhat different characterization.
    Instead of trying to characterize the “totality” of correctness, I prefer to
    distinguish different methods by the *object* resulting from the verification
    activity. In this scheme, “formal” is distinguished from “simulation” by the
    yielding “satisfied formulas” instead of “execution traces”. This highlights
    that in order for someone to understand what has been determined about a design
    through a formal verification effort, they need to understand the set of
    formulas in question.

    In some sense this collapses “formal” and “semi-formal” into a single class. I
    actually think that this is sensible since it’s not clear that one can, in
    general, even specify “total correctness”. However, if you think that concepts
    like “total correctness” and “partial correctness” make sense, then you can
    simply say “formally establish partial correctness” for “semi-formal”.

    I suppose that the problem is also much more extensive than just the “formal”
    vs. “simulation”. Eg “model checking” and “theorem proving” are also usually
    interpreted much too narrowly by people. And the list goes on…

    • Michael,

      I think your concept of “satisfied formulas” is interesting. It is certainly something I hadn’t thought of. But, I think it may be too constraining. I am not sure all formal verification techniques can be considered to produce a proof, which is what I think you are talking about. For example, if I used BDDs to formally verify an adder, the result would be a BDD with just the single node “true”. I don’t think this would meet your definition of a satisfied formula, but most people would consider the adder to have been formally verified.

      –chris

        • Michael Katelman
        • Posted June 9, 2009 at 4:00 pm
        • Permalink

        Chris,

        I had meant to respond sooner and forgot. Yay for auto-notification on new
        postings!

        I agree with you that something like a 1-terminal BDD is difficult to construe
        as a proof in any technical sense. I suppose that the point I want to make is
        that, to distinguish terms like “simulation” and “formal”, it my be useful
        to consider the problem in terms of communicating to a verif. engineer (a) what
        work he is going to have to perform and (b) what result he will end up with.

        I was using the term “satisfied formula” as a weaselly way of avoiding a
        technical discussion on what a “proof” actually is. The point is that there
        is a notion of “formula” in formal verification that the user needs to
        understand, and what entailment relation I am establishing it under is probably
        too academic for most verif. engineers. Does it really matter if I determine
        (an LTL) $\varphi$ with respect to a Kripke structure representation of the RTL
        and the associated entailment relation $\models$, or if I do some weightier
        encoding into HOL and establish it with respect to an entailment relation
        $\proves$ with a proper proof system? To my mind the answer is clearly no.

        Of course, it is another matter entirely when we start talking about the
        academic community. I personally feel that we are way too sloppy with
        terminology. Eg. I read many papers on SMT solvers where the “theory” in
        question isn’t defined precisely. What is the “theory of bit-vectors”, for
        example? It’s kind of obvious, I guess, but no one defines these things
        precisely, and I wish they would and do their new work w.r.t. said definitions,
        as mathematicians do.

        Without going into too long a technical discussion, I can tell you essentially
        how I try to distinguish simulation precisely in my papers. I use a logic (a
        bona fide logic, called rewriting logic) where the only logical connective is
        $\rightarrow$, and judgments are of the form $\Gamma \proves t \rightarrow t’$,
        where $t,t’$ are terms that represent configurations of RTL code and a current
        state (a la operational semantics). The axioms in $\Gamma$ define
        $\rightarrow$ according to the semantics of the RTL language. Now, simulation
        is defined simply as any proof/judgment of the above form where $t$ is a \emph{ground term}, ie. it has no variables.

  2. Hi Chris,

    A) You are posing a very important question. I believe that before answering this question one should address another issue that is also very intriguing: why simulation works at all? Indeed, in many cases, one gets quite decent results by probing a miniscule part of the search space. When studying this issue (see [1]) I made the following conjecture. The effectiveness of simulation can be explained if one considers a set of test vectors as an encoding of a formal proof rather than a sample of the search space. In[1] I show that to encode a resolution proof that a CNF formula is unsatisfiable one needs at most twice as many test vectors as the number of resolutions. (So, informally a resolution proof and a set of test vectors encoding this proof have almost the same size.) The main idea here is to restrict resolution operations by a set of complete assignments (points of the search space). Given a CNF formula F, a set of points is considered as an encoding of a proof if even the restricted set of resolutions is enough to prove unsatisfiability of F.

    Since verification of a combinational circuit can be cast as SAT (checking if a CNF formula is satisfiable), this result covers the case of combinational circuits. However, the idea to treat tests as a proof encoding obviously goes beyond the case of combinational circuits.

    B) The results above imply that the answer to the question “What is the difference between formal verification and simulation” is “None”. (Of course, I am fully aware of the fact that currently there is a gap between them both in practice and theory.) To make this answer more believable let us consider the problem from a different angle. You mentioned that a proof system has to be sound and complete. But there is one more important property that complexity theory people call automatizability. Informally, a proof system is automatizable if it has an efficient algorithm for finding good proofs. (A rule of thumb here is that the more powerful a proof system is the less automatizable it is.) If one adds the automatizability requirement to soundness and completeness, simulation and formal verification naturally merge into a single entity (see below).

    The idea of [1] can be viewed as changing the resolution proof system to make it more automatizable. Namely the following two changes are made. First, we add a “simulation operation”. This operation is just to generate a complete assignment p and check the value of the CNF formula F (to be tested for satisfiability) at point p. If F(p) = 1 we stop and declare F satisfiable. Otherwise, we add the fact that F(p) = 0 to the set of “axioms”. Second, we restrict the resolutions based on the axioms F(p) = 0 accumulated so far. Since we restrict the set of resolutions one can make , finding a proof becomes much easier (i.e. the proof system becomes more automatizable.)

    1. E.Goldberg On bridging simulation and formal verification, VMCAI-2008, San Francisco, USA, LNCS 4905, pp.127-141. (It can be downloaded from http://eigold.tripod.com/papers.html).

    • Hi Eugene,

      You have made some interesting points. I want to reply, but it will probably take a while for me to digest this
      and respond. I will say that the title of my blog “bugs are easy” is answering the question: “why does
      simulation work?” I don’t know if you have read my posts on this, but my arguments are mostly emprical.
      I would really love to see some theoretical explanation for this, so I look forward to reading your paper.

      I have one question, just based on reading your comment and thinking for two seconds. You say that the number
      of test vectors is at most twice the size of a resolution proof. But, to prove a circuit with N inputs is unsatisfiable
      requires 2^N test vectors. Thus, I can interpret this as meaning that all resolution proofs will be exponential
      in length, or more generally, formal verification, in the worst case, can verify no faster than simulation. But, this
      is well known. So, it is not clear what this means in terms of differentiating formal verification from simulation.

      regards,

      –chris

  3. Hi Chris,
    1) I mean that a test set encodes a resolution proof, not the other way around. The fact that one can verify a property of a circuit of n inputs with 2^n test vectors has no bearing on the size of the smallest resolution proof of this property. One can routinely check a property of a circuit with,say, 300 inputs by a state-of-the-art SAT-solver that makes, say, 100,000 backtracks. This typically translates to a resolution proof of, say, 10 million resolutions. To encode this proof, one needs at most 20 million tests as opposed to a complete test set of 2^300 test vectors. (I just finished another paper on this topic. It should make easier reading. Besides it has new stuff.)

    2) I agree that, in practice, the majority of bugs are easy. But I am uncomfortable with the claim that “bugs are easy, no matter what …”. My claim is that simulation works well because there are short formal proofs of correctness, which we may be unaware of. (It may seem strange, because if our design is buggy it can not have any proofs of correctness. Informally, what I mean here is that “the core design” or “a detailed specification” is correct and have simple proofs of correctness. However our current implementation may have bugs.) On the other hand, if our “detailed specification” is messy and does not have short proofs of correctness, the debugging of its implementation will be a nightmare.

    Ciao,
    Eugene

    • Eugene, Michael,

      I think you both are trying to make similar points, which I can oversimplify as: the difference between simulation and formal verification is that formal verification produces a proof of unsatisfiability while simulation does not. Eugene, your further are saying that the proof can be in the form of a set of test vectors,
      which could be exponentially small (again, probably oversimplifying).

      I think this is an interesting concept, but I am not sure it is sufficient to distinguish formal verification from simulation. I think we can agree that simulation can produce a “proof” of size 2^N for an N input circuit. I think we can also agree that formal verification can produce a proof of size less than 2^N, although in the worst case it may be no smaller than a simulation proof.

      I think where we probably disagree is in whether the definition of simulation includes proofs of less than size 2^N. Based on my definition of simulation, the answer would be no. The fact that the output of a verification process is a set of test vectors does not mean that those test vectors were produced by simulation. To produce a proof of size less than 2^N requires some sort of formal analysis. The verification process, then, is: 1) do formal verification to produce proof, 2) convert proof to test vectors, 3) run test vectors on design. To me, this is very clearly formal verification, not simulation.

      –chris

  4. Chris,
    1) I made an inaccurate statement in the previous post. The relation between proofs and tests works in both directions. Given a proof, one can generate its encoding (as a set of points) and vice versa, given a set of points, one can produce a proof encoded by these points.

    2) One should differentiate the generic idea of TTPE (Treating Tests as a Proof Encoding) and its practical applications. Building a formal proof and then finding tests than encode it is only one way to use TTPE. Another method of using TTPE is to build a proof and tests simultaneously as follows. You apply a test vector t to the circuit N to be verified. If N produces the wrong output value for t, then a bug is declared. Otherwise, a new fragment of a proof is added. (For the resolution proof system this fragment is a resolution operation “specified” by t).

    3) You made the correct observation that (classical) simulation deals with unstructured circuit while formal verification makes full use of circuit structure. Here is some elaboration on this idea. The difference between simulation and formal verification can be formulated in terms of the “quality” of proof encodings. Test vectors corresponding to simulation encode a trivial exponential proof (that enumerates input assignments). Test vectors corresponding to formal verification encode a structured proof (i.e. a proof taking into account the circuit structure). The trivial proof is long but universal. A formal proof is short but has to be generated for every design property separately).

    There is a catch here though. As I said before, although originally simulation was related to the trivial proof (enumeration of all input assignments), the reason why it worked (in my opinion) was that test vectors encoded more sophisticated proofs.

    4) I disagree with the conclusion that semi-formal verification “knows what needs to be proven” to finish the proof. Let us consider SAT-solvers. A classical DPLL-like SAT-solver builds a binary tree. In such a case, indeed, the part of the tree that has not been examined yet is easy to describe. However, modern SAT-solvers use clause learning , each clause specifying a part of the search space that has been examined. The problem is that the parts specified by different clauses overlap. So if a clause learning SAT-solver stops before deriving an empty clause (which means that the formula is unsatisfiable), the area of the search space that has not been visited yet is specified only implicitly (as the negation of the conjunction of learned clauses).

    Best regards,
    Eugene

  5. Chris, Eugene,

    I really think that one needs to separate this discussion according to two
    audiences: (1) definitions for day-to-day engineers, and (2) definitions used
    by experts/academics. It may be unreasonable to expect precise, unambiguous
    definitions in the case of (1) if a 95\% accurate definition can be conveyed in
    1/10 the time of a 100\% accurate definition. So, it may be enough to simply
    acknowledge this fact instead of holding out for enlightenment!

    As I wrote in my post yesterday, I think the important aspect to conveying
    understading of such concepts to engineers is to convey the work required to
    perform the verification task, and the result born out of this task. A simple
    idea is to start with some sort of typed function for each task, such as,
    perhaps

    task1 :: RTL -> [InputVector] -> ExecutionTrace
    task2 :: RTL -> Formula -> Maybe ExecutionTrace
    task3 :: RTL -> Formula -> [Commands] -> Maybe Proof

    The types for these tasks convey a lot of unambiguous information. First they
    emphasize that the work required to apply task1 (roughly simulation) and task2
    (roughly bdd-based model checking) is different; for task1 I need to create
    something of type InputVector, and for task2 I need to create an object of type
    Formula. I also know that if I try task2, some of the work is already done for
    task3 (roughly theorem proving). Granted, these type expressions do not tell
    you how to interperet the result of the associated functions; trying to
    generalize that may be a fool’s errand anyhow. In any case, my hypothesis is
    that, on the specific question of boxing “formal” vs “simulation” for
    engineers, things in the formal box would have an input called Formula.

    For case (2), the situation is clearly different. Eugene’s idea of defining
    simulation via a proof-complexity metric is definitely an interesting mental
    exercise, but I’m not sure about it’s usefulness. The first thing that pops to
    mind is some sort of relative Kolmogorov-complexity measure, which seems
    convoluted. I still think my distinction between ground and non-ground terms is
    quite simple and pretty reasonable. Although I realize that I haven’t given a
    lot of information to accurately analzye what I mean by that.

    These are just my slightly-random thoughts, but I’m finding this discussion
    very interesting.

  6. Chris,Michael,

    1) The list of applications of TTPE (Treating Tests as a Proof Encoding) is very long. One of the most important applications is building good metrics. (Currently finding a metric is black magic.) TTPE implies that a formal proof is an “ideal metric”. It contains a complete set of events one needs to test to guarantee that the property in question holds. So, examining formal proofs of design properties and their encodings in terms of tests one actually studies high quality metrics.

    2) In a sense, TTPE justifies formal verification once and for all. Before, a verification engineer could say that all formal verification tools are toys that can handle only small design bits. Now, a formal verification person can retort that a formal proof is an ideal metric. Without studying the structure of proofs (and tests encoding those proofs) one can not make progress in the metrics business. Note that this argument works even if formal verification never becomes scalable.
    Eugene

    • a few more thoughts,

      1) I am not clear on what benefit the user derives from having a proof of unsatisfiability. There is certainly benefit to knowing that a property is unsatisfiable (no bugs), but I don’t see how the user would use the proof. I think users would want to use the test vectors for regression testing. But, if the design changes, then the proof would change also. Running the old set of vectors on the new design does not mean that all bugs in the new design will be caught. Even on moderate sized designs, the proof could be thousands of vectors. I don’t think anybody is going to spend a lot of time studying that many vectors, especially if the proof changes every time the design changes. Also, I don’t understand your claim that TTPE is useful even if formal verification doesn’t scale. I think the only way to produce a (minimal sized) proof is to use formal verification. I don’t think it is possible to produce minimal sized proofs on large designs since formal verification won’t work on large designs.

      2) With respect to the definition of semi-formal verification, I agree that there are different levels of information, but even an implicit representation of what has not been proven is still more than simulation produces. The dividing line for me is zero knowledge vs. more than zero knowledge. An implicit representation is clearly some knowledge and so I think this is a pretty crisp definition.

      3) I realized that my argument about what constitutes a complete proof in simulation is not quite right. It is not 2^N for an N-input circuit, but is, in fact, infinite. The issue is that for the proof to be 2^N, we have to make the assumption that the circuit is combinational when it may not be, even if the specification says so. Since, for simulation, I assume zero knowledge, we cannot make that assumption. For example, suppose we are verifying a 2-input AND gate. If we knew it was combinational, the proof would only be four vectors. But, it could have been designed incorrectly such that there is some state in the design and bugs don’t manifest until after more than four vectors have been applied. (This actually happens when designing at the transistor level). For any finite-sized proof, we could insert a time bomb that only triggers once the proof has been exhausted. Therefore, the only way to be sure there is no sequential behavior is to verify an infinite number of vectors.

      4) Having said that, pragmatically, detecting whether a circuit has state or not is relatively easy (can be done in polynomial time, I think). Therefore, it is not unreasonable to claim that finite proofs can be generated using simulation provided we allow some amount of formal analysis as long as it is computationally tractable (say, no more than polynomial complexity).

      5) The natural follow-on question from that is: are there polynomial formal analyses that can be done to reduce the proof size to less than 2^N? This would be extremely useful, especially if it were exponentially reduced in polynomial time. I am thinking of how NP-hard problems such as traveling salesman can be solved within a finite bound of being optimal in polynomial time. Is it possible to produce a proof that is only polynomially larger than the minimum sized proof in polynomial time?

      cheers,

      –chris

  7. Hi Chris,

    1) To explain how one can use proofs, I need to formulate two generic problems of testing/simulation (in terms of SAT). Problem number 1 (property checking): given a CNF formula F, generate a set of points P such that F(P)=0 implies that F evaluates to 0 for all points. In this problem, one uses simulation to check if a particular design property holds. Problem number 2 (property preservation): given an unsatisfiable formula F, find a set of points P that detects satisfiable variations F* of F. This problem describes the situation when the property in question holds for the current design and one needs to check if it still holds after a design change (the new design being specified by a CNF formula F*). This change may describe a manufacturing fault or design modification depending on whether the design is implemented in hardware or as a software model.

    2) For solving problem 1 (property checking) one can use a proof that F is unsatisfiable under some symplifying assumptions. (I omit explanations here.)

    3) Here is how a proof can be used for solving problem number 2 (property preservation). Given a CNF formula F and a proof R, one just builds a proof encoding P={p1,…,pk} of R and uses the input parts of pi as tests. (Here pi is a complete assignment to the variables of F where F specifies a circuit N. So pi can be represented as (ti,yi) where ti is the assignment to the input variables of N and yi is a simulation trace i.e. assignment to internal variables of N.) The main idea here is follows. One can view R as a proof of a complex proposition F (describing the circuit N plus a property). Suppose that N changes into N* due to a technological fault or design correction and this change is described by CNF formula F* (specifying N* plus the same property). Suppose that the property is broken (i.e. F* is satisfiable). Then the proof R is obviously wrong for F*. Since P encodes R there is high probability that there is a point pi of P such that F(pi) != F*(pi). In this case, the input part ti of pi is a test detecting the bug/fault.

    4) Here is a more concrete example. Let N be the circuit to be tested. If one generates a “natural” resolution proof R that two copies of N are identical, then a proof encoding P={p1,..,pk} of R contains tests detecting all stuck-at faults (each test ti being the input part of pi of P as described above). Interestingly, a proof encoding of R actually contains a stronger test set (because even a certain subset of P contains tests detecting all stuck-at faults). So not only, TTPE explains why the stuck-at fault model works well in ATPG, but it also shows a way to build stronger test sets.

    5) When I say that simulation can benefit from TTPE (even if formal verification turns out to be unscalable) I mean the following. In many cases, one can derive some properties of good test sets without any knowledge of a proof. For example, in the new paper I mentioned before, I show that so called boundary points are good for encoding ANY resolution proof. (A boundary point is a complete assignment p such that all clauses falsified by p share the same variable).

    Another approach is to find a proof for a reduced version of the design at hand. Then analyzing this proof one may come up with a better metric to be used for the entire design (e.g. when analyzing the proof one may identify some non-obvious events that have to be tested).

    Eugene

  8. Hi Chris,
    1) I continue commenting your last post. As far as I understand, your example with a combinational circuit that turns into a sequential one is aimed at finding a limitation of TTPE. In reality, a formal proof and simulation work in the same search space. So having a finite proof and infinite set of tests may mean only one thing: formal verification and simulation work in different search spaces. Once this problem is fixed either both a formal proof and test set become infinite or finite.

    2) However, if you are looking for a catch in TTPE, here it is. TTPE has the same problem as formal verification. Namely, to find a formal proof one needs to have a clearly defined search space. (A formal proof is not just a set of operations over some meaningless symbols. Every symbol has to have a definition relating this symbol to the search space). On the contrary, in simulation, one just needs to know how to perform a simulation run. For example, it is quite possible that for some test vectors, simulation is not even possible yet (because some parts of the design are not finished yet). Then one can run simulation over allowable input assignments.

    BTW, this is one more answer to your question about separation of formal verification and simulation. One can run simulation even when formal verification is not applicable because the search space is still “under construction”.
    3) In theory the answer to the question “Is it possible to produce a proof that is only polynomially larger than the minimum sized proof in polynomial time?” is no. As I mentioned before this is due to the fact that all non-trivial proof systems known so far are most likely non-automatizable. However these results have little bearing on practical applications because they assume that no extra information is given about a particular formula. In reality, every design has tons of extremely useful information that people just do not know how to use. One of the examples of extremely useful information is design high-level structure. When used properly the knowledge of this structure may dramatically reduce the complexity of finding a good proof (the shortest proofs are ones formulated in high-level terms).

    Best regards,
    Eugene


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: