DESIGN VERIFICATION  ·  ARTICLE 05 OF 06

Formal verification isn’t scary — you’re just using it wrong

Most teams treat formal like a fire extinguisher — only when there’s a fire, and usually too late. Here’s how to bake it into your flow from day one.

 

Formal verification has a reputation problem.

Among DV engineers who haven’t used it, formal is the thing that requires a PhD, takes weeks to set up, and either proves your design is correct (unlikely) or times out after 24 hours (common). Among engineers who have used it badly — usually by throwing a formal tool at a large, unconstrained design and waiting for magic — the reputation is similar: powerful in theory, impractical in practice.

Both characterizations are wrong in the same way. They describe formal applied incorrectly, to the wrong problems, without the setup work that makes it useful. Formal verification, used well, is one of the few techniques in the DV toolkit that can give you a mathematical proof of correctness for a bounded set of properties. That’s not a feature of any simulation-based approach. No amount of constrained-random testing can give you that.

This article is about how to use formal well. It’s aimed at DV engineers who work primarily in simulation-based flows and want to add formal to their repertoire without a multi-month onboarding curve. We’ll cover what formal actually does, where it beats simulation decisively, how to write your first meaningful property, and how to integrate formal into a UVM-centric flow without reorganizing your entire methodology.

What formal actually does

At its core, formal verification answers a specific question: given a set of constraints on the inputs to a design, does a specified property hold for all possible input sequences, across all reachable states?

That’s it. No test vectors. No random seeds. No coverage closure. The tool exhaustively explores the state space — either proving the property holds everywhere, or finding a counterexample that violates it.

There are two primary formal engines you’ll encounter:

•        Model checking (bounded and unbounded): searches for counterexamples up to a specified depth (bounded) or across all reachable states (unbounded). Unbounded proofs are expensive; bounded proofs give you “no bug exists within N cycles” — which is still far stronger than simulation coverage.

•        Property checking with SAT/BDD solvers: the engine under most commercial formal tools (Cadence JasperGold, Synopsys VC Formal, Mentor Questa Formal). You write SystemVerilog Assertions (SVA), the tool converts them to a SAT problem, and either proves them or produces a waveform counterexample.

 

What formal cannot do: verify a design end-to-end at full complexity. A modern SoC has a state space that no formal tool can exhaust in any reasonable time. Formal is not a replacement for simulation. It is a complement — and a remarkably powerful one, applied to the right problems.

Formal doesn’t replace simulation. It proves the things simulation can only approximate — and it does so exhaustively, across every possible input sequence.

Where formal beats simulation, every time

The most useful thing to understand about formal is not how it works internally but where it has a decisive advantage over simulation. There are four categories where I reach for formal without hesitation:

Control logic and arbitration

Arbiter correctness — mutual exclusion, starvation-freedom, priority ordering — is extremely hard to verify by simulation. A constrained-random testbench can generate millions of arbitration scenarios and still miss the specific sequence of requests that causes a lower-priority agent to wait forever under a heavy-load condition. A formal tool, given a property that says “if agent A requests and holds its request, it must eventually receive a grant,” will either prove it across all possible request sequences or hand you the exact counterexample.

// Liveness property: a requesting agent must eventually be granted

// This is trivially hard to close with simulation alone

property arb_liveness;

  @(posedge clk) disable iff (!rst_n)

  req[0] |-> ##[1:MAX_WAIT] gnt[0];

endproperty

 

arb_liveness_chk: assert property (arb_liveness)

  else $error("Agent 0 starved: request not granted within %0d                               cycles", MAX_WAIT);

 

FIFO and buffer behavior

FIFOs are deceptively simple to get wrong. Off-by-one errors in depth calculations, incorrect full/empty flag timing, and pointer wrap-around bugs at power-of-two boundaries are all failure modes that simulation can miss for a long time — they only appear at specific fill levels that random stimulus may never reach in a short regression.

Formal, given properties about full/empty flag correctness and no-overflow/no-underflow guarantees, will explore every fill level exhaustively. The state space for a 16-entry FIFO is tractable. The proof is fast. And once proven, it’s proven — not just “we ran a lot of tests and didn’t see this fail.”

// No-overflow: write must not occur when FIFO is full

property fifo_no_overflow;

  @(posedge clk) disable iff (!rst_n)

  (fifo_full && wr_en) |-> $stable(wr_data);  // write is ignored when full

