Assertions & Formal Verification

Prove designs correct instead of just testing them. Learn immediate and concurrent SystemVerilog assertions (SVA), sequences, implication and cover properties, assume/assert/cover in formal, bounded model checking and induction, equivalence checking, and a real Yosys proof — plus how a formal tool finds a counterexample for a buggy counter.

An assertion is an executable statement of intended behaviour: 'a request is always acknowledged within 4 cycles', 'the FIFO is never both full and empty'. In simulation, assertions fire the moment a rule is broken, pointing straight at the bug.

Formal verification goes further: a solver mathematically explores every possible input sequence to prove an assertion can never fail — or produces a precise counterexample waveform. It is ideal for control logic, arbiters, FIFOs, protocols and security properties.

An analogy

Simulation is testing a bridge with the trucks you have; formal verification is the structural engineer's proof that no truck under the limit can break it.

Assertions as executable specifications

Immediate assertions (assert (expr)) check a condition at one moment, like an if-statement that reports errors. Concurrent assertions (assert property) describe behaviour over clock cycles using sequences. Adding assertions to RTL catches bugs close to their source instead of many cycles later at an output.

SVA building blocks

The core operators:

How formal tools work

The design becomes a state machine in logic. Bounded model checking (BMC) asks a SAT solver whether any input sequence of length ≤ k from reset violates an assertion. Induction proves the property for unbounded time: if k consecutive good states always lead to a good state, and the first k states from reset are good, it holds forever. Assumptions restrict inputs to legal behaviour — over-constraining can hide bugs, so covers verify that scenarios remain reachable.

Equivalence checking and formal apps

Logic equivalence checking (LEC) proves that the synthesised or ECO-modified netlist matches the RTL — mandatory sign-off in every ASIC flow (Conformal, Formality). Formal 'apps' target specific problems: connectivity, X-propagation, register access, security (information flow), sequential equivalence and deadlock. Open tools include SymbiYosys, Yosys SAT and the EQY equivalence checker.

Formulas

Worked example: Writing a property

Given: Spec: 'grant must follow request within 2 cycles'

Find: SVA.

Answer: assert property (@(posedge clk) req |-> ##[1:2] gnt);

Worked example: State space

Given: A block with 64 flip-flops

Find: Reachable-state bound.

Answer: Far too many to simulate; formal reasons about them symbolically

Worked example: Counterexample reading

Given: mod-10 counter wrapping at 10

Find: Shortest failing trace.

Answer: ≈ 11 cycles from reset — exactly what Yosys reported

SVA properties for a valid/ready handshake (illustrative)

module handshake_checker (input logic clk, rst_n, valid, ready, input logic [31:0] data);
  default clocking @(posedge clk); endclocking
  default disable iff (!rst_n);

  // Once valid is raised it must stay high until the transfer happens
  a_hold_valid : assert property (valid && !ready |=> valid);

  // Data must not change while waiting for ready
  a_stable_data: assert property (valid && !ready |=> $stable(data));

  // Every request is accepted within 8 cycles (liveness bound)
  a_no_starve  : assert property (valid |-> ##[0:8] ready);

  // Make sure back-pressure is actually exercised
  c_backpressure: cover property (valid && !ready ##1 valid && !ready ##1 valid && ready);
endmodule

// Attach to the design without editing it:
// bind axi_slave handshake_checker u_chk (.*);

These are standard AXI-style rules. The bind statement attaches the checker to every instance of the design. Illustrative — requires a simulator or formal tool with full SVA support (the open-source Yosys front-end supports only a subset).

Formal proof of a modulo-10 counter with Yosys

// Modulo-10 counter with built-in formal properties.
module mod10_counter (
    input  wire       clk,
    input  wire       rst,
    input  wire       en,
    output reg  [3:0] count
);
    always @(posedge clk)
        if (rst)                  count <= 4'd0;
        else if (en)              count <= (count == 4'd9) ? 4'd0 : count + 4'd1;

`ifdef FORMAL
    // Invariant: the counter never leaves the range 0..9
    always @(*) assert (count <= 4'd9);
    // Assume a reset in the first cycle (initial state is unknown otherwise)
    reg init = 1'b1;
    always @(posedge clk) begin
        if (init) assume (rst);
        init <= 1'b0;
    end
`endif
endmodule

// yosys -p "read_verilog -formal formal.v; prep -top mod10_counter; async2sync;
//           sat -tempinduct -prove-asserts -set-assumes -seq 1 -set-at 1 rst 1 -maxsteps 20"
//
// Result:  Induction step proven: SUCCESS!
//
// Bug injected: wrap at 10 instead of 9  (count == 4'd10) ? 0 : count + 1
// Result:  SAT temporal induction proof finished - model found for base case: FAIL!
//          The counterexample trace shows count reaching 10 about 11 cycles after reset.

Real results from Yosys' SAT-based temporal induction. For the correct design the property is proven for all time (not just 20 cycles). For the buggy one, the solver returns the exact input sequence that breaks it — no test had to be written.

Common mistakes

Applications

Key takeaways

Going further