blob: 1b0fd5b0fc2b0b8a60bbb0cc012ac03ff5a4fc58 (
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
28
29
30
31
32
33
34
|
library ieee;
use ieee.std_logic_1164.all;
entity repro is
port (
a, c, d, e, f, x : std_logic;
b : std_logic_vector(3 downto 0);
clk : in std_logic
);
end;
architecture psl of repro is
begin
-- All is sensitive to rising edge of clk
default clock is rising_edge(clk);
NEXT_EVENT_0_a :
-- assert always ((a and b = x"4") -> next_event_a(c)[1 to 2](b = x"4"))
-- assert always ((a and b = x"4") -> ({(not c)[*]; c; {[*0] | { (not c)[*]; c}}} |->(b = x"4")))
-- assert always (a -> ({c; d; {[*0] | {(not e)[*];f}}} |->x))
-- assert always (a -> ({c; {[*0] | {d[*]; e}}} |->x))
-- assert always ({c; {[*0] | {d[*]; e}}} |->x)
-- assert never {c; {[*0] | {d[*]; e}}}
-- assert always ({c | {c; d[*]; e}} |->x)
-- assert always ({c; {d[*]; e}} |->x)
report "NEXT_EVENT_0_a failed";
end architecture psl;
-- next_event_a(b)[k:l](p) = {b[->k:l]} |-> p
-- b[->k:l] = b[->k] | ... | b[->l]
-- = {!b[*];b}[*k:l]
-- s[*i:j] = s[*i] | ... | s[*j]
-- next_event_a(b)[k:l](p) = {{!b[*];b}[*k] | .. | {!b[*];b}[*l] } |-> p
|
