Jonathan Certes

Home / Resources / Dynamic verification of PSL properties with ghdl

Introduction

GHDL is an open-source simulator for the VHDL language. GHDL allows you to compile and execute your VHDL code directly in your PC. GHDL fully supports the 1987, 1993, 2002 versions of the IEEE 1076 VHDL standard, and partially the latest 2008 revision. By using a code generator (llvm, GCC or a builtin one), GHDL is much faster than any interpreted simulator.

Property Specification Language (PSL) is a temporal logic extending Linear Temporal Logic (LTL) with a range of operators for both ease of expression and enhancement of expressive power. It is widely used in the hardware design and verification industry, where formal verification tools (such as model checkers) and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design.

VHDL DUT

To verify a PSL property on a VHDL module, we must first consider a Device Under Test (DUT). Let's consider a 4-bit counter with asynchronous reset.

entity up_counter is
  port(
    clk     : in  std_logic;
    reset   : in  std_logic;
    counter : out std_logic_vector(3 downto 0)
  );
end up_counter;

architecture bhv of up_counter is
  signal counter_up : std_logic_vector(3 downto 0) := "0000";
begin
  process(clk, reset)
  begin
    if ( reset = '1' ) then
      counter_up <= (others => '0');
    elsif ( rising_edge(clk) ) then
      counter_up <= counter_up + 1;
    end if;
  end process;
  counter <= counter_up;
end bhv;

VHDL testbench with PSL

GHDL implements a subset of PSL. A PSL statement is considered as a process, so it is not allowed within a process.

PSL properties are temporal properties, so we must indicate to GHDL how time evolves within the process: i.e. the definition of PSL next() operator. In our case, next event is at next clock rising edge.

Here is an example of a testbench with two PSL properties. For information, both PSL properties do not hold but simulation only shows one assertion violation. This is a limitation of dynamic verification.

entity testbench is
end testbench;

architecture bhv of testbench is
  signal clk     : std_logic := '0';
  signal reset   : std_logic := '0';
  signal counter : std_logic_vector(3 downto 0);
begin
  default clock is rising_edge(clk);  -- definition of PSL next()

  -- PSL:
  psl_end_count   : assert eventually!(counter = "1111");
  psl_start_count : assert always((counter = "0000") -> next(counter = "0001"));

  DUT : entity up_counter(bhv)
  port map (
    clk     => clk,
    reset   => reset,
    counter => counter
  );

  process begin
    clk <= '0';
    wait for 10 ns;
    clk <= '1';
    wait for 10 ns;
  end process;

  process begin
    wait for 365 ns;
    reset <= '1';
    wait; -- forever
  end process;
end bhv;

If we want to show that both properties do not hold, this testbench can be modified to always set signal reset to 1.

Makefile

Now, we must call ghdl to build our testbench. Then we run the simulation. Here, a 400ns simulation time is enough to show one PSL assertion violation.

Here is a Makefile that provides the recipe (make sure to indent with tabulations):

all: testbench
    ghdl-gcc -r $^ --vcd="output.vcd" --stop-time=400ns

testbench: counter.vhd testbench.vhd
    ghdl-gcc -a --std=08 --ieee=synopsys counter.vhd testbench.vhd
    ghdl-gcc -e --std=08 --ieee=synopsys testbench

clean:
    ghdl-gcc --remove --std=08 --ieee=synopsys
    $(RM) output.vcd

Associated resources

Here is an archive which contains the discussed example and its Makefile.

---