From 126fb20387caffaa8e05e2a5fee1be78ab1cb1ff Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 19 Jul 2017 14:32:12 +0200 Subject: Dammit, it says flip-flops are combinational... --- data/property/combinational_processes.pro | 14 ++++++-------- 1 file 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) ) ) ) -- cgit v1.2.3-70-g09d2