Support to evaluate PSL endpoints in VHDL code #45

tmeissner · 2016-03-08T09:11:55Z

GHDL already supports the PSL endpoint statement, which triggers at the last cycle of a sequence which was hit. However, you only can evaluate the endpoint in PSL code. In other simulators it is possible to read the value of the endpoint in VHDL code like this:

-- psl endpoint e_test is {req; not(grant); grant}@rising_edge(clk);

process is
begin
  wait until e_test;
  report "e_test hit";
  wait;
end process;

You can find an other example here: http://www.cvcblr.com/blog/?p=810

I don't know, if evaluating PSL endpoints in VHDL is defined in the PSL standard, but the tools that I now (Modelsim/Questa) support that. I will try on edaplayground, if Riviera also supports that, but I think it does. In the IEEE PSL standard endpoint was replaced by the ended() function, which is similar. But GHDL don't supports any PSL functions, so it would be a more easy way to enhance the already supported endpoint statement.

The text was updated successfully, but these errors were encountered:

tmeissner · 2016-03-08T19:05:44Z

Here is my test case:

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

library std;
use std.env.all;


entity psl_test_endpoint is
end entity psl_test_endpoint;


architecture test of psl_test_endpoint is


  signal s_rst_n : std_logic := '0';
  signal s_clk   : std_logic := '0';
  signal s_write : std_logic;
  signal s_read  : std_logic;


begin


  s_rst_n <= '1' after 100 ns;
  s_clk   <= not s_clk after 10 ns;


  TestP : process is
  begin
    report "RUNNING psl_test_endpoint test case";
    report "==========================================";
    s_write <= '0';
    s_read  <= '0';
    wait until s_rst_n = '1' and rising_edge(s_clk);
    s_write <= '1';
    wait until rising_edge(s_clk);  -- endpoint is be active
    s_read  <= '1';
    wait until rising_edge(s_clk);
    s_write <= '0';
    s_read  <= '0';
    wait until rising_edge(s_clk);
    stop(0);
  end process TestP;


  -- psl default clock is rising_edge(s_clk);
  -- sequence & endpoint definition
  -- psl endpoint E_TEST is {not(s_write); s_write};


  -- It's not possible to use endpoints in VHDL code
  EndpointP: process is
  begin
    wait until E_TEST;
    report "TEST";
    wait;
  end process EndpointP;

$ ghdl -a --std=08 -fpsl psl_test_endpoint.vhdproduces following error: psl_test_endpoint.vhd:55:16: PSL declaration "e_test" not allowed in an expression

tgingold · 2016-03-10T06:47:33Z

Being able to reference endpoints in VHDL is indeed a powerful feature.
I am currently reading 1850-2010 to understand the enhancements since PSL v1.1

Do you need support for PSL functions ?

tmeissner · 2016-03-10T09:52:43Z

PSL functions would be a nice addition to GHDL, but they aren't a blocker at the moment. If you consider to implement PSL functions, the ended() function would be the standard way when evaluating PSL events in VHDL.

Regarding PSL 2010: the main addition I know is local variables in properties. The syntax is crude imho, but they make possible to write more readable properties where you needed property replication before. Modelsim/Questa don't supports this, my support case was answered as "we don't plan to support PSL 2010 standard", which is annoying. They don't support standards which were codefined by their own Chief Verification Scientist :(

Another question: is there a data structure in GHDL which accumulates how often PSL assertion and cover directives when triggered? I've looked into the code regarding PSL, but I don't really understand it works without knowledge of the internal structure of GHDL ;)

tgingold · 2016-03-11T06:58:19Z

On 10/03/16 10:52, T. Meissner wrote:

PSL functions would be a nice addition to GHDL, but they aren't a
blocker at the moment. If you consider to implement PSL functions, the
ended() function would be the standard way when evaluating PSL events in
VHDL.

My understanding is that ended() is only available within PSL expressions.

Regarding PSL 2010: the main addition I know is local variables in
properties I think. The syntax is crude imho, but they make possible to
write more readable properties where you needed property replication before.

Yes, but that's not easy to implement :-(

Another question: is there a data structure in GHDL which accumulates
how often PSL assertion and cover directives were triggered? I've looked
into the code regarding PSL, but I don't really understand it works
without knowledge of the internal structure of GHDL ;)

