| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data/property/combinational_processes.pro')
| -rw-r--r-- | data/property/combinational_processes.pro | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro index 9300672..7f8405f 100644 --- a/data/property/combinational_processes.pro +++ b/data/property/combinational_processes.pro @@ -2,7 +2,7 @@ ( (ps process STRUCT_COMBINATIONAL_PROCESS) ) - (forall sl1 signal + (forall sl1 waveform (and (CTL_verifies ps (implies @@ -11,18 +11,16 @@ ) ) (implies - (exists target signal + (exists target waveform (CTL_verifies ps (EF (and (expr_reads sl1) + (expr_writes target) (not - (and - (expr_writes target) - (AX - (AF - (expr_writes target) - ) + (AX + (AF + (expr_writes target) ) ) ) |