Formal Verification with SymbiYosys and Yices2: Proving Your RTL Correct

March 15, 2026

hardware rtl computer-architecture verification formal verification SymbiYosys yices2 SVA SystemVerilog assertions deadlock handshake reset verification bounded model checking ASIC design RTL verification sby

Simulation tells you what happened in the cases you thought of. Formal verification tells you what happens in every case that can ever occur.

That difference matters. A handshake protocol looks correct in simulation when your testbench never hits the corner case where both sides stall simultaneously. Formal will find it on the first run.

This post walks through a complete formal verification flow using SymbiYosys and Yices2. You will write a real design with real bugs, write SVAs to catch them, run the tools, read the counterexamples, and fix the issues one by one.

What SymbiYosys Actually Is

SymbiYosys is a front end for formal hardware verification. It takes your RTL, your property files, and a solver backend, and either proves your assertions hold for all reachable states or gives you a concrete trace showing a violation.

It is not a simulator. It does not run test vectors. It uses formal methods, specifically bounded model checking and k-induction, to reason about all possible behaviors of your design up to some bound depth.

Yices2 is one of the SMT solvers that SymbiYosys can use as a backend. It is fast, mature, and works well for most RTL problems. Other backends include Boolector, Z3, and ABC.

The flow looks like this:

RTL (Verilog/SV)
     +
Property file (.sby)
     |
     v
SymbiYosys
     |
     v
Yosys (synthesis to internal IR)
     |
     v
Yices2 (SMT solving)
     |
     v
PASS or FAIL + counterexample trace

Installing the Tools

On Ubuntu or Debian

sudo apt-get update
sudo apt-get install -y symbiyosys yices2

If those packages are not in your distribution’s repository, install from source.

Installing SymbiYosys from Source

# Install Yosys first
sudo apt-get install -y build-essential clang bison flex \
    libreadline-dev gawk tcl-dev libffi-dev git graphviz \
    xdot pkg-config python3 libboost-system-dev \
    libboost-python-dev libboost-filesystem-dev zlib1g-dev

git clone https://github.com/YosysHQ/yosys.git
cd yosys
make -j$(nproc)
sudo make install
cd ..

# Now install SymbiYosys
git clone https://github.com/YosysHQ/sby.git
cd sby
sudo make install
cd ..

Installing Yices2 from Source

git clone https://github.com/SRI-CSL/yices2.git
cd yices2
autoconf
./configure
make -j$(nproc)
sudo make install
cd ..

Verify the Installation

yosys --version
sby --version
yices-smt2 --version

All three should print version strings without errors.

The Design Under Verification

The design is a ready/valid handshake controller. It manages a two-sided handshake: a producer side and a consumer side. The controller asserts that data only transfers when both sides are ready, and it should never deadlock.

Here is the design with intentional bugs included. We will find and fix them using formal.

// handshake_ctrl.v
module handshake_ctrl (
    input  wire        clk,
    input  wire        rst_n,

    // Producer side
    input  wire        prod_valid,
    output reg         prod_ready,

    // Consumer side
    output reg         cons_valid,
    input  wire        cons_ready,

    // Internal data path
    output reg         transfer_done
);

    // State encoding
    localparam IDLE     = 2'b00;
    localparam WAITING  = 2'b01;
    localparam ACTIVE   = 2'b10;
    localparam DONE     = 2'b11;

    reg [1:0] state;
    reg [1:0] next_state;

    // BUG 1: State register has no reset. On power-up,
    // state is X, and the FSM never reaches a known state.
    always @(posedge clk) begin
        state <= next_state;
    end

    // Next state logic
    always @(*) begin
        next_state = state;
        prod_ready = 1'b0;
        cons_valid = 1'b0;
        transfer_done = 1'b0;

        case (state)
            IDLE: begin
                prod_ready = 1'b1;
                if (prod_valid)
                    next_state = WAITING;
            end

            WAITING: begin
                cons_valid = 1'b1;
                // BUG 2: If cons_ready never asserts, we stay
                // in WAITING forever. No timeout, no escape.
                if (cons_ready)
                    next_state = ACTIVE;
            end

            ACTIVE: begin
                cons_valid = 1'b1;
                prod_ready = 1'b1;
                transfer_done = 1'b1;
                next_state = DONE;
            end

            DONE: begin
                // BUG 3: DONE transitions back to WAITING, not IDLE.
                // A new transaction starts before prod_valid is checked.
                next_state = WAITING;
            end

            default: next_state = IDLE;
        endcase
    end