No, but that's much easier to implement.

Tristan.

tmeissner · 2016-03-11T09:23:34Z

My understanding is that ended() is only available within PSL expressions.

Maybe this isn't described in the PSL standard. It is also not mentioned in the book "Practical Introduction to PSL". They only claim, that ended() is a boolean which is true in the last cycle of a triggered sequence.

Modelsim/Questa supports evaluating ended() in HDL. The syntax is similar to evaluating endpoints in VHDL like this:

-- psl sequence s_test is {req; not(grant); grant}@rising_edge(clk);

process is
begin
  wait until ended(s_test);
  report "s_test hit";
  wait;
end process;

I've tried a similar example with Riviera 2015.01 on edaplayground (http://www.edaplayground.com/x/3sjM), but it don't work. So, is it a Mentor extension? I don't believe that, but I'm not sure. There are some articles on the web, that describe that behaviour, most with endpoints, but the behaviour should be the same.

Regarding the PSL data structure: It's content could be similar to other simulators. They store the assertion/cover name, counts of passes and failures, the type of assertion/cover (psl/vhdl) and in which design unit they are. Something like this (I use strings for fields which would printed as strings in a report):

type CoverageLog is record
    Name    : string;
    Passes  : natural;
    Fails   : natural;
    Type    : string;
    Unit    : string;
end record;

This could be used to export a coverage report in plain text and xml (which would be good for further processing by tools).

tgingold · 2016-03-18T19:01:55Z

On 10/03/16 10:52, T. Meissner wrote:

PSL functions would be a nice addition to GHDL, but they aren't a
blocker at the moment. If you consider to implement PSL functions, the
ended() function would be the standard way when evaluating PSL events in
VHDL.

Regarding PSL 2010: the main addition I know is local variables in
properties I think. The syntax is crude imho, but they make possible to
write more readable properties where you needed property replication before.

Another question: is there a data structure in GHDL which accumulates
how often PSL assertion and cover directives were triggered? I've looked
into the code regarding PSL, but I don't really understand it works
without knowledge of the internal structure of GHDL ;)

This latter is now implemented. I have posted this message to
sourceforge ticket 24:

this enhancement is now implemented. A new option,
--psl-report=FILENAME write a JSON report to FILENAME.

Feedback is welcome.

Now I will investigate endpoints.

Tristan.

tmeissner · 2016-03-18T19:12:27Z

Oh, cool. I'm at the linux days in Chemnitz this weekend, i think I will have time to test it between the lectures. Thanks 👍

Regarding endpoints/ended() in VHDL: I think now, they are valid in the modeling layer of PSL. So, in a PSL vunit, they should be valid in the selected HDL flavor. The evaluation of endpoints/ended() in normal VHDL architectures is a Mentor extension maybe.

tgingold · 2016-03-18T20:23:00Z

On 18/03/16 20:12, T. Meissner wrote:

Oh, cool. I'm at the linux days in Chemnitz this weekend, i think I will
have time to test it between the lectures. Thanks 👍

Have fun!

Regarding endpoints/ended() in VHDL: I think now, they are valid in the
modeling layer of PSL. So, in a PSL vunit, they should be valid in the
selected HDL flavor. The evaluation of endpoints/ended() in normal VHDL
architectures is a Mentor extension maybe.

Possibly. But this is unambiguous and powerful.

tmeissner · 2016-03-18T20:31:48Z

Mhm, I get no report file. What I'm doing wrong?

$ ghdl -a -fpsl --std=08 psl_test_endpoint.vhd 
$ ghdl -e -fpsl --std=08 psl_test_endpoint
$ ./psl_test_endpoint --psl-report=psl_report.json
psl_test_endpoint.vhd:31:5:@0ms:(report note): RUNNING psl_test_endpoint test case
psl_test_endpoint.vhd:32:5:@0ms:(report note): ==========================================
psl_test_endpoint.vhd:64:10:@30ns:(psl assertion error): ENDPOINT ASSERT
psl_test_endpoint.vhd:64:10:@50ns:(psl assertion error): ENDPOINT ASSERT
psl_test_endpoint.vhd:64:10:@70ns:(psl assertion error): ENDPOINT ASSERT
psl_test_endpoint.vhd:64:10:@90ns:(psl assertion error): ENDPOINT ASSERT
psl_test_endpoint.vhd:64:10:@110ns:(psl assertion error): ENDPOINT ASSERT
psl_test_endpoint.vhd:67:10:@130ns:(psl cover note): COVERED2
psl_test_endpoint.vhd:65:10:@130ns:(psl cover note): COVERED0
psl_test_endpoint.vhd:64:10:@130ns:(psl assertion error): ENDPOINT ASSERT
psl_test_endpoint.vhd:64:10:@150ns:(psl assertion error): ENDPOINT ASSERT
simulation stopped @170ns with status 0

