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

(seek
   (
      (wfm waveform)
   )
   (exists ps process
      (and
         (is_explicit_process ps)
         (forall sl1 waveform
            (and
               (CTL_verifies ps
                  (implies
                     (EF (expr_writes sl1))
                     (AF (expr_writes sl1))
                  )
               )
               (implies
                  (exists target waveform
                     (CTL_verifies ps
                        (EF
                           (and
                              (is_read_element _ sl1)
                              (not
                                 (and
                                    (expr_writes target)
                                    (AX
                                       (AF
                                          (expr_writes target)
                                       )
                                    )
                                 )
                              )
                           )
                        )
                     )
                  )
                  (is_in_sensitivity_list sl1 ps)
               )
            )
         )
         (CTL_verifies ps
            (AF
               (and
                  (or
                     (kind "case")
                     (kind "if")
                  )
                  (does_not_reach_parent_before
                     (and
                        (expr_writes wfm)
                        (AX
                           (not
                              (EF
                                 (expr_writes wfm)
                              )
                           )
                        )
                     )
                  )
               )
            )
         )
      )
   )
)