endmodule

Three bugs are planted here deliberately:

No reset on the state register
A deadlock path when the consumer stalls permanently
A wrong state transition that skips the idle handshake

Writing the Formal Verification Wrapper

The formal wrapper instantiates the DUT and houses all SVA properties. It uses assume for input constraints, assert for properties we want to prove, and cover for reachability goals.

// handshake_ctrl_fv.sv
module handshake_ctrl_fv (
    input wire clk,
    input wire rst_n
);

    // Free variables (inputs to DUT)
    wire prod_valid;
    wire cons_ready;

    // DUT outputs
    wire prod_ready;
    wire cons_valid;
    wire transfer_done;

    // Instantiate DUT
    handshake_ctrl dut (
        .clk          (clk),
        .rst_n        (rst_n),
        .prod_valid   (prod_valid),
        .prod_ready   (prod_ready),
        .cons_valid   (cons_valid),
        .cons_ready   (cons_ready),
        .transfer_done(transfer_done)
    );

    // -------------------------------------------------------
    // Reset behavior
    // -------------------------------------------------------

    // After reset deasserts, the state must be known (IDLE).
    // We check this by asserting prod_ready should be high
    // and cons_valid should be low in the first cycle after reset.
    property reset_to_idle;
        @(posedge clk)
        $rose(rst_n) |=> (prod_ready == 1'b1 && cons_valid == 1'b0);
    endproperty

    assert property (reset_to_idle)
        else $error("FV FAIL: Reset did not land in IDLE");

    // -------------------------------------------------------
    // Handshake protocol: valid before ready is not allowed
    // on the producer side. prod_ready must come from the DUT
    // and should not assert when cons_valid is active.
    // -------------------------------------------------------

    property no_double_accept;
        @(posedge clk) disable iff (!rst_n)
        (cons_valid && !cons_ready) |-> !prod_ready;
    endproperty

    assert property (no_double_accept)
        else $error("FV FAIL: prod_ready asserted while consumer is stalled");

    // -------------------------------------------------------
    // Transfer done should only pulse for one cycle
    // -------------------------------------------------------

    property transfer_done_one_cycle;
        @(posedge clk) disable iff (!rst_n)
        transfer_done |=> !transfer_done;
    endproperty

    assert property (transfer_done_one_cycle)
        else $error("FV FAIL: transfer_done held for more than one cycle");

    // -------------------------------------------------------
    // Deadlock check: if cons_valid is asserted, the FSM
    // must eventually leave the WAITING state. We bound this
    // using a liveness-style assertion over a finite window.
    // -------------------------------------------------------

    // Track consecutive cycles where we are stuck waiting
    reg [4:0] wait_count;

    always @(posedge clk or negedge rst_n) begin
        if (!rst_n)
            wait_count <= 5'd0;
        else if (cons_valid && !cons_ready && !prod_ready)
            wait_count <= wait_count + 1;
        else
            wait_count <= 5'd0;
    end

    // If we have been stuck for 16 cycles, something is wrong
    property no_deadlock;
        @(posedge clk) disable iff (!rst_n)
        wait_count < 5'd16;
    endproperty

    assert property (no_deadlock)
        else $error("FV FAIL: Deadlock detected, FSM stuck for 16+ cycles");

    // -------------------------------------------------------
    // Output stability: cons_valid should not glitch low
    // once asserted during a transfer without a reset
    // -------------------------------------------------------

    property cons_valid_stable;
        @(posedge clk) disable iff (!rst_n)
        (cons_valid && !cons_ready) |=> cons_valid;
    endproperty

    assert property (cons_valid_stable)
        else $error("FV FAIL: cons_valid dropped without handshake completion");

    // -------------------------------------------------------
    // Reachability covers: prove transfer can complete
    // -------------------------------------------------------

    cover property (
        @(posedge clk) disable iff (!rst_n)
        $rose(transfer_done)
    );

    cover property (
        @(posedge clk) disable iff (!rst_n)
        $rose(rst_n) ##[1:20] $rose(transfer_done)
    );

