blob: 656c2d6592fd735876cb5c99ac5969b747fc2b02 (
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
|
vunit i_rising_pulse_detector(rising_pulse_detector(rising_pulse_detector_1))
{
default clock is rising_edge(clk);
-- reset is true at beginning
f_reset_initial : assume {rst};
-- no reset after begining
f_reset_disable : assume always {not rst} |=> {not rst};
--working cover without generate
fc_output_4 : cover {output_pulse(4) = '1'};
-- generate cover pulse
g1: for I in 0 to 15 generate
cover {output_pulse(I) = '1'};
end generate;
--working bmc witout generate:
f_ouptut_7 : assert always {(not rst) and output_pulse(7) = '1'}
|=> {output_pulse(7) = '0'};
-- generate pulse one cycle assertion
g2: for J in 0 to 15 generate
assert always {(not rst) and output_pulse(J) = '1'} |=> {output_pulse(J) = '0'};
end generate;
} -- vunit i_rising_pulse_detector(rising_pulse_detector(rising_pulse_detector_1))
|
