Skip navigation

My advisor at Stanford, David Dill, coined the term, “semi-formal verification”. In his talks to justify switching from pure formal verification to semi-formal verification, he would show the following graph.

bug rate vs. time for a typical project

bug rate vs. time for a typical project

Dave would say that it was the period at the end of the verification process in which the bug rate was low that characterized the verification bottleneck. He called this period “purgatory” and proposed that, rather than trying to prove designs correct, formal verification researchers should focus on trying to eliminate the purgatory period by concentrating on those few remaining hard-to-find bugs. Semi-formal verification went on to become the standard methodology used by practically all industrial tools.

But what struck me most about this was not the proposed solution, but the shape of this curve itself. There was the unstated assumption that the bug rate would be high at the beginning and low at the end, which caused the shape of this curve. In all projects I had worked on, the bug rate curve was the same shape as this. There is often some ramp up time at the beginning as verification engineers come up to speed on the design. But, there is always a period of high productivity in finding bugs followed by a purgatory period in which it is extremely time consuming to find each new bug. I have seen this so often, I have come to call it the first law of verification.

first law of verification: the bug rate will be high at the beginning and low at the end.

To most people, this law is so ingrained that they don’t even realize it’s most basic implication: bug rate is the single most important factor in determining whether a design is ready to tapeout/ship. To illustrate, let’s assume you have met all your tapeout criteria:

  • coding complete.
  • testplan written and reviewed.
  • all tests written and passing.
  • coverage is 100%.
  • code reviews complete and lint checks clean.
  • physical design checks complete.

But, the bug rate curve looks like this:

A bad bug rate curve

A bad bug rate curve

Do you tapeout?

No, you assume that something is wrong. The design is changing or the testing has some problems, but either way, more work needs to be done. Why do you believe this? Because of the first law of verification.


3 Trackbacks/Pingbacks

  1. […] Bugs Are Easy essays on designing complex systems About « Entymology 101: The First Law of Verification […]

  2. […] The First Law of Verification, The Second Law, The Third […]

  3. […] the framework of the the three laws of verification, it is possible to synthesize a consistent explanation for all the conflicting […]

Leave a Reply

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

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

Google+ photo

You are commenting using your Google+ 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 )


Connecting to %s

%d bloggers like this: