Add example for cover directive

formal/psl_cover.sby

@@ -0,0 +1,18 @@
+[tasks]
+bmc
+
+[options]
+depth 25
+bmc: mode cover
+
+[engines]
+bmc: smtbmc z3
+
+[script]
+bmc: ghdl --std=08 pkg.vhd sequencer.vhd psl_cover.vhd -e psl_cover
+prep -top psl_cover
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_cover.vhd

formal/tests.mk

@@ -18,4 +18,5 @@ psl_sere_overlapping_suffix_impl \
 psl_sere_non_overlapping_suffix_impl \
 psl_sere_consecutive_repetition \
 psl_sere_non_consecutive_repeat_repetition \
-psl_sere_non_consecutive_goto_repetition
+psl_sere_non_consecutive_goto_repetition \
+psl_cover

src/psl_cover.vhd

@@ -0,0 +1,74 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity psl_cover is
+  port (
+    clk : in std_logic
+  );
+end entity psl_cover;
+
+
+architecture psl of psl_cover is
+
+  signal req, busy, done : std_logic;
+
+begin
+
+
+  --                                 0123456789
+  SEQ_REQ  : sequencer generic map ("_-________") port map (clk, req);
+  SEQ_BUSY : sequencer generic map ("__-_-_-___") port map (clk, busy);
+  SEQ_DONE : sequencer generic map ("________-_") port map (clk, done);
+
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- Covers a transfer request
+  -- This cover directive holds at cycle 1
+  COVER_0_c : cover {req}
+    report "Transfer requested";
+
+  -- Covers started processing of transfers
+  -- This cover directive holds at cycle 2
+  COVER_1_c : cover {req; {{busy[=1]} && {not done[+]}}}
+    report "Transfer in progress";
+
+  -- Covers each transfer with length in range 1 to 8
+  -- This cover directive holds at cycle 8
+  COVER_2_c : cover {req; {{busy[=1 to 8]} && {not done[+]}}; done}
+    report "Transfer done";
+
+  -- Cover transfers with length in range 1 to 8 separately
+  cover_transfer_lengths : for i in 1 to 8 generate
+  begin
+    -- Don't works with GHDL, but should? Is a defined as static in the
+    -- generate body?
+    --COVER_TRANSFER_LENGTH_c : cover {req; {{busy[=i]} && {not done[+]}}; done};
+  end generate cover_transfer_lengths;
+
+  -- Workaround: writing separate cover directives for
+  -- each length, very tedious
+  -- Only length 3 holds at cycle 8, all others not
+  COVER_LENGTH_1_c : cover {req; {{busy[=1]} && {not done[+]}}; done};
+  COVER_LENGTH_2_c : cover {req; {{busy[=2]} && {not done[+]}}; done};
+  COVER_LENGTH_3_c : cover {req; {{busy[=3]} && {not done[+]}}; done};
+  COVER_LENGTH_4_c : cover {req; {{busy[=4]} && {not done[+]}}; done};
+  COVER_LENGTH_5_c : cover {req; {{busy[=5]} && {not done[+]}}; done};
+  COVER_LENGTH_6_c : cover {req; {{busy[=6]} && {not done[+]}}; done};
+  COVER_LENGTH_7_c : cover {req; {{busy[=7]} && {not done[+]}}; done};
+  COVER_LENGTH_8_c : cover {req; {{busy[=8]} && {not done[+]}}; done};
+
+  -- BTW: GHDL creates a cover directive for each assert directive
+  -- which is really nice. So you can run SymbiYosys in cover mode
+  -- to see if your assertions can actually be active.
+  -- This assertion checks for the final done at the end of transfer.
+  -- In cover mode, the LHS side of the property has to hold.
+  -- This cover directive holds at cycle 6
+  ASSERT_a : assert always {req; {{busy[=3]} && {not done[+]}}} |=> {done};
+
+
+end architecture psl;