diff --git a/README.md b/README.md index 033fa79..ad75e66 100644 --- a/README.md +++ b/README.md @@ -48,6 +48,7 @@ The next lists will grow during further development * Simple SERE * Overlapping suffix implication operator (|->) * Non overlapping suffix implication operator (|=>) +* Consecutive repetition operator ([*], [+], [*n], [*i to j]) ## PSL features not yet supported by GHDL: diff --git a/formal/psl_sere_consecutive_repetition.sby b/formal/psl_sere_consecutive_repetition.sby new file mode 100644 index 0000000..574fd8d --- /dev/null +++ b/formal/psl_sere_consecutive_repetition.sby @@ -0,0 +1,18 @@ +[tasks] +bmc + +[options] +depth 25 +bmc: mode bmc + +[engines] +bmc: smtbmc z3 + +[script] +bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_sere_consecutive_repetition.vhd -e psl_sere_consecutive_repetition +prep -top psl_sere_consecutive_repetition + +[files] +../src/pkg.vhd +../src/sequencer.vhd +../src/psl_sere_consecutive_repetition.vhd diff --git a/formal/tests.mk b/formal/tests.mk index 9b63294..b197819 100644 --- a/formal/tests.mk +++ b/formal/tests.mk @@ -15,4 +15,5 @@ psl_before \ psl_eventually \ psl_sere \ psl_sere_overlapping_suffix_impl \ -psl_sere_non_overlapping_suffix_impl +psl_sere_non_overlapping_suffix_impl \ +psl_sere_consecutive_repetition diff --git a/src/psl_sere_consecutive_repetition.vhd b/src/psl_sere_consecutive_repetition.vhd new file mode 100644 index 0000000..b455175 --- /dev/null +++ b/src/psl_sere_consecutive_repetition.vhd @@ -0,0 +1,46 @@ +library ieee; + use ieee.std_logic_1164.all; + +use work.pkg.all; + + +entity psl_sere_consecutive_repetition is + port ( + clk : in std_logic + ); +end entity psl_sere_consecutive_repetition; + + +architecture psl of psl_sere_consecutive_repetition is + + signal a, b, c : std_logic; + +begin + + + -- 012345678 + SEQ_A : sequencer generic map ("_-_______") port map (clk, a); + SEQ_B : sequencer generic map ("__----___") port map (clk, b); + SEQ_C : sequencer generic map ("______-__") port map (clk, c); + + + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + + -- This assertion holds + SERE_0_a : assert always {a} |=> {b; b; b; b; c}; + + -- This assertion holds + SERE_1_a : assert always {a} |=> {b[*4]; c}; + + -- This assertion holds + SERE_2_a : assert always {a} |=> {b[*3 to 5]; c}; + + -- This assertion holds + SERE_3_a : assert always {a} |=> {b[*]; c}; + + -- This assertion holds + SERE_4_a : assert always {a} |=> {b[+]; c}; + + +end architecture psl;