Having had to solve two black box debug issues this year, both related to AXI, and met two new colleagues who both had prior experience of formal verification, I was keen to explore better ways to verify some common RTL coding situations. The only restriction is that I am using free tools outside of work to explore the art of the possible.

• Introduction
• Tool Used
• PSL in QuestaSim
• In-line
• Separate File
• Waveforms
• Unclocked Assertions
• Labels
• AXI-Stream Example
• QuestaSim TCL Commands
• Conclusions
• References

Introduction

The Property Specification Language (PSL) is an IEEE standard (1850) now integrated in the VHDL language as of VHDL-2008.

PSL is an abbreviation for Property Specification Language. A property is a boolean-valued fact about a design-under-test. Right now, PSL works alongside a design written in VHDL or Verilog, but in future PSL may be extended to work with other languages. Properties written in PSL may be embedded within the HDL code as comments or may be placed in a separate file alongside the HDL code.

Properties are used to create assertions. An assertion is an instruction to a verification tool to prove that a given property holds. The verification tool could be a simulator (dynamic verification) or a model checker that constructs a mathematical proof of a property (static formal verification).

The Designer's Guide to PSL - Doulos

I read in an article posted on VHDLwhiz that the Free QuestaSim software from Intel supported PSL. The article is posted under the title of "Formal Verification", so some care needs to be taken with getting too excited about what we can acheive here. I also found few articles on the Internet explaining how to use PSL in VHDL. There are lots of articles explaining System Verilog Assertions (SVA), and plenty on PSL itself which is a big topic, and lots of people asking how to use them in QuestaSim. So this blog is primarily about getting some basic examples of PSL working with VHDL code in Intel's Free QuestaSim simulator, and exploring some of the features available.

For those new to the topic of how to use PSL and why, it is necessary to understand there are two applications that benefit from the same PSL code written once for your VHDL.

What is Assertion-based Verification (ABV)

Assertions when used with simulation are checking the design block dynamically at the functional level early in the process. Formal verification uses only a subset of these assertion rules statically at the behavioral level after simulation is verified. Based on the amount of time designers spend at the functional level and the limitations with formal verification, checking assertions during simulation offers an early indication of a potential problem and can ultimately reduce the overall debugging time needed. Formal verification further increases the thoroughness but without this early indication, the corrections can take much longer or be missed entirely.

Assertion-Based Verification - www.aldec.com

QuestaSim enables ABV through support of SystemVerilog Assertion (SVA) constructs and the Property Specification Language (PSL).

Siemens QuestaSim Fact Sheet

Formal verification software is an additional (and I hear expensive) software license. With the free Questasim we can only test Assertion-based Verification with PSL.

Tool Used

Questa Intel Starter FPGA Edition-64 2023.3
Revision: 2023.07
Date: Jul 17 2023

PSL in QuestaSim

The following two examples use the same VHDL RTL component, but specify the PSL in two different ways. The VHDL RTL component used here is a classic pulse generator, given a multi-cycle pulse on the input, create a single cycle pulse on the output.

In-line

The PSL code can be specified along side the RTL by using embedded comments as shown below. Each line of PSL needs to start with -- psl.

library ieee;
  use ieee.std_logic_1164.all;

entity pulse_gen is
  port(
    clk : in  std_logic;
    i   : in  std_logic;
    o   : out std_logic
  );
end entity;


architecture rtl of pulse_gen is

  signal i_d : std_logic;

begin

  -- Two ways of writing "next clock cycle"
  -- psl i_high  : assert (always {i}             |=> {i_d})          @rising_edge(clk);
  -- psl i_low   : assert (always not i            -> next (not i_d)) @rising_edge(clk);
  -- Specify an expected sequence
  -- psl o_pulse : assert (always {not i and i_d} |-> {o; not o})     @falling_edge(clk);

  process(clk)
  begin
    if rising_edge(clk) then
      i_d <= i;
    end if;
  end process;

  o <= i_d and not i;

end architecture;

The above PSL code uses two different ways of specifying "next clock", firstly with the "|=>" operator and then with "-> next".

Separate File

