From f2b7e406b8e77df22ef379a5e880f64d1e5043b9 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 19 Sep 2017 14:05:52 +0200 Subject: Fixes case/when models, regroups properties. --- data/property/CNE_00100.pro | 59 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 data/property/CNE_00100.pro (limited to 'data/property/CNE_00100.pro') diff --git a/data/property/CNE_00100.pro b/data/property/CNE_00100.pro new file mode 100644 index 0000000..1b0893e --- /dev/null +++ b/data/property/CNE_00100.pro @@ -0,0 +1,59 @@ +(tag_existing + ( + (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" "=") + (or + (and + (is_read_element "1" "'0'") + (is_read_element "2" wfm) + ) + (and + (is_read_element "1" wfm) + (is_read_element "2" "'0'") + ) + ) + ) + ) + ) + ) + ;; and that signal is never tested against '1'. + (not + (exists p2 process + (CTL_verifies p2 + (EF + (and + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (or + (and + (is_read_element "1" "'1'") + (is_read_element "2" wfm) + ) + (and + (is_read_element "1" wfm) + (is_read_element "2" "'1'") + ) + ) + ) + ) + ) + ) + ) + ) + ;; Then it is misnamed. +) -- cgit v1.2.3-70-g09d2