| summaryrefslogtreecommitdiff | 
diff options
Diffstat (limited to 'data/property/cnes/CNE_05100.pro')
| -rw-r--r-- | data/property/cnes/CNE_05100.pro | 64 | 
1 files changed, 0 insertions, 64 deletions
diff --git a/data/property/cnes/CNE_05100.pro b/data/property/cnes/CNE_05100.pro deleted file mode 100644 index dd8b2c1..0000000 --- a/data/property/cnes/CNE_05100.pro +++ /dev/null @@ -1,64 +0,0 @@ -(tag_existing -   ( -      (wfm waveform STRUCT_SINGLE_PROCESS_MULTIPLEXOR) -   ) -   (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) -                              ) -                           ) -                        ) -                     ) -                  ) -               ) -            ) -         ) -      ) -   ) -)  | 


