From cbd80e413cd95dcc2067020c71826b7bf8d0d2ca Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sat, 6 Jun 2020 12:09:12 +0200 Subject: [PATCH] Add stable() example to formal tests after it was implemented by ghdl/ghdl#1353 --- formal/tests.mk | 3 ++- src/psl_stable.vhd | 6 +++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/formal/tests.mk b/formal/tests.mk index e6a363a..e500c9a 100644 --- a/formal/tests.mk +++ b/formal/tests.mk @@ -26,4 +26,5 @@ psl_sere_len_matching_and \ psl_sere_non_len_matching_and \ psl_sere_concat \ psl_sere_fusion \ -psl_prev +psl_prev \ +psl_stable diff --git a/src/psl_stable.vhd b/src/psl_stable.vhd index f0d6995..d5f918c 100644 --- a/src/psl_stable.vhd +++ b/src/psl_stable.vhd @@ -30,12 +30,12 @@ begin default clock is rising_edge(clk); -- This assertion holds - STABLE_0_a : assert always {not valid; valid} -> next (stable(a) until_ ack); + STABLE_0_a : assert always {not valid; valid} |=> (stable(a) until_ ack); -- This assertion holds - STABLE_1_a : assert always {not valid; valid} -> next (stable(b) until_ ack); + STABLE_1_a : assert always {not valid; valid} |=> (stable(b) until_ ack); - -- Workaround needed before stable() is implemented + -- Workaround needed before stable() was implemented -- With VHDL glue logic generating the -- previous value of a and simple comparing the two values a_reg : block is