From 9437d2d27219661803cae0c976d705fe69980cee Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sat, 9 May 2020 22:01:38 +0200 Subject: [PATCH] Add more failing assertions (should hold, assuming GHDL bug) to next_event_a example --- formal/tests.mk | 1 + src/psl_next_event_a.vhd | 43 ++++++++++++++-------------------------- 2 files changed, 16 insertions(+), 28 deletions(-) diff --git a/formal/tests.mk b/formal/tests.mk index d646d58..55b44ec 100644 --- a/formal/tests.mk +++ b/formal/tests.mk @@ -8,6 +8,7 @@ psl_next_e \ psl_next_event \ psl_next_event_4 \ psl_next_event_e \ +psl_next_event_a \ psl_until \ psl_before \ psl_eventually diff --git a/src/psl_next_event_a.vhd b/src/psl_next_event_a.vhd index 01a7ee0..79b31d5 100644 --- a/src/psl_next_event_a.vhd +++ b/src/psl_next_event_a.vhd @@ -1,6 +1,7 @@ library ieee; use ieee.std_logic_1164.all; use ieee.numeric_std.all; + use ieee.math_real.all; use work.pkg.all; @@ -20,10 +21,10 @@ architecture psl of psl_next_event_a is begin - -- 012345678901234567890 - SEQ_A : sequencer generic map ("_-______________-____") port map (clk, a); - SEQ_B : hex_sequencer generic map ("443334477444433355555") port map (clk, b); - SEQ_C : sequencer generic map ("_____-___---_____----") port map (clk, c); + -- 012345678901234567890123 + SEQ_A : sequencer generic map ("_-______________-_______") port map (clk, a); + SEQ_B : hex_sequencer generic map ("443334477444433355554555") port map (clk, b); + SEQ_C : sequencer generic map ("_____-___---______--_--_") port map (clk, c); @@ -31,40 +32,26 @@ begin default clock is rising_edge(clk); -- Check for one possible value of b - -- This assertion holds - NEXT_EVENT_a : assert always ((a and b = x"4") -> next_event_a(c)[1 to 4](b = x"4")); + -- Both assertions should hold + -- Assertions don't hold, assuming GHDL bug + NEXT_EVENT_0_a : assert always ((a and b = x"4") -> next_event_a(c)[1 to 4](b = x"4")); + NEXT_EVENT_1_a : assert always ((a and b = x"5") -> next_event_a(c)[1 to 4](b = x"5")); + -- Check for all possible values of b -- Workaround for missing PSL forall in {i to j} statement - -- This assertion holds - check_b : for i in 0 to 0 generate + -- This assertions should hold + -- Assertions for i = 4 & i = 5 don't hold, assuming GHDL bug + check_b : for i in 0 to 2**b'length-1 generate signal i_slv : std_logic_vector(b'range); begin i_slv <= std_logic_vector(to_unsigned(i, 4)); - --Without name it works + -- Without name it works assert always ((a and b = i_slv) -> next_event_a(c)[1 to 4](b = i_slv)); -- This errors because of similar names for all asserts -- ERROR: Assert `count_id(cell->name) == 0' failed in kernel/rtlil.cc:1613. - -- NEXT_EVENT_a : assert always ((a and b = i_slv) -> next_event_a(c)[1](b = i_slv)); + -- NEXT_EVENT_a : assert always ((a and b = i_slv) -> next_event_a(c)[1 to 4](b = i_slv)); end generate check_b; - -- psl.sem_property: cannot handle N_NEXT_EVENT_A - -- - -- ******************** GHDL Bug occurred *************************** - -- Please report this bug on https://github.com/ghdl/ghdl/issues - -- GHDL release: 1.0-dev (tarball) [Dunoon edition] - -- Compiled with GNAT Version: 8.3.0 - -- Target: x86_64-linux-gnu - -- /build/src/ - -- Command line: - -- ghdl --synth --std=08 pkg.vhd sequencer.vhd hex_sequencer.vhd psl_next_event_a.vhd -e psl_next_event_a - -- Exception TYPES.INTERNAL_ERROR raised - -- Exception information: - -- raised TYPES.INTERNAL_ERROR : psl-errors.adb:39 - -- Call stack traceback locations: - -- 0x556095397b3a 0x5560954bbbb7 0x5560954bb8f1 0x5560954bb69f 0x5560954bb765 0x5560954bc557 0x5560954c2fd7 0x5560954c30de 0x5560954c3235 0x5560954fb17d 0x556095501e72 0x5560954b99c2 0x5560954ba814 0x5560954ba9bc 0x5560955621c6 0x5560955a0ab9 0x5560955a1361 0x5560954b136f 0x5560955aacaf 0x556095363fa3 0x7f72faa58099 0x556095362df8 0xfffffffffffffffe - -- ****************************************************************** - - end architecture psl;