blob: 83a80a4e50eb530a8c9a81e99e478ed334ab2509 (
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
|
#require "flip_flop"
(seek
(
(x_re waveform)
)
(and
(not (string_matches [identifier [is_waveform_of x_re]] ".*_re$"))
;; 'x' is the signal 'x_re' detects the rising edge of.
(exists x waveform
(and
(not (eq x x_re))
;; 'x_r1' is 'x' delayed by a flipflop
(exists x_r1 waveform
(and
(not (eq x_r1 x_re))
(not (eq x_r1 x))
;; 'ps2' is the process describing 'x_re' as the rising edge
(exists ps2 process
(and
(is_in_sensitivity_list x_r1 ps2)
(is_in_sensitivity_list x ps2)
(is_accessed_by x_re ps2)
(CTL_verifies ps2
(AF
(and
(expr_writes x_re)
(is_read_element "0" "and")
(or
;; x_re <= (not x_r1) and x
(and
(is_read_structure "(?(??)?)")
(is_read_element "1" "not")
(is_read_element "2" x_r1)
(is_read_element "3" x)
)
;; x_re <= x and (not x_r1)
(and
(is_read_structure "(??(??))")
(is_read_element "1" x)
(is_read_element "2" "not")
(is_read_element "3" x_r1)
)
)
(AX
(not
(EF
(expr_writes x_r1)
)
)
)
)
)
)
)
)
;; 'ps1' is the process describing 'x_r1' as a flipflop.
(exists ps1 process
(and
(is_accessed_by x_r1 ps1)
(is_accessed_by x ps1)
(is_explicit_process ps1)
(flip_flop x_r1 _ ps1)
(CTL_verifies ps1
(EF
(and
(expr_writes x_r1)
(is_read_structure "?")
(is_read_element "0" x)
)
)
)
)
)
))))))
|
