property/likely_a_clock.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

(seek
   (
      (clock port)
   )
   (exists wf waveform
      (and
         (is_waveform_of wf clock)
         (exists ps process
            (and
               (is_accessed_by wf ps)
               (is_in_sensitivity_list wf ps)
               (CTL_verifies ps
                     (EF
                        (and
                           (kind "if")
                           (or
                              (and
                                 (is_read_structure "(??)")
                                 (or
                                    (is_read_element "0" "falling_edge")
                                    (is_read_element "0" "rising_edge")
                                 )
                                 (is_read_element "1" wf)
                              )
                              (and
                                 (is_read_structure "(?(??)(???))")
                                 (is_read_element "0" "and")
                                 (is_read_element "1" "event")
                                 (is_read_element "2" wf)
                                 (is_read_element "3" "=")
                                 (or
                                    (is_read_element "4" wf)
                                    (is_read_element "5" wf)
                                 )
                              )
                              (and
                                 (is_read_structure "(?(???)(??))")
                                 (is_read_element "0" "and")
                                 (is_read_element "1" "=")
                                 (or
                                    (is_read_element "2" wf)
                                    (is_read_element "3" wf)
                                 )
                                 (is_read_element "4" "event")
                                 (is_read_element "5" wf)
                              )
                           )
                        )
                     )
                  )
               )
            )
         )
      )
   )
)