Add example for PSL abort operator

README.md

@@ -92,8 +92,9 @@ The next lists will grow during further development
 * PSL macros (`%for`, `%if`)
 * `union` expression
 
-## Under investigation
+## Supported, but under investigation
 
+* `abort` operator (Seems to be a `sync_abort`, while it has to be a `async_abort`)
 * `before_` operator (Seems that LHS & RHS of operator have to be active at same cycle, see psl_before.vhd)
 * `next_event_a[i to j]` operator
 * `eventually!` behaviour with liveness proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345)

formal/psl_abort.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_abort.vhd -e psl_abort
+prep -top psl_abort
+
+[files]
+../src/pkg.vhd
+../src/sequencer.vhd
+../src/psl_abort.vhd

formal/tests.mk

@@ -35,4 +35,5 @@ psl_onehot \
 psl_onehot0 \
 psl_vunit \
 yosys_anyconst \
-yosys_anyseq
+yosys_anyseq \
+psl_abort

sim/Makefile

@@ -14,7 +14,7 @@ all: ${psl_tests}
 	ghdl -a --std=$(VHD_STD) -fpsl --workdir=work/$@ ../src/$@.vhd
 	ghdl -a --std=$(VHD_STD) --workdir=work/$@ work/$@/testbench.vhd
 	ghdl -e --std=$(VHD_STD) -fpsl --workdir=work/$@ -o work/$@/tb_$@ tb_$@
-	cd work/$@; ghdl -r --std=$(VHD_STD) tb_$@ --wave=$@.ghw --psl-report=$@_psl_coverage.json
+	cd work/$@; ghdl -r --std=$(VHD_STD) -fpsl tb_$@ --wave=$@.ghw --psl-report=$@_psl_coverage.json
 
 work/%/testbench.vhd: template.vhd
 	mkdir -p work; mkdir -p $(dir $@)

sim/tests.mk

@@ -28,4 +28,5 @@ psl_sere_concat \
 psl_sere_fusion \
 psl_sequence \
 psl_property \
-psl_endpoint
+psl_endpoint \
+psl_abort

src/psl_abort.vhd

@@ -0,0 +1,50 @@
+library ieee;
+  use ieee.std_logic_1164.all;
+
+use work.pkg.all;
+
+
+entity psl_abort is
+  port (
+    clk : in std_logic
+  );
+end entity psl_abort;
+
+
+architecture psl of psl_abort is
+
+  signal a, b, c, d : std_logic;
+
+begin
+
+  d <= '0', '1' after 1100 ps, '0' after 1400 ps;
+
+  --                              0123456789
+  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);
+  --  D :                         _|________
+
+  -- All is sensitive to rising edge of clk
+  default clock is rising_edge(clk);
+
+  -- This assertion doesn't hold at cycle 4
+  WITHOUT_ABORT_a : assert (always a -> next (b before a));
+
+  -- This assertion holds
+  WITH_ABORT_0_a : assert (always a -> next (b before a)) abort c;
+
+  -- In simulation this assertion should also hold, but it does not
+  -- GHDL seems to implement abort as sync_abort instead of async_abort
+  -- See 1850-2010 6.2.1.5.1 abort, async_abort, and sync_abort
+  -- In formal this assertion fails as d is 0 all the time
+  WITH_ABORT_1_a : assert (always a -> next (b before a)) abort d;
+
+  -- Stop simulation after longest running sequencer is finished
+  -- Simulation only code by using pragmas
+  -- synthesis translate_off
+  stop_sim(clk, 12);
+  -- synthesis translate_on
+
+
+end architecture psl;