blob: b213d96d51cdc6c1e4791a56161f005d2bc25859 (
plain)
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
26
27
|
library ieee;
use ieee.std_logic_1164.all;
entity top2 is
end entity;
architecture a of top2 is
signal a,b,c,d : std_logic := '0';
signal clk_sys, clk1, clk2 : std_logic;
begin
-- psl default clock is clk_sys;
-- Following throws bug occured with: "build_sere_fa: cannot handle N_IMP_SEQ"
-- This is strange because with "always" this is working.
-- According to PSL LRM 2003 FL_Property production for "always" is the
-- same as for "never":
-- FL_Property ::=
-- always FL_Property
-- | always Sequence
--
-- FL_Property ::=
-- never FL_Property
-- | never Sequence
-- Therefore I think if sequence implication works with one, it shall work
-- also with other.
-- psl my_seq : assert never {a} |=> {b; c};
end a;
|