The simulation worked, but no psl_report.json file was written.

tmeissner · 2016-03-18T21:33:13Z

Mhm, testcase for ticket24 works as expected. But it uses elab-run as option. And, it doesn't work anymore, if -std=08 is added in analysing. Then elab-run gives an error:

$ ghdl -a --std=08 -fpsl psl.vhdl
$ ghdl --elab-run -fpsl psl --psl-report=psl.out
/usr/local/bin/ghdl1-llvm: cannot find entity or configuration psl
ghdl: compilation error

I always use --std=08 in my testbenches because of OSVVM. If I use -a and -e to analyse/elaborate, ticket24 works with --std=08:

$ ghdl -a --std=08 -fpsl psl.vhdl
$ ghdl -e --std=08 -fpsl psl
$ ./psl --psl-report=psl.out 
psl.vhdl:29:10:@5ns:(psl cover note): sequence covered
psl.vhdl:29:10:@11ns:(psl cover note): sequence covered
psl.vhdl:29:10:@15ns:(psl cover note): sequence covered
$ ls -l psl.out
-rw-r--r--  1 torsten  staff  549 18 Mär 22:40 psl.out

If I use the same commands for my test design, I don' get the psl export file. strange :o

tmeissner · 2016-03-18T22:28:29Z

My testcase for the psl-report, which doesn't produce psl-export file:

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

library std;
use std.env.all;


entity psl_test_endpoint is
end entity psl_test_endpoint;


architecture test of psl_test_endpoint is


  signal s_rst_n : std_logic := '0';
  signal s_clk   : std_logic := '0';
  signal s_write : std_logic;
  signal s_read  : std_logic;


begin


  s_rst_n <= '1' after 100 ns;
  s_clk   <= not s_clk after 10 ns;


  TestP : process is
  begin
    report "RUNNING psl_test_endpoint test case";
    report "==========================================";
    s_write <= '0';  -- named assertion should hit
    s_read  <= '0';
    wait until s_rst_n = '1' and rising_edge(s_clk);
    s_write <= '1';
    wait until rising_edge(s_clk);
    s_read  <= '1';  -- assertion should hit
    wait until rising_edge(s_clk);
    s_write <= '0';
    s_read  <= '0';
    wait until rising_edge(s_clk);
    stop(0);
  end process TestP;


  -- psl default clock is rising_edge(s_clk);
  -- psl endpoint E_TEST is {not(s_write); s_write};
  -- psl sequence abc_seq is {not(s_write); s_write};

  -- psl ENDPOINT_ASSERT : assert always {E_TEST; s_read} report  "ENDPOINT ASSERT";
  -- psl COVERAGE0 : cover {not(s_write); s_write} report "COVERED0";
  -- psl COVERAGE1 : cover {abc_seq} report "COVERED1";
  -- psl COVERAGE2 : cover {E_TEST} report "COVERED2";


end architecture test;

tgingold · 2016-03-19T06:00:58Z

On 18/03/16 21:31, T. Meissner wrote:

Mhm, I get no report file. What I'm doing wrong?

Nothing, but you are stopping simulation with std.env.stop
I will fix.

Tristan.

tgingold · 2016-03-19T06:05:48Z

On 18/03/16 23:28, T. Meissner wrote:

My testcase for the psl-report, which doesn't produce psl-export file:

Thanks. It now works on my setup, I will commit the fix soon.

Tristan.

tmeissner · 2016-03-19T10:27:51Z

Yep, after I removed the stop()statement, the report is generated. Looks good, great 👍