The same PSL code can be provided via an external file. Firstly remove the embedded PSL as the assertion names will clash between the VHDL file and the PSL file.

architecture rtl of pulse_gen is

  signal i_d : std_logic;

begin

  process(clk)
  begin
    if rising_edge(clk) then
      i_d <= i;
    end if;
  end process;

  o <= i_d and not i;

end architecture;

Move the PSL lines out to a PSL file and remove the -- psl prefixes. A vunit must now be specified to tie the two halves of code together.

vunit pulse_gen_i(pulse_gen(rtl)) {
  i_high  : assert (always {i}             |=> {i_d})          @rising_edge(clk);
  -- Defining a property
  property P1 is (always not i              -> next (not i_d)) @rising_edge(clk);
  i_low   : assert P1;
  -- A specific sequence
  o_pulse : assert (always {not i and i_d} |-> {o; not o})     @falling_edge(clk);
}

The above code takes the opportunity to provide an example of a property given PSL is about specifying properties. This file needs to be added to the vcom command line with the -pslfile command line switch as follows.

vcom -quiet -2008 ^
  -pslfile %SRC%\pulse_gen.psl ^
  %SRC%\pulse_gen.vhdl ^
  %SRC%\test_pulse_gen.vhdl

Waveforms

The signals for your RTL can now include the assertions and assumptions you have defined in your PSL code. Each of these is a group including the constituent parts.

If I redefine the output sequence to expect o to go high for two clock cycles with:

o_pulse : assert (always {not i and i_d} |-> {o; o; not o}) @falling_edge(clk);

The simulation window now shows the point in time where the assertion failed because the RTL does not implement the PSL defined timing of a pulse lasting for two clock cycles.

Unclocked Assertions

You are not allowed unclock assertions, even when the assertions are supposed to be made in the same clock cycle (i.e. asynchronously) because they are causal from pure combinatorial logic. It might compile with 'vcom' but then and 'vsim' complains. The unclocked combinatorial logic issue can be circumnavigated by using the falling edge of the clock.

o_pulse : assert (always {not i and i_d} |-> {o}) @falling_edge(clk);

Or they can be replaced by a standard VHDL assert statements of the form of either of these two lines:

  f1 : assert not(falling_edge(clk) and o /= (not i and i_d));
  f2 : assert not falling_edge(clk) or o = (not i and i_d);

PSL is intended for designs with synchronous timing.

The Structure of PSL, Doulos

Labels

The label names defined in your PSL are the only refernce provided by QuestaSim, so make them descriptive. If you have two architectures for the same entity, the labels used for assertions, assumptions and covers must differ in each architecture. Now it feels a bit pointless specifying the architecture name in the vunit declaration.

Symbol "f_in_ready_stable" has already been declared in this region.

AXI-Stream Example

The next example is not that much more complicated and uses the axi_delay component taken from Working With AXI Streaming Data. Here a default clock has been defined to reduce clutter. Two local signals have also been created called give and give using standard VHDL syntax. A whole process could be defined if required. These two signals defined in PSL appear in the list of available signals for simulation, and hence this PSL file defines debug that is effectively a separate layer from the RTL.

vunit axi_delay_simple(axi_delay(simple)) {
  signal take : std_logic := '0';
  signal give : std_logic := '0';
  take <= s_axi_valid and s_axi_ready;
  give <= m_axi_valid and m_axi_ready;

  default clock is rising_edge(clk);

  -- Input valid/data must be stable until accepted.
  f1_in_data_stable : assume always
    {s_axi_valid and not s_axi_ready} |=>
    {stable(s_axi_valid) and stable(s_axi_data)};

  f1_in_data_stall1_cover : cover {s_axi_valid and not s_axi_ready};
  f1_in_data_stall2_cover : cover {not s_axi_valid and s_axi_ready};

  f1_in_ready_retracted : cover {
    s_axi_valid = '0' and s_axi_ready = '1';
    s_axi_ready = '0'
  };

  -- Output valid/data must be stable until accepted.
  f1_out_data_stable : assert always
    {m_axi_valid and not m_axi_ready} |=>
    {stable(m_axi_valid) and stable(m_axi_data)};

  f1_out_data_stall1_cover : cover {m_axi_valid and not m_axi_ready};
  f1_out_data_stall2_cover : cover {not m_axi_valid and m_axi_ready};

  f1_out_ready_retracted : cover {
    m_axi_valid = '0' and m_axi_ready = '1';
    m_axi_ready = '0'
  };
}