endmodule

The SymbiYosys Configuration File

The .sby file tells SymbiYosys which files to use, which top module to verify, which solver to use, and what mode to run in.

# handshake.sby
[options]
mode bmc
depth 30
multiclock off

[engines]
smtbmc yices

[script]
read -formal handshake_ctrl.v
read -formal handshake_ctrl_fv.sv
prep -top handshake_ctrl_fv

[files]
handshake_ctrl.v
handshake_ctrl_fv.sv

A few things worth understanding here:

mode bmc runs bounded model checking. It checks all assertions up to depth clock cycles from any reachable initial state.

depth 30 means the solver explores traces up to 30 cycles long. For detecting deadlock in this design, 30 is more than enough. For deep protocol bugs, you may need to increase this.

smtbmc yices selects the Yices2 backend via the SMT-BMC bridge that SymbiYosys provides.

Running SymbiYosys

sby -f handshake.sby

The -f flag forces a clean run by removing any previous output directory.

Output will look something like this:

SBY  0:00:00 [handshake] Removing directory 'handshake'.
SBY  0:00:00 [handshake] Copy 'handshake_ctrl.v' to 'handshake/src/handshake_ctrl.v'.
SBY  0:00:00 [handshake] Copy 'handshake_ctrl_fv.sv' to 'handshake/src/handshake_ctrl_fv.sv'.
SBY  0:00:00 [handshake] engine_0: smtbmc yices
SBY  0:00:01 [handshake] Generating SMTLIB2 model...
SBY  0:00:02 [handshake] engine_0: ## 0:00:00 Checking assumptions...
SBY  0:00:02 [handshake] engine_0: ## 0:00:00 BMC: step 1
...
SBY  0:00:03 [handshake] engine_0: ## 0:00:01 BMC: FAILED (assert)
SBY  0:00:03 [handshake] engine_0: Status: FAILED
SBY  0:00:03 [handshake] engine_0: Writing trace to 'handshake/engine_0/trace.vcd'
SBY  0:00:03 [handshake] DONE (FAIL, rc=2)

It fails immediately. The first thing that fails will be the reset property.

Reading the Counterexample

SymbiYosys writes a VCD file to the engine output directory.

gtkwave handshake/engine_0/trace.vcd

You will see that after rst_n rises, the state register does not land in IDLE. It holds the value X because it was never reset. prod_ready is therefore undefined and the assertion fires on cycle 1.

This is Bug 1.

Fix 1: Add a Synchronous Reset to the State Register

always @(posedge clk) begin
    if (!rst_n)
        state <= IDLE;
    else
        state <= next_state;
end

Run SymbiYosys again.

sby -f handshake.sby

The reset assertion now passes. The tool moves on and finds the next failure. This time it is the deadlock assertion.

SBY engine_0: BMC: FAILED (assert)
SBY engine_0: Writing trace to 'handshake/engine_0/trace.vcd'

Reading the Deadlock Trace

Open the new VCD. You will see:

Reset deasserts
prod_valid asserts for one cycle
FSM moves from IDLE to WAITING
cons_valid asserts
cons_ready never asserts
wait_count increments every cycle
At cycle 17, wait_count reaches 16 and the assertion fires

