Browse Source

Add stable() example to formal tests after it was implemented by ghdl/ghdl#1353

master
T. Meissner 5 years ago
parent
commit
cbd80e413c
2 changed files with 5 additions and 4 deletions
  1. +2
    -1
      formal/tests.mk
  2. +3
    -3
      src/psl_stable.vhd

+ 2
- 1
formal/tests.mk View File

@ -26,4 +26,5 @@ psl_sere_len_matching_and \
psl_sere_non_len_matching_and \ psl_sere_non_len_matching_and \
psl_sere_concat \ psl_sere_concat \
psl_sere_fusion \ psl_sere_fusion \
psl_prev
psl_prev \
psl_stable

+ 3
- 3
src/psl_stable.vhd View File

@ -30,12 +30,12 @@ begin
default clock is rising_edge(clk); default clock is rising_edge(clk);
-- This assertion holds -- 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 -- 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 -- With VHDL glue logic generating the
-- previous value of a and simple comparing the two values -- previous value of a and simple comparing the two values
a_reg : block is a_reg : block is


Loading…
Cancel
Save