The above PSL code implements the check for the condition where "once TVALID is asserted, it must remain asserted until the handshake occurs". See the conditions below from the AXI-Stream protocol specification.

2.2 Handshake signaling

This section gives details of the handshake signaling and defines the relationship of the TVALID and TREADY signals.

The TVALID and TREADY handshake determines when information is passed across the interface. A two-way flow control mechanism enables both the Transmitter and Receiver to control the rate at which the data and control information is transmitted across the interface.

For a transfer to occur, both TVALID and TREADY must be asserted. Either TVALID or TREADY can be asserted first, or both can be asserted in the same ACLK cycle.

A Transmitter is not permitted to wait until TREADY is asserted before asserting TVALID. Once TVALID is asserted, it must remain asserted until the handshake occurs.

A Receiver is permitted to wait for TVALID to be asserted before asserting TREADY. It is permitted that a Receiver asserts and deasserts TREADY without TVALID being asserted.

The following sections give examples of the handshake sequence.

AMBA AXI-Stream Protocol Specification

There are no conditions defined for s_axi_ready and m_axi_ready remaining stable once asserted (until tvalid). This is because the AXI standard as stated above does not require this, and if someone does retract tready before tvalid the PSL must not assert failure as it is legal by the specification.

My PSL also creates several cover conditions to count when certain properties occur.

The cover points here are checking for the data stalling on ingest or egress and whether its throttling (tvalid) or backpressure (tready). There are also two cover definitions looking for the condition where tready was asserted and then retracted, mainly to see if that situation was ever tested.

  -- f1_in_data_stable written an alternative way
  f1_in_data_stable2 : assume always
    {s_axi_valid and not s_axi_ready} |=>
    {s_axi_valid = '1' and stable(s_axi_data)};

In trialing PSL syntax, I note that for f1_in_data_stable, stable(s_axi_valid) can be replaced by s_axi_valid = '1' for the same effect.

QuestaSim TCL Commands

You can cause the simulation to stop on an assertion fail with the following:

assertion fail -r / -action break

# ** Error: Assertion failed
#    Time: 100 ns Started: 90 ns  Scope: /test_axi_delay_err/axi_delay_i/f1_in_data_stable File: A:/Philip/Work/VHDL/Public/VHDL/AXI_Delay/axi_delay.psl Line: 7
# ** Note: Requesting simulation stop on assertion event
#    Time: 100 ns  Scope: /test_axi_delay_err/axi_delay_i/f1_in_data_stable File: A:/Philip/Work/VHDL/Public/VHDL/AXI_Delay/axi_delay.psl Line: 7

You can undo the effect of that command with:

assertion fail -r / -action continue

Also try more specific commands:

assertion action -cond fail -exec break /test_axi_delay/axi_delay_i/f1_in_data_stable
assertion action -cond fail -exec continue /test_axi_delay/axi_delay_i/f1_in_data_stable

cover terms can be reported in text to the console using the commands below. It's the same information as the screen shot above.

fcover report /test_axi_delay/axi_delay_i/f1_out_data_stall2_cover
fcover report /test_axi_delay/axi_delay_i/*

Conclusions

It is worth noting that if you use OSVVM, the AXI protocol will already be checked by the Bus Functional Models it uses. Now armed with some basics and ways of working it is time to get clever with PSL assertion-based verification using the class material at University of Bristol.

References

1. Github Source Code
2. Property Specification Language (PSL) - Wikipedia
3. IEEE Standard for Property Specification Language (PSL)
4. Formal verification in VHDL using PSL - VHDLwhiz
5. The Designer's Guide to PSL - Doulos
6. Course content for the Design Verification module at the University of Bristol
7. Modelsim 6.0 PSL Quick Guide
8. PSL/Sugar Quick Reference Card VHDL - VHDLCohen Publishing & Consulting