This is Bug 2. The FSM has no way to escape WAITING if the consumer never responds.

Fix 2: Add a Timeout and an Abort Path

reg [4:0] timeout_cnt;

always @(posedge clk) begin
    if (!rst_n)
        timeout_cnt <= 5'd0;
    else if (state == WAITING)
        timeout_cnt <= timeout_cnt + 1;
    else
        timeout_cnt <= 5'd0;
end

// In the next state logic, add a timeout exit from WAITING
WAITING: begin
    cons_valid = 1'b1;
    if (cons_ready)
        next_state = ACTIVE;
    else if (timeout_cnt == 5'd15)
        next_state = IDLE;  // Abort and return to idle
end

Run again.

sby -f handshake.sby

The deadlock assertion now passes. The tool finds the next failure: the wrong transition in DONE.

SBY engine_0: BMC: FAILED (assert) -- no_double_accept

Reading the State Transition Trace

The VCD now shows:

A transfer completes
FSM enters DONE
DONE immediately transitions to WAITING without passing through IDLE
In WAITING, cons_valid asserts
Simultaneously, prod_ready is still high from the brief passage through ACTIVE
The no_double_accept assertion fires

This is Bug 3. After a transfer, the FSM skips IDLE entirely and goes back to hunting for a consumer without checking whether the producer has a new transaction ready.

Fix 3: Return to IDLE from DONE

DONE: begin
    transfer_done = 1'b1;
    next_state = IDLE;  // Return to IDLE, not WAITING
end

Also remove transfer_done from the ACTIVE state since we moved it to DONE:

ACTIVE: begin
    cons_valid = 1'b1;
    prod_ready = 1'b1;
    next_state = DONE;
end

Run again.

sby -f handshake.sby

The Full Fixed Design

// handshake_ctrl_fixed.v
module handshake_ctrl (
    input  wire        clk,
    input  wire        rst_n,

    input  wire        prod_valid,
    output reg         prod_ready,

    output reg         cons_valid,
    input  wire        cons_ready,

    output reg         transfer_done
);

    localparam IDLE     = 2'b00;
    localparam WAITING  = 2'b01;
    localparam ACTIVE   = 2'b10;
    localparam DONE     = 2'b11;

    reg [1:0] state;
    reg [1:0] next_state;
    reg [4:0] timeout_cnt;

    // FIX 1: Synchronous reset on state register
    always @(posedge clk) begin
        if (!rst_n)
            state <= IDLE;
        else
            state <= next_state;
    end

    // FIX 2: Timeout counter
    always @(posedge clk) begin
        if (!rst_n)
            timeout_cnt <= 5'd0;
        else if (state == WAITING)
            timeout_cnt <= timeout_cnt + 1;
        else
            timeout_cnt <= 5'd0;
    end

    always @(*) begin
        next_state    = state;
        prod_ready    = 1'b0;
        cons_valid    = 1'b0;
        transfer_done = 1'b0;

        case (state)
            IDLE: begin
                prod_ready = 1'b1;
                if (prod_valid)
                    next_state = WAITING;
            end

            WAITING: begin
                cons_valid = 1'b1;
                if (cons_ready)
                    next_state = ACTIVE;
                else if (timeout_cnt == 5'd15)
                    next_state = IDLE;
            end

            ACTIVE: begin
                cons_valid = 1'b1;
                prod_ready = 1'b1;
                next_state = DONE;
            end

            // FIX 3: Return to IDLE, assert transfer_done here
            DONE: begin
                transfer_done = 1'b1;
                next_state    = IDLE;
            end

            default: next_state = IDLE;
        endcase
    end

endmodule

Running the Full Clean Pass

sby -f handshake.sby

Expected output:

SBY  0:00:02 [handshake] engine_0: ## 0:00:01 BMC: step 30
SBY  0:00:02 [handshake] engine_0: ## 0:00:01 BMC: PASSED
SBY  0:00:02 [handshake] engine_0: Status: passed
SBY  0:00:02 [handshake] DONE (PASS, rc=0)

All assertions pass for all traces up to 30 cycles deep.

Running Cover Mode to Check Reachability

A passing BMC result does not tell you whether transfer_done is ever reachable. The cover properties handle that.

Add a second sby configuration for cover mode:

# handshake_cover.sby
[options]
mode cover
depth 30

[engines]
smtbmc yices

[script]
read -formal handshake_ctrl.v
read -formal handshake_ctrl_fv.sv
prep -top handshake_ctrl_fv

[files]
handshake_ctrl.v
handshake_ctrl_fv.sv

sby -f handshake_cover.sby

Expected output:

SBY engine_0: Cover: PASSED (2 reached)
SBY DONE (PASS, rc=0)

Both cover properties are reachable. The solver found a valid input sequence that causes transfer_done to assert within 30 cycles of reset.

Running k-Induction for Unbounded Proof

BMC proves properties up to a depth bound. k-Induction can prove them for all depths.

# handshake_prove.sby
[options]
mode prove
depth 20

[engines]
smtbmc yices

[script]
read -formal handshake_ctrl.v
read -formal handshake_ctrl_fv.sv
prep -top handshake_ctrl_fv

[files]
handshake_ctrl.v
handshake_ctrl_fv.sv

sby -f handshake_prove.sby

If all assertions hold under induction, SymbiYosys prints:

SBY engine_0: Inductive step: PASSED
SBY DONE (PASS, rc=0)

This is a stronger result. It means the properties hold not just up to 20 cycles but for any reachable trace of any length.

SVA Reference: Patterns Used in This Post

Here is a quick reference for the SVA constructs used above.

Implication:

// If A is true at the current clock, then B must be true at the same clock
A |-> B

// If A is true now, then B must be true one cycle later
A |=> B

Sequence operators:

// B must occur exactly 2 cycles after A
A ##2 B

// B must occur between 1 and 5 cycles after A
A ##[1:5] B

// B must occur eventually after A (no bound)
A ##[1:$] B

Disable iff:

// Property is only checked when rst_n is high
property p;
    @(posedge clk) disable iff (!rst_n)
    A |-> B;
endproperty

$rose and $fell:

// True on the first clock where sig goes 0 to 1
$rose(sig)

// True on the first clock where sig goes 1 to 0
$fell(sig)

$past:

// B must be true if A was true one cycle ago
$past(A) |-> B

What Formal Verification Does Not Do

It is worth being clear about the limits.

Formal BMC proves properties up to the depth bound. If a bug only appears at cycle 100 and your depth is 30, it will not be found unless you use induction or increase the bound.

Formal does not check timing in the analog sense. It reasons about logical behavior, not setup/hold violations or clock skew.

Formal does not help if your properties are wrong. If you write an incorrect assertion that passes trivially, the tool will report a pass for the wrong reason. Writing good properties is the hard part.

Formal also scales poorly with design size. A single module like this handshake controller runs in seconds. A full CPU pipeline with hundreds of state bits can take hours or become intractable. For large designs, bounded model checking is usually applied module by module, with interface assumptions replacing upstream logic.

Summary

At this point you have:

Installed SymbiYosys and Yices2 from source
Written a buggy handshake controller
Created a formal verification wrapper with SVA properties covering reset, deadlock, output stability, and reachability
Configured and run SymbiYosys in BMC, cover, and prove modes
Found three bugs using counterexample traces
Fixed each bug and verified the fix with a clean pass

The bugs found here, missing reset, unbounded wait, and wrong state transition, are exactly the kind that survive simulation for months and surface only in silicon or late in integration. Formal finds them in seconds.

Write the properties before you write the design. Let the solver do the exhaustive work.