From 09fab71a5091da87586d27b1fb203aa84fc756ef Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sat, 13 Jun 2020 13:41:19 +0200 Subject: [PATCH] Update prev() & stable() examples after ghdl/ghdl#1366 & ghdl/ghdl#1367 were fixed --- issues/issue_1366.vhd | 14 +++++++++----- issues/issue_1367.vhd | 35 +++++++++++++++++++++++++++-------- issues/tests.mk | 4 +++- src/psl_prev.vhd | 4 ++++ src/psl_stable.vhd | 6 +++++- 5 files changed, 48 insertions(+), 15 deletions(-) diff --git a/issues/issue_1366.vhd b/issues/issue_1366.vhd index 14e315a..40f7de2 100644 --- a/issues/issue_1366.vhd +++ b/issues/issue_1366.vhd @@ -1,29 +1,33 @@ vunit issue_vunit (issue(psl)) { - + -- VHDL declaration seem to be working - signal a_delayed : std_logic := '0'; + signal a_delayed : std_logic := '0'; + signal prev_valid : boolean := false; -- Other VHDL code not -- results in parser errors -- during synthesis + -- EDIT: works since fix of ghdl issue #1366 process is begin wait until rising_edge(clk); a_delayed <= a; - end process; + prev_valid <= true; + end process; -- All is sensitive to rising edge of clk default clock is rising_edge(clk); -- This assertion holds - CHECK_a : assert always (a -> b); + CHECK_0_a : assert always (a -> b); -- You can't do anything with the declared signal -- Can be synthesized with GHDL, however -- results in error in ghdl-yosys-plugin: -- ERROR: Assert `n.id != 0' failed in src/ghdl.cc:172 - assert always a_delayed = prev(a); + -- EDIT: works since fix of ghdl issue #1366 + CHECK_1_a : assert always prev_valid -> a_delayed = prev(a); } diff --git a/issues/issue_1367.vhd b/issues/issue_1367.vhd index 6888d3f..f6b5539 100644 --- a/issues/issue_1367.vhd +++ b/issues/issue_1367.vhd @@ -83,10 +83,17 @@ architecture psl of issue is end component hex_sequencer; signal a, b : std_logic_vector(3 downto 0); + signal prev_valid : boolean := false; begin + process is + begin + wait until rising_edge(clk); + prev_valid <= true; + end process; + -- 0123456789 SEQ_A : hex_sequencer generic map ("4444444444") port map (clk, a); SEQ_B : hex_sequencer generic map ("4444544444") port map (clk, b); @@ -96,24 +103,36 @@ begin default clock is rising_edge(clk); -- Holds - STABLE_0 : assert always stable(a); + STABLE_0 : assert always prev_valid -> stable(a); -- Doesn't hold at cycle 4 - STABLE_1 : assert always stable(b); + STABLE_1 : assert always prev_valid -> stable(b); -- Triggers GHDL bug - STABLE_2 : assert always stable(a(1 downto 0)); - STABLE_3 : assert always stable(b(1 downto 0)); + -- EDIT: works since fix of ghdl issue #1367 + -- Holds + STABLE_2 : assert always prev_valid -> stable(a(1 downto 0)); + + -- Triggers GHDL bug + -- EDIT: works since fix of ghdl issue #1367 + -- Doesn't hold at cycle 4 + STABLE_3 : assert always prev_valid -> stable(b(1 downto 0)); -- Holds - PREV_0 : assert always a = prev(a); + PREV_0 : assert always prev_valid -> a = prev(a); -- Doesn't hold at cycle 4 - PREV_1 : assert always b = prev(b); + PREV_1 : assert always prev_valid -> b = prev(b); -- Triggers GHDL bug - PREV_2 : assert always always a(1 downto 0) = prev(a(1 downto 0)); - PREV_3 : assert always always b(1 downto 0) = prev(b(1 downto 0)); + -- EDIT: works since fix of ghdl issue #1367 + -- Holds + PREV_2 : assert always always prev_valid -> a(1 downto 0) = prev(a(1 downto 0)); + + -- Triggers GHDL bug + -- EDIT: works since fix of ghdl issue #1367 + -- Doesn't hold at cycle 4 + PREV_3 : assert always always prev_valid -> b(1 downto 0) = prev(b(1 downto 0)); end architecture psl; diff --git a/issues/tests.mk b/issues/tests.mk index 7be1b71..00399bb 100644 --- a/issues/tests.mk +++ b/issues/tests.mk @@ -4,4 +4,6 @@ issue_1292 \ issue_1314 \ issue_1321 \ issue_1322 \ -issue_1345 +issue_1345 \ +issue_1366 \ +issue_1367 diff --git a/src/psl_prev.vhd b/src/psl_prev.vhd index 6106938..09bcb5c 100644 --- a/src/psl_prev.vhd +++ b/src/psl_prev.vhd @@ -76,6 +76,10 @@ begin -- This assertion holds PREV_6_a : assert always ((cnt /= x"F") -> next (unsigned(cnt) = unsigned(prev(cnt)) + 1)); + -- Check parts of a vector + -- This assertion should hold + PREV_7_a : assert always (valid -> di(1 downto 0) = prev(di(1 downto 0))); + -- Stop simulation after longest running sequencer is finished -- Simulation only code by using pragmas -- synthesis translate_off diff --git a/src/psl_stable.vhd b/src/psl_stable.vhd index d5f918c..934efa6 100644 --- a/src/psl_stable.vhd +++ b/src/psl_stable.vhd @@ -33,7 +33,7 @@ begin STABLE_0_a : assert always {not valid; valid} |=> (stable(a) until_ ack); -- This assertion holds - STABLE_1_a : assert always {not valid; valid} |=> (stable(b) until_ ack); + STABLE_1_a : assert always rose(valid) -> next (stable(b) until_ ack); -- Workaround needed before stable() was implemented -- With VHDL glue logic generating the @@ -53,6 +53,10 @@ begin STABLE_3_a : assert always {not valid; valid} |=> (b = b_prev until_ ack); end block a_reg; + -- Check parts of a vector + -- This assertion holds + STABLE_4_a : assert always rose(valid) -> next (stable(b(1 downto 0)) until_ ack); + -- Stop simulation after longest running sequencer is finished -- Simulation only code by using pragmas