blob: 90f9d3ab76aafdb54d2964c831630773992c4f01 (
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
library ieee;
use ieee.std_logic_1164.all;
entity compare_psl_p_plus is
port(
clk_in: in std_logic;
a_in: in std_logic;
b_in: in std_logic;
c_in: in std_logic
);
end;
architecture rtl of compare_psl_p_plus is
component psl_p_plus is
port(
clk_in: in std_logic;
a_in: in std_logic;
b_in: in std_logic;
c_in: in std_logic;
\p_plus_psl.A\: out std_logic;
\p_plus_psl.EN\: out std_logic
);
end component;
signal first_cycle: std_logic := '1';
signal nda_r0: std_logic := '0';
signal nda_res: std_logic;
signal p_plus_psl_a: std_logic;
signal p_plus_psl_en: std_logic;
signal p_plus_psl: std_logic;
begin
dut: psl_p_plus
port map(
clk_in => clk_in,
a_in => a_in,
b_in => b_in,
c_in => c_in,
\p_plus_psl.A\ => p_plus_psl_a,
\p_plus_psl.EN\ => p_plus_psl_en
);
p_plus_psl <= p_plus_psl_en and p_plus_psl_a;
reference_model_sync_pr: process(clk_in)
begin
if rising_edge(clk_in) then
first_cycle <= '0';
nda_r0 <= '0';
if first_cycle = '1' and a_in = '1' then
nda_r0 <= '1';
end if;
if nda_r0 = '1' and a_in = '1' then
nda_r0 <= '1';
end if;
end if;
end process;
reference_model_async_pr: process(all)
begin
nda_res <= '1';
if nda_r0 = '1' and b_in = '1' and c_in = '0' then
nda_res <= '0';
end if;
end process;
default clock is rising_edge(clk_in);
comparison_assert: postponed assert nda_res = p_plus_psl;
cover_psl: cover {true; true; p_plus_psl = '0'};
cover_psl_first: cover {true; true; [*]; p_plus_psl = '0'};
end;
|
