From b018d2e608a2c911686f02baf52748cd0413a3b8 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Wed, 3 Jun 2020 00:02:30 +0200 Subject: [PATCH] Add examples for currently unsupported rose(), fell() & stable() PSL functions --- formal/psl_fell.sby | 18 ++++++++++++ formal/psl_rose.sby | 18 ++++++++++++ formal/psl_stable.sby | 19 +++++++++++++ src/psl_fell.vhd | 57 ++++++++++++++++++++++++++++++++++++++ src/psl_rose.vhd | 57 ++++++++++++++++++++++++++++++++++++++ src/psl_stable.vhd | 64 +++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 233 insertions(+) create mode 100644 formal/psl_fell.sby create mode 100644 formal/psl_rose.sby create mode 100644 formal/psl_stable.sby create mode 100644 src/psl_fell.vhd create mode 100644 src/psl_rose.vhd create mode 100644 src/psl_stable.vhd diff --git a/formal/psl_fell.sby b/formal/psl_fell.sby new file mode 100644 index 0000000..a653479 --- /dev/null +++ b/formal/psl_fell.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_fell.vhd -e psl_fell +prep -top psl_fell + +[files] +../src/pkg.vhd +../src/sequencer.vhd +../src/psl_fell.vhd diff --git a/formal/psl_rose.sby b/formal/psl_rose.sby new file mode 100644 index 0000000..d3c5b2e --- /dev/null +++ b/formal/psl_rose.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_rose.vhd -e psl_rose +prep -top psl_rose + +[files] +../src/pkg.vhd +../src/sequencer.vhd +../src/psl_rose.vhd diff --git a/formal/psl_stable.sby b/formal/psl_stable.sby new file mode 100644 index 0000000..cf05a79 --- /dev/null +++ b/formal/psl_stable.sby @@ -0,0 +1,19 @@ +[tasks] +bmc + +[options] +depth 25 +bmc: mode bmc + +[engines] +bmc: smtbmc z3 + +[script] +bmc: ghdl --std=08 pkg.vhd sequencer.vhd hex_sequencer.vhd psl_stable.vhd -e psl_stable +prep -top psl_stable + +[files] +../src/pkg.vhd +../src/sequencer.vhd +../src/hex_sequencer.vhd +../src/psl_stable.vhd diff --git a/src/psl_fell.vhd b/src/psl_fell.vhd new file mode 100644 index 0000000..293a4ae --- /dev/null +++ b/src/psl_fell.vhd @@ -0,0 +1,57 @@ +library ieee; + use ieee.std_logic_1164.all; + +use work.pkg.all; + + +entity psl_fell is + port ( + clk : in std_logic + ); +end entity psl_fell; + + +architecture psl of psl_fell is + + signal a, b : std_logic; + +begin + + + -- 01234567890 + SEQ_A : sequencer generic map ("_-__-_---__") port map (clk, a); + SEQ_B : sequencer generic map ("__-__-___-_") port map (clk, b); + + + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + + -- This assertion holds + FELL_0_a : assert always (fell(a) -> b); + + -- Workaround needed before fell() is implemented + -- With VHDL glue logic generating the + -- previous value of a and simple comparing the two values + d_reg : block is + signal a_prev : std_logic := '0'; + begin + process (clk) is + begin + if rising_edge(clk) then + a_prev <= a; + end if; + end process; + FELL_1_a : assert always (not a and a_prev -> b); + end block d_reg; + + -- Another workaround by using simple SERE concatenation on LHS + FELL_2_a : assert always {a; not a} |-> b; + + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 11); + -- synthesis translate_on + + +end architecture psl; diff --git a/src/psl_rose.vhd b/src/psl_rose.vhd new file mode 100644 index 0000000..e6003d1 --- /dev/null +++ b/src/psl_rose.vhd @@ -0,0 +1,57 @@ +library ieee; + use ieee.std_logic_1164.all; + +use work.pkg.all; + + +entity psl_rose is + port ( + clk : in std_logic + ); +end entity psl_rose; + + +architecture psl of psl_rose is + + signal a, b : std_logic; + +begin + + + -- 01234567890 + SEQ_A : sequencer generic map ("_--__-_---_") port map (clk, a); + SEQ_B : sequencer generic map ("_-___-_-___") port map (clk, b); + + + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + + -- This assertion holds + ROSE_0_a : assert always (rose(a) -> b); + + -- Workaround needed before rose() is implemented + -- With VHDL glue logic generating the + -- previous value of a and simple comparing the two values + d_reg : block is + signal a_prev : std_logic := '0'; + begin + process (clk) is + begin + if rising_edge(clk) then + a_prev <= a; + end if; + end process; + ROSE_1_a : assert always (a and not a_prev -> b); + end block d_reg; + + -- Another workaround by using simple SERE concatenation on LHS + FELL_2_a : assert always {not a; a} |-> b; + + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 11); + -- synthesis translate_on + + +end architecture psl; diff --git a/src/psl_stable.vhd b/src/psl_stable.vhd new file mode 100644 index 0000000..f0d6995 --- /dev/null +++ b/src/psl_stable.vhd @@ -0,0 +1,64 @@ +library ieee; + use ieee.std_logic_1164.all; + +use work.pkg.all; + + +entity psl_stable is + port ( + clk : in std_logic + ); +end entity psl_stable; + + +architecture psl of psl_stable is + + signal valid, ack, a : std_logic; + signal b : std_logic_vector(3 downto 0); + +begin + + + -- 0123456789 + SEQ_VALID : sequencer generic map ("_--__---__") port map (clk, valid); + SEQ_ACK : sequencer generic map ("__-____-__") port map (clk, ack); + SEQ_A : sequencer generic map ("_--_______") port map (clk, a); + SEQ_B : hex_sequencer generic map ("0110066600") port map (clk, b); + + + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + + -- This assertion holds + STABLE_0_a : assert always {not valid; valid} -> next (stable(a) until_ ack); + + -- This assertion holds + STABLE_1_a : assert always {not valid; valid} -> next (stable(b) until_ ack); + + -- Workaround needed before stable() is implemented + -- With VHDL glue logic generating the + -- previous value of a and simple comparing the two values + a_reg : block is + signal a_prev : std_logic; + signal b_prev : std_logic_vector(b'range); + begin + process (clk) is + begin + if rising_edge(clk) then + a_prev <= a; + b_prev <= b; + end if; + end process; + STABLE_2_a : assert always {not valid; valid} |=> (a = a_prev until_ ack); + STABLE_3_a : assert always {not valid; valid} |=> (b = b_prev until_ ack); + end block a_reg; + + + -- Stop simulation after longest running sequencer is finished + -- Simulation only code by using pragmas + -- synthesis translate_off + stop_sim(clk, 10); + -- synthesis translate_on + + +end architecture psl;