endproperty

 

// Flag correctness: full flag asserted iff count == DEPTH

property fifo_full_correct;

  @(posedge clk) disable iff (!rst_n)

  fifo_full == (count == DEPTH);

endproperty

 

// Empty flag correctness

property fifo_empty_correct;

  @(posedge clk) disable iff (!rst_n)

  fifo_empty == (count == 0);

endproperty

 

Reset and initialization sequences

Reset behavior is one of the most consistently under-verified areas of RTL design. Questions like “what state is the DUT in immediately after deasserting reset?”, “can reset be asserted mid-transaction without corrupting state?”, and “does a second reset after partial initialization produce the same result as a clean reset?” are all properties that formal handles cleanly and simulation handles poorly.

Simulation can run a reset sequence, but it can only run the reset sequences you think of generating. Formal can prove that reset produces a known-good state regardless of what was happening in the design when reset was asserted.

Protocol compliance checking

AXI, AHB, APB, CHI — bus protocols define legal signal orderings as sequences of events over time. These are naturally expressed as SVA sequences and properties. A formal tool can prove that the DUT never violates a protocol rule across all possible transaction sequences, not just the ones your testbench happened to generate.

This is especially valuable for interface logic that bridges two protocols. The bridging logic must simultaneously produce legal output on the downstream interface regardless of what it receives on the upstream one. Simulation can explore the combinations your testbench generates. Formal can prove the property holds for all of them.

Formal vs. simulation for protocol compliance

A common workflow: use formal to prove the DUT never violates protocol rules (the safety properties), and use simulation to verify that the DUT achieves its functional goals (correct data, correct ordering, correct response). The two techniques are complementary, not competing.

Writing your first meaningful property

The single biggest barrier to adopting formal is the blank page problem: where do I start? The answer is almost always the same: start with something you believe to be true about your design, that you would currently verify by simulation, and that simulation can’t prove exhaustively.

Here is a worked example for a simple write-enable register block. We’ll build up from a basic assertion to a formally meaningful property with constraints.

Step 1: Identify what you believe is true

The register block has a write-enable input. When write-enable is deasserted, no register should change value, regardless of what the data or address inputs do. This is a safety property: “registers are read-only when write-enable is low.”

// The claim: registers only change when write-enable is asserted

// We want to prove this for ALL possible addr and data inputs

property reg_stable_when_we_low;

  @(posedge clk) disable iff (!rst_n)

  !we |-> ##1 $stable(reg_file);  // all registers unchanged next cycle

endproperty

reg_stable_chk: assert property (reg_stable_when_we_low);

 

Step 2: Add assumptions to constrain the environment

A property without assumptions will be checked against all possible input sequences, including ones that could never occur in a real system. This leads to spurious counterexamples — the tool finds a violation that your protocol would never produce. You need assumptions to tell the tool what inputs are legal.

// Assumptions: what the environment is allowed to do

// These constrain the formal tool’s input space

 

// Address must be within the valid register range

assume property (@(posedge clk) addr < NUM_REGS);

 

// Write-enable must be a single-cycle pulse (per protocol)

// This prevents the tool from holding we high indefinitely

