From 333c6f8c16b9e6612d281226ccc821731f9b9709 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Tue, 19 Jan 2021 22:40:32 +0100 Subject: [PATCH] Add example for PSL endpoints (currently simulation only) --- sim/Makefile | 4 ++-- sim/tests.mk | 3 ++- src/psl_endpoint.vhd | 45 ++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 49 insertions(+), 3 deletions(-) create mode 100644 src/psl_endpoint.vhd diff --git a/sim/Makefile b/sim/Makefile index fdc4b29..188d556 100644 --- a/sim/Makefile +++ b/sim/Makefile @@ -11,9 +11,9 @@ all: ${psl_tests} %: ../src/%.vhd ../src/pkg.vhd ../src/sequencer.vhd ../src/hex_sequencer.vhd work/%/testbench.vhd ghdl -a --std=$(VHD_STD) --workdir=work/$@ ../src/pkg.vhd ../src/sequencer.vhd ../src/hex_sequencer.vhd - ghdl -a --std=$(VHD_STD) --workdir=work/$@ ../src/$@.vhd + ghdl -a --std=$(VHD_STD) -fpsl --workdir=work/$@ ../src/$@.vhd ghdl -a --std=$(VHD_STD) --workdir=work/$@ work/$@/testbench.vhd - ghdl -e --std=$(VHD_STD) --workdir=work/$@ -o work/$@/tb_$@ tb_$@ + ghdl -e --std=$(VHD_STD) -fpsl --workdir=work/$@ -o work/$@/tb_$@ tb_$@ cd work/$@; ghdl -r --std=$(VHD_STD) tb_$@ --wave=$@.ghw --psl-report=$@_psl_coverage.json work/%/testbench.vhd: template.vhd diff --git a/sim/tests.mk b/sim/tests.mk index 291c54d..e5d1467 100644 --- a/sim/tests.mk +++ b/sim/tests.mk @@ -27,4 +27,5 @@ psl_sere_non_len_matching_and \ psl_sere_concat \ psl_sere_fusion \ psl_sequence \ -psl_property +psl_property \ +psl_endpoint diff --git a/src/psl_endpoint.vhd b/src/psl_endpoint.vhd new file mode 100644 index 0000000..ab2e80f --- /dev/null +++ b/src/psl_endpoint.vhd @@ -0,0 +1,45 @@ +library ieee; + use ieee.std_logic_1164.all; + +use work.pkg.all; + + +entity psl_endpoint is + port ( + clk : in std_logic + ); +end entity psl_endpoint; + + +architecture psl of psl_endpoint is + + signal a, b : std_logic; + signal c, d : std_logic; + +begin + + + -- 01234567890123 + SEQ_A : sequencer generic map ("_-_____-______") port map (clk, a); + SEQ_B : sequencer generic map ("__--____---___") port map (clk, b); + SEQ_C : sequencer generic map ("____-______-__") port map (clk, c); + SEQ_D : sequencer generic map ("____________-_") port map (clk, d); + + + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + + -- only endpoint in psl comment works + -- psl endpoint ENDPOINT_1_e is {a; b[*3]; c}; + + -- This assertion holds + ASSERT_a : assert always (ENDPOINT_1_e <-> d); + + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 14); + -- synthesis translate_on + + +end architecture psl;