Kinds of Formal Verification

Formal verification is not one single technique. The same engines answer different kinds of questions, and the industry groups them into three families: property checking, equivalence checking and formal apps. This article explains what each family checks, what you have to write for it, and where it is used, so that you can tell which one a verification question needs.

7 min read | Beginner to Intermediate

What You'll Learn

• Describe property checking, equivalence checking and formal apps
• Explain how an equivalence check compares two designs with one formal question
• Name common formal apps and the questions they answer
• Choose the right kind of formal check for a verification question

Three Families

Property Checking

Property checking is what the first articles of this tutorial showed. You have one design and a list of properties, and the tool checks every property against every input sequence. It is also called model checking or assertion-based formal verification.

Typical questions are about the rules of a block:

• Can the FIFO overflow or underflow?
• Is the grant of the arbiter always one-hot?
• Does every request receive an acknowledge within 8 cycles?
• Can the state machine get stuck in a state it never leaves?

You write the properties, the assumptions about the inputs, and sometimes helper logic. The answer for each property is a pass, a proof, or a counterexample. Most of this tutorial is about property checking, because it is where formal thinking starts and where most of the work is.

Equivalence Checking

Equivalence checking compares two designs and asks whether they behave in exactly the same way. Typical pairs are:

• The RTL and the gate-level netlist that synthesis made from it.
• A netlist before and after a small fix, called an engineering change order, ECO.
• The RTL before and after a rewrite that should not change the function, such as a clean-up of the code.

The tool builds a combined circuit, called a miter. It feeds the same inputs into both designs, compares every output, and asks the formal question: is there any input for which an output of the two designs differs? If not, the designs are equivalent. If yes, the tool shows the input that makes them differ.

For designs whose registers correspond one to one, as RTL and its netlist usually do, the tool can compare the logic between registers only. This is combinational equivalence, and it works on very large designs. When the registers do not correspond, for example after retiming moved registers, the tool must compare behavior over time, which is sequential equivalence and is harder.

Equivalence checking needs no properties at all. The second design is the specification. That is why every chip project runs it after synthesis and after every change of the netlist.

Formal Apps

Some questions come up in every project and have a standard form. Tool vendors package them as apps: the tool generates the properties itself from a short description. Common ones are:

• Connectivity: is every signal of a large SoC connected to the right pin of the right block, through the multiplexers of the test and debug logic?
• X-propagation: can an unknown value, from an uninitialized register, reach an output that matters?
• Unreachable coverage: which coverage points of a simulation can never be hit, so that the team can stop trying?
• Register checks: does every register of a block behave as its specification file says (read-only, write-one-to-clear and so on)?
• Security: can a secret key ever reach a debug output?

Apps need little or no property writing, which makes formal available to engineers who are not formal specialists. They use the same engines underneath.

One Engine, Different Questions

All three families use the same kind of engine: a model checker with a solver. What differs is who writes the question. In property checking you write it. In equivalence checking the second design provides it. In apps the tool generates it from a template. Knowing this helps when an app or an equivalence check fails: the counterexample means the same thing in each case, an input sequence that makes the question come out false.

Running It in ChipVerify Lab

The formal panel of the lab does property checking with SymbiYosys. Equivalence checking of RTL against the netlist of the lab synthesis is shown later in this tutorial with Yosys commands. The apps are commercial products and are described, not run.

Common Mistakes