assume property (@(posedge clk)

  $rose(we) |-> ##1 !we);

 

// Now the assertion is checked only against legal input sequences

reg_stable_chk: assert property (reg_stable_when_we_low);

 

Step 3: Add a cover property to confirm reachability

One of the most common formal pitfalls: an assertion passes because the assumed constraints make it vacuously true. The property holds because the scenario it describes is unreachable. Cover properties let you check that the interesting scenario actually occurs under your assumptions.

// Cover: a write actually happens under these constraints

// If this never fires, your assumptions may be over-constraining

cov_write_occurs: cover property (

  @(posedge clk) disable iff (!rst_n)

  we && (addr < NUM_REGS)  // a write is legal and occurs

);

 

// Cover: consecutive writes to the same address

cov_back_to_back: cover property (

  @(posedge clk) disable iff (!rst_n)

  we ##1 we && ($past(addr) == addr)  // same address, two cycles

);

 

// If both cover properties are reachable, your assumptions are not

// over-constraining the interesting behavior.

 

Step 4: Understand the output

When you run the formal tool, you get one of three results for each property:

•        Proven: the property holds for all reachable states within the proof depth. For bounded proofs, this means “no counterexample exists within N cycles.” For unbounded proofs, it’s a full mathematical guarantee.

•        Counterexample (CEX): the tool found an input sequence that violates the property. It will give you a waveform. This is not a failure of formal — it’s exactly the output you want. Analyze the waveform, determine whether it’s a real bug or an assumption gap, and fix accordingly.

•        Inconclusive / timeout: the proof didn’t complete within the resource budget. This usually means the property is too complex for the current decomposition, or the design is too large without abstraction. It’s not a result you can act on — see the section on bounded proofs below.

 

A counterexample is the tool doing its job

First-time formal users sometimes treat a CEX as a sign that formal “failed.” It didn’t. It found a case you missed. Your job is to determine whether the CEX represents a real design bug, a gap in your assumptions, or an underspecified property. All three are useful discoveries.

Integrating formal into a UVM-centric flow

The most common objection to formal from simulation engineers: “my entire testbench is UVM. I’d have to build a separate formal environment from scratch.” This is partly true and mostly unnecessary.

The practical integration approach is to treat formal as a parallel lane, not a replacement lane. Your UVM simulation environment continues to exist. You add a lightweight formal environment alongside it, targeting the specific properties that formal is better suited to prove.

The formal app model

Modern commercial formal tools support “formal applications” — pre-packaged verification tasks with their own setup and methodology. The most useful for a first-time formal user:

•        Connectivity / X-propagation checks: prove that specific outputs can never go X under normal operating conditions. Zero setup beyond enabling the app against your RTL.

•        Reset checking: prove that reset drives all registers to their defined initial values, and that no register retains a value across an active reset. Usually a one-day setup.

•        Unreachability checks: prove that specific states or signal combinations defined as illegal in the spec can never be reached. Complements your illegal-bin functional coverage.

 

These apps are explicitly designed for engineers who are not formal specialists. They have constrained scope, fast setup, and interpretable results. Starting here — rather than with a blank SVA file — is the right entry point for most DV engineers.

Binding assertions to RTL without modifying it

A common concern: if I write SVA assertions, do I have to add them to the RTL? That would require RTL sign-off, coordination with designers, and introduces code that’s verification-only into production files.

The answer is no. SystemVerilog bind declarations let you attach an assertion module to any RTL hierarchy point without modifying the RTL itself. The assertions live in your verification environment, not in the design.

// Assertion module — lives in your tb/formal/ directory, not in RTL

module my_block_assertions (

  input logic clk,

  input logic rst_n,

  input logic we,

  input logic [ADDR_W-1:0] addr,

  input logic [DATA_W-1:0] reg_file [NUM_REGS]

);

 

  property reg_stable_when_we_low;

    @(posedge clk) disable iff (!rst_n)

    !we |-> ##1 $stable(reg_file);

  endproperty

  reg_stable_chk: assert property (reg_stable_when_we_low);

 

endmodule

 

// Bind statement — in your testbench or formal plan file

// Attaches the assertion module to the RTL instance

bind my_reg_block my_block_assertions u_assertions (

  .clk      (clk),

  .rst_n    (rst_n),

  .we       (we),

  .addr     (addr),

  .reg_file (reg_file)

);

 

// The RTL is untouched. Assertions are co-simulated in UVM

// and proven formally — same SVA, two flows.

 

Shared SVA between simulation and formal

The bind approach has a second benefit: the same assertion module runs in both your UVM simulation and your formal tool. In simulation, the assertions fire as runtime checkers and flag violations immediately. In formal, the same properties are proven exhaustively.

This means you write the SVA once. You get runtime checking in simulation for free, and you get formal proof coverage for the properties that matter most. The maintenance cost is one set of assertions, not two.

// Makefile / build script excerpt

# UVM simulation: assertions fire as runtime checkers

$ vcs -sverilog +define+BIND_ASSERTIONS \

      tb/formal/my_block_assertions.sv \

      rtl/my_reg_block.sv \

      tb/top.sv

 

# Formal: same assertions proven exhaustively

$ jg -formal \

     -define BIND_ASSERTIONS \

     tb/formal/my_block_assertions.sv \

     rtl/my_reg_block.sv \

     tb/formal/my_block_formal_plan.tcl

 

Handling the bounded proof problem

Unbounded proofs — proofs that hold for all reachable states, not just up to a cycle depth — are the gold standard. They are also computationally expensive and often infeasible for complex designs without significant abstraction effort.

Most practical formal verification for DV engineers working outside a dedicated formal team is bounded. A bounded proof says: no counterexample exists within N cycles. This is weaker than a full proof, but it’s still far stronger than simulation, and it’s achievable in a daily regression context.

The right way to use bounded proofs:

•        Set the bound based on the latency of the property you’re checking. An arbitration liveness property with a 4-cycle maximum grant latency needs a bound of at least 8–12 cycles (round-trip plus pipeline depth). A FIFO overflow property needs a bound that covers at least DEPTH+2 write cycles.

•        Treat an unreached bound as a scope decision, not a proof. If your tool runs for 6 hours and doesn’t find a counterexample at depth 50, you haven’t proven the property — you’ve determined that no bug manifests within 50 cycles. Document this scope explicitly.

•        Use k-induction when available. K-induction extends bounded model checking to produce unbounded proofs for many practical properties by proving both the base case (no CEX in k steps) and the inductive step (if no CEX in k steps, then no CEX ever). Most commercial tools support this.

 

A bounded proof that covers the relevant latency range is not a compromise. It’s a precise, documented claim: no bug of this class exists within this scope. That’s more than most simulation campaigns can say.

Common objections, honest answers

Every time I recommend formal to a team that hasn’t used it, I hear variations of the same objections. Here they are, with honest answers.

“We don’t have a formal specialist on the team”

You don’t need one to start. The formal app model — reset checking, X-propagation, connectivity — requires no SVA expertise. Writing basic assertions for control logic or FIFO behavior requires a day of learning SVA syntax, which is a tractable investment for any experienced DV engineer. The PhD-level formal work — full unbounded proofs of complex protocols, abstraction refinement, deep equivalence checking — does require specialization. The work described in this article does not.

“The tools are too expensive”

Commercial formal tools (JasperGold, VC Formal, Questa Formal) are licensed separately and can be expensive. However, most EDA vendor agreements at companies that already use their simulation tools include some formal entitlement. Check your license before assuming it’s unavailable. Additionally, open-source tools (SymbiYosys with the SMTBMC backend) handle a meaningful subset of SVA properties and are genuinely useful for FPGAs and smaller ASIC blocks.

“Formal always times out on our design”

This is the result of applying formal to the wrong scope. If you point a formal tool at a full SoC subsystem with dozens of interfaces and expect it to prove complex end-to-end properties, it will time out. Formal works on bounded, well-defined subproblems: a single arbiter, a FIFO, a CSR block, a reset network. Scope the problem to match the tool’s capabilities, not the other way around.

“Simulation gives us enough confidence”

For many properties, this is true. For control logic, arbitration, and reset behavior — properties where the failure space is large and the failure conditions are hard to generate randomly — it is not. The question is not whether simulation is good enough on average; it’s whether simulation is good enough for the specific class of bugs that formal excels at catching. Those bugs have shipped in production silicon from teams with mature simulation-based verification flows. Formal catches them cheaply, early, and exhaustively.

Where to start this week

If you have never run a formal tool and want to start with something concrete, here is a one-week path:

•        Day 1: identify a FIFO, arbiter, or CSR block in your current design that has well-defined properties. Write down three things you believe are true about it — in English first, then in SVA syntax.

•        Day 2: write the SVA properties and assumptions. Use the bind approach so the RTL is untouched. Simulate with your UVM testbench and confirm the assertions don’t fire on legal stimulus.

•        Day 3: run the properties through your formal tool. If you hit a counterexample, determine whether it’s a real bug, an assumption gap, or a property specification error. All three are useful.

•        Day 4: add cover properties to confirm that the scenarios you care about are reachable under your assumptions. Adjust assumptions if needed.

•        Day 5: document the scope and result. “No counterexample for these three properties within 20 cycles.” Add this to your sign-off evidence.

 

That’s a week of work, not a six-month project. The output is a set of properties that run in your regression, catch a class of bugs that simulation handles poorly, and produce documented proof evidence for your sign-off package.

Formal isn’t scary. It’s a power tool with a specific set of applications where it’s decisively better than anything else in the DV toolkit. Learn those applications. Apply the tool to them. The state space it exhausts in an afternoon would take your simulation regression years to approximate.

 

Next in this series:

Article 06 — What AI tools actually change about verification — and what they don’t