Browse Source

Add testcase for evaluating PSL endpoints in VHDL code

master
T. Meissner 9 years ago
parent
commit
ad80c4c082
2 changed files with 95 additions and 0 deletions
  1. +33
    -0
      psl_endpoint_eval_in_vhdl/Makefile
  2. +62
    -0
      psl_endpoint_eval_in_vhdl/psl_endpoint_eval_in_vhdl.vhd

+ 33
- 0
psl_endpoint_eval_in_vhdl/Makefile View File

@ -0,0 +1,33 @@
.PHONY: sim compile clean wave
sim \
work/psl_endpoint_eval_in_vhdl \
work/psl_endpoint_eval_in_vhdl.ghw: work/psl_endpoint_eval_in_vhdl.o log
@echo Run test ...
@cd work; ghdl -r --std=08 -fpsl psl_endpoint_eval_in_vhdl \
--psl-report=../log/psl_endpoint_eval_in_vhdl.json \
--wave=../log/psl_endpoint_eval_in_vhdl.ghw \
--stop-time=200ns
compile \
work/psl_endpoint_eval_in_vhdl.o: psl_endpoint_eval_in_vhdl.vhd work
@echo "Analyse & elaborate test ..."
cd work; ghdl -a --std=08 -fpsl ../psl_endpoint_eval_in_vhdl.vhd
cd work; ghdl -e --std=08 -fpsl psl_endpoint_eval_in_vhdl >& /dev/null
wave: work/psl_endpoint_eval_in_vhdl.ghw
@echo Run waveform viewer ...
@gtkwave log/psl_endpoint_eval_in_vhdl.ghw -S psl_endpoint_eval_in_vhdl.tcl &
work \
log:
mkdir $@
clean:
@echo Remove generated files ...
@rm -rf work log

+ 62
- 0
psl_endpoint_eval_in_vhdl/psl_endpoint_eval_in_vhdl.vhd View File

@ -0,0 +1,62 @@
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
library std;
use std.env.all;
entity psl_endpoint_eval_in_vhdl is
end entity psl_endpoint_eval_in_vhdl;
architecture test of psl_endpoint_eval_in_vhdl 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_endpoint_eval_in_vhdl 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);
wait;
end process TestP;
-- psl default clock is rising_edge(s_clk);
-- psl endpoint E_TEST0 is {not(s_write); s_write};
process is
begin
wait for E_TEST0;
report "HIT";
wait;
end process;
end architecture test;

Loading…
Cancel
Save