| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data')
| -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)) + ) ) ) ) |