Browse Source

Update PSL abort example as ghdl/ghdl#1654 was fixed

master
T. Meissner 3 years ago
parent
commit
f8d2ac230e
4 changed files with 26 additions and 5 deletions
  1. +6
    -1
      README.md
  2. +3
    -0
      issues/issue_1832.vhd
  3. +3
    -1
      issues/tests.mk
  4. +14
    -3
      src/psl_abort.vhd

+ 6
- 1
README.md View File

@ -59,6 +59,12 @@ The next lists will grow during further development
* or operator (`|`) * or operator (`|`)
* `within` operator * `within` operator
### Other operators
* `abort` operator
* `async_abort` operator
* `sync_abort` operator
### Built-in functions ### Built-in functions
* `prev()` function (Synthesis only) * `prev()` function (Synthesis only)
@ -94,7 +100,6 @@ The next lists will grow during further development
## Supported, but 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) * `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 * `next_event_a[i to j]` operator
* `eventually!` behaviour with liveness proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345) * `eventually!` behaviour with liveness proofs, see [GHDL issue 1345](https://github.com/ghdl/ghdl/issues/1345)


+ 3
- 0
issues/issue_1832.vhd View File

@ -76,6 +76,9 @@ begin
default clock is rising_edge(clk); default clock is rising_edge(clk);
-- This assertion should hold -- 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}; INF_a : assert always {a} |=> {not b[*0 to inf]; b};


+ 3
- 1
issues/tests.mk View File

@ -8,4 +8,6 @@ issue_1345 \
issue_1366 \ issue_1366 \
issue_1367 \ issue_1367 \
issue_1372 \ issue_1372 \
issue_1591
issue_1591 \
issue_1658 \
issue_1832

+ 14
- 3
src/psl_abort.vhd View File

@ -17,6 +17,7 @@ architecture psl of psl_abort is
begin begin
-- Creating an abort signal which is asynchronously set & reset
d <= '0', '1' after 1100 ps, '0' after 1400 ps; d <= '0', '1' after 1100 ps, '0' after 1400 ps;
-- 0123456789 -- 0123456789
@ -35,11 +36,21 @@ begin
WITH_ABORT_0_a : assert (always a -> next (b before a)) abort c; WITH_ABORT_0_a : assert (always a -> next (b before a)) abort c;
-- In simulation this assertion should also hold, but it does not -- 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; 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 -- Stop simulation after longest running sequencer is finished
-- Simulation only code by using pragmas -- Simulation only code by using pragmas
-- synthesis translate_off -- synthesis translate_off


Loading…
Cancel
Save