| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | data/property/cnes/CNE_00100.pro | 13 | ||||
| -rw-r--r-- | data/property/combinational_processes.pro | 16 |
2 files changed, 15 insertions, 14 deletions
diff --git a/data/property/cnes/CNE_00100.pro b/data/property/cnes/CNE_00100.pro index 221008b..1b0893e 100644 --- a/data/property/cnes/CNE_00100.pro +++ b/data/property/cnes/CNE_00100.pro @@ -3,11 +3,16 @@ (wfm waveform CNE_00100_HAS_BAD_NAME) ) (and + ;; If the name of the waveform does not end in "_n", (not (string_matches [identifier [is_waveform_of wfm]] ".*_n")) + ;; and there is a process (exists p1 process + ;; that. (CTL_verifies p1 + ;; at some point, (EF (and + ;; has a condition which tests the the signal against '0'. (kind "if") (is_read_structure "(???)") (is_read_element "0" "=") @@ -25,8 +30,9 @@ ) ) ) + ;; and that signal is never tested against '1'. (not - (exists p2 process + (exists p2 process (CTL_verifies p2 (EF (and @@ -35,12 +41,12 @@ (is_read_element "0" "=") (or (and - (is_read_element "1" "'0'") + (is_read_element "1" "'1'") (is_read_element "2" wfm) ) (and (is_read_element "1" wfm) - (is_read_element "2" "'0'") + (is_read_element "2" "'1'") ) ) ) @@ -49,4 +55,5 @@ ) ) ) + ;; Then it is misnamed. ) 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)) ) ) |