From f8d2ac230eaaf1c5e812f914d9e17d5d14e799c5 Mon Sep 17 00:00:00 2001
From: tmeissner <programming@goodcleanfun.de>
Date: Mon, 6 Sep 2021 17:36:11 +0200
Subject: [PATCH] Update PSL abort example as ghdl/ghdl#1654 was fixed

---
 README.md             |  7 ++++++-
 issues/issue_1832.vhd |  3 +++
 issues/tests.mk       |  4 +++-
 src/psl_abort.vhd     | 17 ++++++++++++++---
 4 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 1bd0b92..c1a7d10 100644
--- a/README.md
+++ b/README.md
@@ -59,6 +59,12 @@ The next lists will grow during further development
 * or operator (`|`)
 * `within` operator
 
+### Other operators
+
+* `abort` operator
+* `async_abort` operator
+* `sync_abort` operator
+
 ### Built-in functions
 
 * `prev()` function (Synthesis only)
@@ -94,7 +100,6 @@ The next lists will grow during further development
 
 ## 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)
diff --git a/issues/issue_1832.vhd b/issues/issue_1832.vhd
index 64fd0e9..9792479 100644
--- a/issues/issue_1832.vhd
+++ b/issues/issue_1832.vhd
@@ -76,6 +76,9 @@ begin
   default clock is rising_edge(clk);
 
   -- This assertion should hold
+  -- Beware: As this is a liveness property, SymbiYosys has
+  -- to be used in live mode. Currently GHDL doesn't really support
+  -- liveness properties in synthesis (needed for formal verification).
   INF_a : assert always {a} |=> {not b[*0 to inf]; b};
 
 
diff --git a/issues/tests.mk b/issues/tests.mk
index 99ee6cd..fe2ddc2 100644
--- a/issues/tests.mk
+++ b/issues/tests.mk
@@ -8,4 +8,6 @@ issue_1345 \
 issue_1366 \
 issue_1367 \
 issue_1372 \
-issue_1591
\ No newline at end of file
+issue_1591 \
+issue_1658 \
+issue_1832
\ No newline at end of file
diff --git a/src/psl_abort.vhd b/src/psl_abort.vhd
index d771bde..2838762 100644
--- a/src/psl_abort.vhd
+++ b/src/psl_abort.vhd
@@ -17,6 +17,7 @@ architecture psl of psl_abort is
 
 begin
 
+  -- Creating an abort signal which is asynchronously set & reset
   d <= '0', '1' after 1100 ps, '0' after 1400 ps;
 
   --                              0123456789
@@ -35,11 +36,21 @@ begin
   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
+  -- GHDL seemed 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 at cycle 4 as d is 0 all the time
+  -- Is fixed now, see issue ghdl/ghdl#1654 
   WITH_ABORT_1_a : assert (always a -> next (b before a)) abort d;
 
+  -- async_abort is similar to abort
+  -- In formal this assertion fails at cycle 4 as d is 0 all the time
+  WITH_ABORT_2_a : assert (always a -> next (b before a)) async_abort d;
+
+  -- sync_abort is working on synchronously events
+  -- This assertion holds
+  WITH_ABORT_3_a : assert (always a -> next (b before a)) sync_abort c;
+
+
   -- Stop simulation after longest running sequencer is finished
   -- Simulation only code by using pragmas
   -- synthesis translate_off