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

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