| summaryrefslogtreecommitdiff | 
diff options
Diffstat (limited to 'data/property/combinational_processes.pro')
| -rw-r--r-- | data/property/combinational_processes.pro | 14 | 
1 files changed, 7 insertions, 7 deletions
| diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro index 7f8405f..5008a06 100644 --- a/data/property/combinational_processes.pro +++ b/data/property/combinational_processes.pro @@ -4,12 +4,6 @@     )     (forall sl1 waveform        (and -         (CTL_verifies ps -            (implies -               (EF (expr_writes sl1)) -               (AF (expr_writes sl1)) -            ) -         )           (implies              (exists target waveform                 (CTL_verifies ps @@ -28,7 +22,13 @@                    )                 )              ) -            (is_in_sensitivity_list ps sl1) +            (is_in_sensitivity_list sl1 ps) +         ) +         (CTL_verifies ps +            (implies +               (EF (expr_writes sl1)) +               (AF (expr_writes sl1)) +            )           )        )     ) | 


