data/property/combinational_processes.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

(tag_existing
   (
      (ps process STRUCT_COMBINATIONAL_PROCESS)
   )
   (forall sl1 signal
      (and
         (CTL_verifies ps
            (implies
               (EF (expr_writes sl1))
               (AF (expr_writes sl1))
            )
         )
         (implies
            (exists target signal
               (CTL_verifies ps
                  (EF
                     (and
                        (expr_reads sl1)
                        (not
                           (and
                              (expr_writes target)
                              (AX
                                 (AF
                                    (expr_writes target)
                                 )
                              )
                           )
                        )
                     )
                  )
               )
            )
            (is_in_sensitivity_list ps sl1)
         )
      )
   )
)