{ "details" : [
 { "directive": "assertion",
   "name": ".psl_test_endpoint(test).endpoint_assert",
   "file": "psl_test_endpoint.vhd",
   "line": 52,
   "count": 1,
   "status": "failed"},
 { "directive": "cover",
   "name": ".psl_test_endpoint(test).coverage0",
   "file": "psl_test_endpoint.vhd",
   "line": 53,
   "count": 1,
   "status": "covered"},
 { "directive": "cover",
   "name": ".psl_test_endpoint(test).coverage1",
   "file": "psl_test_endpoint.vhd",
   "line": 54,
   "count": 1,
   "status": "covered"},
 { "directive": "cover",
   "name": ".psl_test_endpoint(test).coverage2",
   "file": "psl_test_endpoint.vhd",
   "line": 55,
   "count": 1,
   "status": "covered"}],
 "summary" : {
  "assert": 1,
  "assert-failure": 1,
  "assert-pass": 0,
  "cover": 3,
  "cover-failure": 0,
  "cover-pass": 3}
}

What I would like to add is pass counts not only for the summary, but also for each assert detail. So I can see if a assert was passed, when not, I have a coverage hole in my test case. It could look like this:

{ "details" : [
 { "directive": "assertion",
   "name": ".psl_test_endpoint(test).endpoint_assert",
   "file": "psl_test_endpoint.vhd",
   "line": 52,
   "count-pass": 0,
   "count-failure": 1,
   "status": "failed"},

tgingold · 2016-03-19T20:14:11Z

On 19/03/16 11:27, T. Meissner wrote:

Yep, after I removed the |stop()|statement, the report is generated.
Looks good, great 👍

Thanks!

[...]

What I would like to add is pass counts not only for the summary, but
also for each assert/cover detail.So, I can see if a assert was passed,
when not, I have a coverage hole in my test case. It could look like this:

{"details" : [
{"directive":"assertion",
"name":".psl_test_endpoint(test).endpoint_assert",
"file":"psl_test_endpoint.vhd",
"line":52,
"count-pass":0,
"count-failure":1,
"status":"failed"},

Unfortunately, the state machine only detects failure, not success.
I will investigate, but after endpoints.

tgingold · 2016-03-20T15:12:48Z

On 18/03/16 23:28, T. Meissner wrote:

My testcase for the psl-report, which doesn't produce psl-export file:

This is now fixed.

Thanks!
Tristan.

tmeissner · 2016-03-22T13:34:25Z

It works. Thanks. BTW: I have a new repository where I collect all my test cases: https://github.com/tmeissner/vhdl_verification

tgingold · 2016-03-22T20:09:37Z

On 22/03/16 14:34, T. Meissner wrote:

It works. Thanks. BTW: I have a new repository where I collect all my
test cases: https://github.com/tmeissner/vhdl_verification

Ok, I will bookmark it.

I have just pushed the enhancement for endpoints: it is now possible
to refer to an endpoint in vhdl code.

Tristan.

tmeissner · 2016-03-22T21:03:03Z

Thanks 👍

For my test test extended by a VHDL process reading the endpoint:
https://github.com/tmeissner/vhdl_verification/blob/master/psl_endpoint_eval_in_vhdl/psl_endpoint_eval_in_vhdl.vhd)
I get following error:

$ make compile
Analyse & elaborate test ...
cd work; ghdl -a --std=08 -fpsl ../psl_endpoint_eval_in_vhdl.vhd
Assertion failed: ((i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && "Calling a function with a bad signature!"), function init, file Instructions.cpp, line 281.

Execution terminated by unhandled exception
Exception name: PROGRAM_ERROR
Message: unhandled signal
Load address: 0x10b306000
Call stack traceback locations:
0x10bc9ad27 0x7fff9653fea8
ghdl: compilation error
make: *** [compile] Error 1

tgingold · 2016-03-23T04:27:05Z

On 22/03/16 22:03, T. Meissner wrote:

Thanks 👍

For my test test extended by a VHDL process reading the endpoint:
https://github.com/tmeissner/vhdl_verification/blob/master/psl_endpoint_eval_in_vhdl/psl_endpoint_eval_in_vhdl.vhd)
I get following error:

I am fixing the crash, but your code should be: wait until E_TEST0;

Tristan.

tmeissner · 2016-03-23T10:41:00Z

Yep, my fault. It works now, thanks :)

Masshat · 2016-09-26T18:17:31Z

Hi Guys, with the last version of GHDL 0.34Dev, i have this error when compiling some code of @tmeissner : https://github.com/tmeissner/vhdl_verification/tree/master/osvvm_fsm_coverage

ghdl:warning: library std does not exists for v08
ghdl:warning: library ieee does not exists for v08
/usr/lib/gcc/x86_64-unknown-linux-gnu/4.9.3/ghdl1: cannot find "std" library
ghdl: compilation error

according to @tmeissner there is no error in his side, here is also the PKGBUILD Used to build ghdl: https://aur.archlinux.org/packages/ghdl-gcc-git/

@tgingold Do you have some idea tohow to debug this issue?
Thanks in advance.

tgingold · 2016-09-26T18:23:15Z

On 26/09/16 20:17, Massine wrote:

Hi Guys, with the last version of GHDL 0.34Dev, i have this error when
compiling some code of @tmeissner https://github.com/tmeissner :
https://github.com/tmeissner/vhdl_verification/tree/master/osvvm_fsm_coverage

ghdl⚠️ library std does not exists for v08
ghdl⚠️ library ieee does not exists for v08
/usr/lib/gcc/x86_64-unknown-linux-gnu/4.9.3/ghdl1: cannot find "std" library
ghdl: compilation error

according to @tmeissner https://github.com/tmeissner there is no error
in his side, here is also the PKGBUILD Used to build ghdl:
https://aur.archlinux.org/packages/ghdl-gcc-git/

@tgingold https://github.com/tgingold Do you have some idea tohow to
debug this issue?

Looks like the archlinux package is not complete: vhdl 2008 libraries
are missing, or the installation is not correct.

You can try to use the latest beta from github.

Tristan.

Masshat · 2016-09-26T19:20:05Z

OK @tgingold I will try this and keep you informed.

Can you tell me if possible when you will release the new version with PSL support? it would be good if you can Tag this version.

tgingold added the Enhancement label Mar 10, 2016

tgingold closed this as completed Mar 23, 2016

tmeissner mentioned this issue Sep 25, 2018

Support of PSL functions #662

Open

9 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support to evaluate PSL endpoints in VHDL code #45

Support to evaluate PSL endpoints in VHDL code #45

tmeissner commented Mar 8, 2016

tmeissner commented Mar 8, 2016

tgingold commented Mar 10, 2016

tmeissner commented Mar 10, 2016

tgingold commented Mar 11, 2016

tmeissner commented Mar 11, 2016

tgingold commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tgingold commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tgingold commented Mar 19, 2016

tgingold commented Mar 19, 2016

tmeissner commented Mar 19, 2016

tgingold commented Mar 19, 2016

tgingold commented Mar 20, 2016

tmeissner commented Mar 22, 2016

tgingold commented Mar 22, 2016

tmeissner commented Mar 22, 2016

tgingold commented Mar 23, 2016

tmeissner commented Mar 23, 2016

Masshat commented Sep 26, 2016

tgingold commented Sep 26, 2016

Masshat commented Sep 26, 2016 •

edited

Loading

Support to evaluate PSL endpoints in VHDL code #45

Support to evaluate PSL endpoints in VHDL code #45

Comments

tmeissner commented Mar 8, 2016

tmeissner commented Mar 8, 2016

tgingold commented Mar 10, 2016

tmeissner commented Mar 10, 2016

tgingold commented Mar 11, 2016

tmeissner commented Mar 11, 2016

tgingold commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tgingold commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tmeissner commented Mar 18, 2016

tgingold commented Mar 19, 2016

tgingold commented Mar 19, 2016

tmeissner commented Mar 19, 2016

tgingold commented Mar 19, 2016

tgingold commented Mar 20, 2016

tmeissner commented Mar 22, 2016

tgingold commented Mar 22, 2016

tmeissner commented Mar 22, 2016

tgingold commented Mar 23, 2016

tmeissner commented Mar 23, 2016

Masshat commented Sep 26, 2016

tgingold commented Sep 26, 2016

Masshat commented Sep 26, 2016 • edited Loading

Masshat commented Sep 26, 2016 •

edited

Loading