What kind of VHDL process is this?

Question

This is from an example that comes with VUnit inside the array_axis_vcs fifo.vhd file.

  PslChecks : block is
    constant dx : std_logic_vector(d'left downto 0) := (others => 'X');
    constant du : std_logic_vector(d'left downto 0) := (others => 'U');
  begin
    assert always (not rst and wr -> not (d ?= dx or d ?= du))@rising_edge(clkw)
      report "wrote X|U to FIFO";
    assert always (not rst and f -> not wr)@rising_edge(clkw)
      report "Wrote to FIFO while full";
    assert always (not rst and e -> not rd)@rising_edge(clkr)
      report "Read from FIFO while empty";
  end block PslChecks;

My simulator is not able to understand these assert statements.

What kind of VHDL is this? How can this be written in "normal VHDL" so it works with my ActiveHDL 11.1? I have never seen block and assert always in my life in VHDL before this. I can't find these in the VHDL 2008 LRM as well.

It claims to be a block instead of a process. What makes you think it's a process? It's using PSL as the block name suggests : does your simulator support PSL? — , Jan 04 '21 at 17:40
A cursory scan af Aldec's website hints at PSL support, but I'd have to register with them to pursue this further. — , Jan 04 '21 at 17:46
PSL? I have never used this. Am I supposed to know about it? — gyuunyuu, Jan 04 '21 at 17:52

score 4 · Answer 1 · 2021-01-05T16:15:20.927

Incomplete answer.

First note this is a block, not a process. A block wraps some declarations and concurrent statements (which can include processes) together, without exposing those details to the wider design.

But the problem here is not the block; it's that these Asserts are written in PSL, Property Specification Language, which is used to extend VHDL's formal verification capabilities. I'll let the linked Wiki article describe PSL in more details. I have rarely come across it myself...

See also "Property (PSL)" in the VHDL-2008 LRM index or or search for PSL in the entire LRM.

Most VHDL simulators allow PSL embedded in VHDL code, as here; (including the open source ghdl, as far as I understand).

And the Aldec website hints at PSL support in Active-HDL (though without opening an account there, I can't look any more closely than that. This is the incomplete aspect!).

So my guess is that your best way forward is to read the Aldec docs and find out why PSL support isn't enabled (sim version? missing compile option?) and enable it. And add to the question (or answer it yourself) with your findings.

If PSL assertions were trivial to re-write in VHDL, PSL support wouldn't be available, so rewriting these as VHDL is probably not optimal...

If you can't enable PSL, or move to a simulator that understands it, you need some way forward...

In that case I'd suggest adding a boolean constant (or generic) use_psl, and surround this block with label: if use_psl generate ... end generate. That'll let you move forward, and the design will work equally well, but obviously you lose the verification provided by this block.

Finally it's probably worth reporting this to the Vunit team via their github site : their support is excellent and they may well have answers I have overlooked.

tmeissner · Accepted Answer · 2021-01-06T16:15:47.217

If I remember correctly, I'm the original origin of that PSL code. PSL was integrated to VHDL with the VHDL-08 standard. GHDL is supporting this. Most (vendor) simulators do only support PSL in so-called 'PSL comments'. With these comments, you could also let the PSL stuff in your code using a simulator without (proper) PSL support.

For example:

  PslChecks : block is
    constant dx : std_logic_vector(d'left downto 0) := (others => 'X');
    constant du : std_logic_vector(d'left downto 0) := (others => 'U');
  begin
    -- psl assert always (not rst and wr -> not (d ?= dx or d ?= du))@rising_edge(clkw)
    --   report "wrote X|U to FIFO";
    -- psl assert always (not rst and f -> not wr)@rising_edge(clkw)
    --   report "Wrote to FIFO while full";
    -- psl assert always (not rst and e -> not rd)@rising_edge(clkr)
    --   report "Read from FIFO while empty";
  end block PslChecks;

Another possibility is to rewrite them in pure VHDL. The PSL which is used here is simple. -> is a simple implication like if this than that. So the 3rd PSL assert can be rewritten as (no warranties for correctness):

process is
begin
  wait until rising_edge(clkr);
  if not rst and e then
    assert not rd
    report "Read from FIFO while empty"
    severity failure;
  end if;
end process;

Good introduction to rewriting a simple PSL assertion in pure VHDL! Is there a "psl" missing in one of the commented asserts? — , Jan 06 '21 at 13:15
Thanks. In this case, rewriting it as VHDL is easy. However, there are much more powerful PSL operators, which aren't so easy to mimic. And you're right, there was a psl missing in the second comment. Thanks for the hint, I added it. — tmeissner, Jan 06 '21 at 16:17

What kind of VHDL process is this?

2 Answers2