testsuite/synth/issue1654/checker.vhdl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

library ieee;
  use ieee.std_logic_1164.all;

entity checker is
  port (
    clk : in std_logic;
    a, b, c, d : std_logic
  );
end;


architecture psl of checker is
begin
  -- All is sensitive to rising edge of clk
  default clock is rising_edge(clk);

  -- This assertion holds
  WITH_sync_ABORT_a : assert (always a -> next (b before a)) sync_abort c;

  -- 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
  WITH_async_ABORT_a : assert (always a -> next (b before a)) async_abort d;
end architecture psl;