diff options
author | Tristan Gingold <tgingold@free.fr> | 2016-03-18 05:26:29 +0100 |
---|---|---|
committer | Tristan Gingold <tgingold@free.fr> | 2016-03-18 05:26:29 +0100 |
commit | f5d6578a062f1af9c3508ed26b0f7edff04b1a01 (patch) | |
tree | 44e86f3ca64f25f0c59cc5ff5a7488673fbba631 /testsuite | |
parent | 1c8872240feffcc2324a1b46a055d5afcfa3e2bb (diff) | |
download | ghdl-f5d6578a062f1af9c3508ed26b0f7edff04b1a01.tar.gz ghdl-f5d6578a062f1af9c3508ed26b0f7edff04b1a01.tar.bz2 ghdl-f5d6578a062f1af9c3508ed26b0f7edff04b1a01.zip |
Add testcase for ticket24
Diffstat (limited to 'testsuite')
-rw-r--r-- | testsuite/gna/ticket24/psl.ref | 27 | ||||
-rw-r--r-- | testsuite/gna/ticket24/psl.vhdl | 30 | ||||
-rwxr-xr-x | testsuite/gna/ticket24/testsuite.sh | 24 |
3 files changed, 81 insertions, 0 deletions
diff --git a/testsuite/gna/ticket24/psl.ref b/testsuite/gna/ticket24/psl.ref new file mode 100644 index 000000000..6a5588a3a --- /dev/null +++ b/testsuite/gna/ticket24/psl.ref @@ -0,0 +1,27 @@ +{ "details" : [ + { "directive": "assertion", + "name": ".psl(behav).a1", + "file": "psl.vhdl", + "line": 27, + "count": 0, + "status": "passed"}, + { "directive": "assertion", + "name": ".psl(behav).a2", + "file": "psl.vhdl", + "line": 28, + "count": 0, + "status": "passed"}, + { "directive": "cover", + "name": ".psl(behav).c1", + "file": "psl.vhdl", + "line": 29, + "count": 3, + "status": "covered"}], + "summary" : { + "assert": 2, + "assert-failure": 0, + "assert-pass": 2, + "cover": 1, + "cover-failure": 0, + "cover-pass": 1} +} diff --git a/testsuite/gna/ticket24/psl.vhdl b/testsuite/gna/ticket24/psl.vhdl new file mode 100644 index 000000000..a838b8fd2 --- /dev/null +++ b/testsuite/gna/ticket24/psl.vhdl @@ -0,0 +1,30 @@ +entity psl is +end; + +architecture behav of psl is + signal a, b, c : bit; + signal clk : bit; + subtype wf_type is bit_vector (0 to 7); + constant wave_a : wf_type := "10010100"; + constant wave_b : wf_type := "01001010"; + constant wave_c : wf_type := "00100101"; +begin + process + begin + for i in wf_type'range loop + clk <= '0'; + wait for 1 ns; + a <= wave_a (i); + b <= wave_b (i); + c <= wave_c (i); + clk <= '1'; + wait for 1 ns; + end loop; + wait; + end process; + + -- psl default clock is (clk'event and clk = '1'); + -- psl a1: assert always a |=> b; + -- psl a2: assert always a -> eventually! c; + -- psl c1: cover {a;b;c}; +end behav; diff --git a/testsuite/gna/ticket24/testsuite.sh b/testsuite/gna/ticket24/testsuite.sh new file mode 100755 index 000000000..96b37c948 --- /dev/null +++ b/testsuite/gna/ticket24/testsuite.sh @@ -0,0 +1,24 @@ +#! /bin/sh + +. ../../testenv.sh + +analyze -fpsl psl.vhdl +elab_simulate -fpsl psl --psl-report=psl.out + +if ! cmp psl.out psl.ref; then + echo "report mismatch" + exit 1 +fi + +# Usage example (python 2.7): +# +# import json +# d=json.load(open("psl.out")) +# print d['summary'] +# {u'assert-pass': 2, u'cover': 1, ... } +# print d['summary']['assert'] + +rm -f psl.out +clean + +echo "Test successful" |