summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to 'data/property/combinational_processes.pro')
-rw-r--r--data/property/combinational_processes.pro14
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))
+ )
)
)
)