Mastering Formal Verification of VHDL Modules with PSL

When designing VHDL for safety‑critical FPGA applications, simply writing testbenches isn’t enough. Engineers must prove that a module behaves exactly as specified, free of hidden side‑effects. Formal verification provides that mathematical assurance.

Formal verification bridges the gap between requirements and implementation by proving that every possible input sequence satisfies the design’s properties. It’s indispensable for certifying medical devices, avionics systems, or any domain where DO‑254 certification is required.

In this guest post, Michael Finn Jørgensen—an experienced formal verification practitioner—shares practical insights and actionable tips. The example below builds on the familiar AXI FIFO tutorial How to make an AXI FIFO in block RAM using the ready/valid handshake and demonstrates how to apply PSL to a real VHDL design.

What Is Formal Verification?

Formal verification (FV) is a systematic, pre‑synthesis method that guarantees a design’s correctness for all input combinations. Unlike conventional testbenches, which rely on manually crafted stimuli, FV specifies properties that must hold at every clock cycle. A SAT solver then exhaustively proves that these properties are satisfied—or pinpoints a counter‑example if they’re not.

Two core techniques power FV:

• Bounded Model Checking (BMC) – checks a finite number of cycles, starting from reset.
• Induction Proof – verifies that if a state is valid, all subsequent states remain valid. This requires a complete set of properties but yields guarantees for an infinite number of cycles.

Because BMC can be run with only a few properties, it’s often the first line of defense. Induction, while more demanding, delivers absolute certainty.

Why Use Formal Verification?

FV excels at uncovering elusive bugs because it explores the entire input space automatically. When a fault is discovered, the tool produces a concise waveform that pinpoints the exact cycle where the property violated—much easier to debug than a long simulation trace.

Although FV is a powerful unit‑testing tool, it doesn’t replace hand‑crafted integration tests. As module size grows, the solver’s runtime can become prohibitive. Nevertheless, investing time in FV reduces overall debugging effort and accelerates time‑to‑market.

Writing Properties in PSL

PSL (Property Specification Language) is the lingua franca of formal verification in VHDL. Properties are typically stored in a separate .psl file that the solver reads during the verification phase.

Three PSL keywords describe properties:

• assert – guarantees that a condition will always hold.
• assume – states assumptions about the inputs.
• cover – checks whether a particular scenario can ever occur.

PSL files can also contain ordinary VHDL declarations and processes, allowing you to create auxiliary signals for complex assertions.

Every PSL file starts with a vunit block that ties the file to a specific entity:

vunit INSTANCE_NAME(ENTITY_NAME(ARCHITECTURE_NAME)) {
}

Followed by a default clock declaration:

default clock is rising_edge(clk);

Property syntax looks like this:

LABEL : assert always {PRECONDITION} |-> {POSTCONDITION}
LABEL : assume always {PRECONDITION} |-> {POSTCONDITION}

Use |=> for next‑cycle assertions:

LABEL : assert always {PRECONDITION} |=> {POSTCONDITION}

Inside conditions you can use stable to enforce that a signal doesn’t change between cycles, and you can chain conditions using {C1; C2} to express sequential constraints.

Installing the Required Tools

Leading commercial tools (e.g., ModelSim) support formal verification, but the free Student Edition lacks this feature. Fortunately, a robust open‑source stack is available for Linux (and via WSL on Windows). The following guide uses Ubuntu 20.04 LTS but works on any recent Debian‑based distro.

Prerequisites

sudo apt update && sudo apt upgrade

Install essential development libraries:

sudo apt install build-essential clang bison flex libreadline-dev \
    gawk tcl-dev libffi-dev git mercurial graphviz \
    xdot pkg-config python python3 libftdi-dev gperf \
    libboost-program-options-dev autoconf libgmp-dev \
    cmake gnat gtkwave

Yosys and SymbiYosys

git clone https://github.com/YosysHQ/yosys
cd yosys
make
sudo make install
cd ..

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

git clone https://github.com/SRI-CSL/yices2
cd yices2
autoconf
./configure
make
sudo make install
cd ..

GHDL and Yosys Plugin

git clone https://github.com/ghdl/ghdl
cd ghdl
./configure --prefix=/usr/local
make
sudo make install
cd ..

git clone https://github.com/ghdl/ghdl-yosys-plugin
cd ghdl-yosys-plugin
make
sudo make install
cd ..

Download the Example Project

Fill out the form below to receive a ZIP archive containing the complete AXI FIFO source, PSL file, and verification scripts.

Worked Example: Formal Verification of an AXI FIFO

Below we outline the key property categories for a FIFO and illustrate how to encode them in PSL.

Reset Handling

f_reset : assume {rst};

Because the always keyword is omitted, this assumption applies only to the first cycle after reset. A label convention (f_) helps identify failures.

