data/property/cnes/STD_04800.pro


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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

(tag_existing
   (
      (wfm waveform STD_04800_DOUBLE_SENSITIVITY_EDGE_CLOCK)
   )
   (and
      (exists ps_re process
         (CTL_verifies ps_re
            (EF
               (or
                  (and
                     (is_read_structure "(??)")
                     (is_read_element "0" "rising_edge")
                     (is_read_element "1" wfm)
                  )
                  (and
                     (is_read_structure "(?(??)(???))")
                     (is_read_element "0" "and")
                     (is_read_element "1" "event")
                     (is_read_element "2" wfm)
                     (is_read_element "3" "=")
                     (or
                        (and
                           (is_read_element "4" wfm)
                           (is_read_element "5" "'1'")
                        )
                        (and
                           (is_read_element "4" "'1'")
                           (is_read_element "5" wfm)
                        )
                     )
                  )
                  (and
                     (is_read_structure "(?(???)(??))")
                     (is_read_element "0" "and")
                     (is_read_element "1" "=")
                     (or
                        (and
                           (is_read_element "2" wfm)
                           (is_read_element "3" "'1'")
                        )
                        (and
                           (is_read_element "2" "'1'")
                           (is_read_element "3" wfm)
                        )
                     )
                     (is_read_element "4" "event")
                     (is_read_element "5" wfm)
                  )
               )
            )
         )
      )
      (exists ps_fe process
         (CTL_verifies ps_fe
            (EF
               (or
                  (and
                     (is_read_structure "(??)")
                     (is_read_element "0" "falling_edge")
                     (is_read_element "1" wfm)
                  )
                  (and
                     (is_read_structure "(?(??)(???))")
                     (is_read_element "0" "and")
                     (is_read_element "1" "event")
                     (is_read_element "2" wfm)
                     (is_read_element "3" "=")
                     (or
                        (and
                           (is_read_element "4" wfm)
                           (is_read_element "5" "'0'")
                        )
                        (and
                           (is_read_element "4" "'0'")
                           (is_read_element "5" wfm)
                        )
                     )
                  )
                  (and
                     (is_read_structure "(?(???)(??))")
                     (is_read_element "0" "and")
                     (is_read_element "1" "=")
                     (or
                        (and
                           (is_read_element "2" wfm)
                           (is_read_element "3" "'0'")
                        )
                        (and
                           (is_read_element "2" "'0'")
                           (is_read_element "3" wfm)
                        )
                     )
                     (is_read_element "4" "event")
                     (is_read_element "5" wfm)
                  )
               )
            )
         )
      )
   )
)