From d40f3e7845b00bbcd534c3ba299851614afb1386 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 18 Sep 2017 10:37:24 +0200 Subject: Fixes combinational processes property. --- data/property/combinational_processes.pro | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro index b3f2633..b0f0d0c 100644 --- a/data/property/combinational_processes.pro +++ b/data/property/combinational_processes.pro @@ -5,28 +5,22 @@ (forall sl1 waveform (and (implies + ;; If a signal is read, (exists target waveform (CTL_verifies ps (EF - (and - (is_read_element _ sl1) - (expr_writes target) - (not - (AX - (AF - (expr_writes target) - ) - ) - ) - ) + (is_read_element _ sl1) ) ) ) + ;; Then it must be in the sensitivity list. (is_in_sensitivity_list sl1 ps) ) (CTL_verifies ps (implies + ;; If a signal is somehow assigned by this process, (EF (expr_writes sl1)) + ;; Then it is assigned at every execution of the process. (AF (expr_writes sl1)) ) ) -- cgit v1.2.3-70-g09d2