f_after_reset_valid : assert always {rst} |=> {not out_valid};
f_after_reset_ready : assert always {rst} |=> {in_ready};
f_after_reset_head  : assert always {rst} |=> {count = 0};

Notice that internal signals such as count can be referenced because the vunit declaration includes the architecture name.

FIFO Full and Empty Signaling

f_empty : assert always {count = 0} |-> {not out_valid};
f_full  : assert always {count = ram_depth-1} |-> {not in_ready};

AXI Protocol Compliance

f_in_data_stable : assume always
   {in_valid and not in_ready and not rst} |=>
   {stable(in_valid) and stable(in_data)};

f_out_data_stable : assert always
   {out_valid and not out_ready and not rst} |=>
   {stable(out_valid) and stable(out_data)};

For the ready signal’s stability:

f_out_ready_stable : assume always
   {out_ready and not out_valid and not rst} |=>
   {stable(out_ready)};

f_in_ready_stable : assert always
   {in_ready and not in_valid and not rst} |=>
   {stable(in_ready)};

FIFO Ordering

Ordering guarantees that earlier writes exit before later writes. We model this with auxiliary signals that remember when particular data values entered or exited.

signal f_sampled_in_d1  : std_logic := '0';
signal f_sampled_in_d2  : std_logic := '0';

p_sampled : process (clk)
begin
   if rising_edge(clk) then
      if in_valid then
         if in_data = f_value_d1 then
            f_sampled_in_d1 <= '1';
         end if;
         if in_data = f_value_d2 then
            f_sampled_in_d2 <= '1';
         end if;
      end if;

      if out_valid then
         if out_data = f_value_d1 then
            f_sampled_out_d1 <= '1';
         end if;
         if out_data = f_value_d2 then
            f_sampled_out_d2 <= '1';
         end if;
      end if;

      if rst = '1' then
         f_sampled_in_d1  <= '0';
         f_sampled_in_d2  <= '0';
         f_sampled_out_d1 <= '0';
         f_sampled_out_d2 <= '0';
      end if;
   end if;
end process p_sampled;

Declare the data values as unconstrained constants so the solver can choose any bit pattern:

signal f_value_d1 : std_logic_vector(ram_width - 1 downto 0);
signal f_value_d2 : std_logic_vector(ram_width - 1 downto 0);
attribute anyconst : boolean;
attribute anyconst of f_value_d1 : signal is true;
attribute anyconst of f_value_d2 : signal is true;

Finally, encode the ordering constraints:

f_fifo_ordering_in : assume always
   {f_sampled_in_d2} |->
   {f_sampled_in_d1};

f_fifo_ordering_out : assert always
   {f_sampled_out_d2} |->
   {f_sampled_out_d1};

Running Formal Verification

Create a axi_fifo.sby script for the sby tool:

[tasks]
bmc

[options]
bmc: mode bmc
bmc: depth 10

[engines]
smtbmc

[script]
ghdl --std=08 -gram_width=4 -gram_depth=8 axi_fifo.vhd axi_fifo.psl -e axi_fifo
prep -top axi_fifo

[files]
axi_fifo.psl
axi_fifo.vhd

Run the verification:

sby --yosys ";yosys -m ghdl" -f axi_fifo.sby

A successful run prints:

[axi_fifo_bmc] DONE (PASS, rc=0)

Adjusting depth beyond the FIFO depth ensures the solver explores full‑capacity scenarios.

Mutation Testing

To gauge the completeness of your property set, deliberately inject a small bug—such as removing the logic that drives out_valid—and rerun FV. If the solver reports an assertion failure, you’ve verified that your properties are expressive enough to catch that error.

Example failure message:

Assert failed in axi_fifo: i_axi_fifo.f_out_data_stable

Open the generated trace.vcd in GTKWave to pinpoint the exact cycle where the property violated.

Cover Statements

Cover statements are useful for asserting that a particular scenario is reachable. For example, to verify that the FIFO can be filled and then emptied:

f_full_to_empty : cover {
   rst = '1';
   rst = '0'[*];
   rst = '0' and count = ram_depth-1;
   rst = '0'[*];
   rst = '0' and count = 0};

Adjust the sby script to include the cover task:

[tasks]
bmc
cover

[options]
bmc: mode bmc
bmc: depth 10
cover: mode cover

Successful coverage yields:

Reached cover statement at i_axi_fifo.f_full_to_empty in step 15.

Changing count = ram_depth-1 to count = ram_depth will make the cover unreachable, demonstrating the tool’s sensitivity to property accuracy.

Next Steps

• Introduction to the PSL Language
• Formal Verification Fundamentals
• Video Series: Getting Started with Formal Verification
• Advanced Formal Verification Articles
• Mini‑Project Repository for Formal Verification