| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data/property')
| -rw-r--r-- | data/property/CNE_01100.pro | 35 | ||||
| -rw-r--r-- | data/property/CNE_01700.pro | 161 | ||||
| -rw-r--r-- | data/property/simple_flip_flop.pro | 5 |
3 files changed, 26 insertions, 175 deletions
diff --git a/data/property/CNE_01100.pro b/data/property/CNE_01100.pro index 6ed2cff..ad94747 100644 --- a/data/property/CNE_01100.pro +++ b/data/property/CNE_01100.pro @@ -2,28 +2,19 @@ ( (pt port CNE_01100_BAD_NAME) ) - (exists pt2 port - (and -;; Goes into infinity: -;; (has_mode pt2 _) -;; (has_mode pt2 "in") -;; Fixes all: - (eq pt2 pt) - (not - (or - (and - (string_matches [identifier pt] "^i_.*") - (has_mode pt "in") - ) - (and - (string_matches [identifier pt] "^o_.*") - (has_mode pt "out") - ) - (and - (string_matches [identifier pt] "^b_.*") - (has_mode pt "inout") - ) - ) + (not + (or + (and + (string_matches [identifier pt] "^i_.*") + (has_mode pt "in") + ) + (and + (string_matches [identifier pt] "^o_.*") + (has_mode pt "out") + ) + (and + (string_matches [identifier pt] "^b_.*") + (has_mode pt "inout") ) ) ) diff --git a/data/property/CNE_01700.pro b/data/property/CNE_01700.pro index 7452a3c..2327afc 100644 --- a/data/property/CNE_01700.pro +++ b/data/property/CNE_01700.pro @@ -1,9 +1,11 @@ +#require "flip_flop" + (tag_existing ( (x_re waveform CNE_01700_HAS_BAD_NAME) ) (and - (not (string_matches [identifier [is_waveform_of x_re]] ".*_re")) + (not (string_matches [identifier [is_waveform_of x_re]] ".*_re$")) ;; 'x' is the signal 'x_re' detects the rising edge of. (exists x waveform (and @@ -58,159 +60,16 @@ (is_accessed_by x_r1 ps1) (is_accessed_by x ps1) (is_explicit_process ps1) -;; 'clk1' is the clock controlling that flipflop -(exists clk1 waveform - (and - (is_in_sensitivity_list clk1 ps1) - (not (eq clk1 x_re)) - (not (eq clk1 x)) - (not (eq clk1 x_r1)) - (or -;; 'ps1' could be a simple flipflop -(CTL_verifies ps1 - (AF - (and - (kind "if") - (or - (and - (is_read_structure "(??)") - (or - (is_read_element "0" "falling_edge") - (is_read_element "0" "rising_edge") - ) - (is_read_element "1" clk1) - ) - (and - (is_read_structure "(?(??)(???))") - (is_read_element "0" "and") - (is_read_element "1" "event") - (is_read_element "2" clk1) - (is_read_element "3" "=") - (or - (is_read_element "4" clk1) - (is_read_element "5" clk1) - ) - ) - (and - (is_read_structure "(?(???)(??))") - (is_read_element "0" "and") - (is_read_element "1" "=") - (or - (is_read_element "2" clk1) - (is_read_element "3" clk1) - ) - (is_read_element "4" "event") - (is_read_element "5" clk1) - ) - ) - (EX + (_flip_flop x_r1 _ ps1) + (CTL_verifies ps1 + (EF (and - (has_option "cond_was_true") - (does_not_reach_parent_before - (and - (expr_writes x_r1) - (is_read_structure "?") - (is_read_element "0" x) - (AX - (not - (EF - (expr_writes x_r1) - ) - ) - ) - ) - ) + (expr_writes x_r1) + (is_read_structure "?") + (is_read_element "0" x) ) ) ) ) ) -;; 'ps1' could be a flipflop with reset -;; 'rst1' is that reset signal -(exists rst1 waveform - (and - (is_in_sensitivity_list rst1 ps1) - (not (eq rst1 x_re)) - (not (eq rst1 x)) - (not (eq rst1 x_r1)) - (not (eq rst1 clk1)) -(CTL_verifies ps1 - (AF - (and - (kind "if") - (is_read_structure "(???)") - (is_read_element "0" "=") - (is_read_element _ rst1) - (EX - (and - (not (has_option "cond_was_true")) - (kind "if") - (or - (and - (is_read_structure "(??)") - (or - (is_read_element "0" "falling_edge") - (is_read_element "0" "rising_edge") - ) - (is_read_element "1" clk1) - ) - (and - (is_read_structure "(?(??)(???))") - (is_read_element "0" "and") - (is_read_element "1" "event") - (is_read_element "2" clk1) - (is_read_element "3" "=") - (or - (is_read_element "4" clk1) - (is_read_element "5" clk1) - ) - ) - (and - (is_read_structure "(?(???)(??))") - (is_read_element "0" "and") - (is_read_element "1" "=") - (or - (is_read_element "2" clk1) - (is_read_element "3" clk1) - ) - (is_read_element "4" "event") - (is_read_element "5" clk1) - ) - ) - (EX - (and - (has_option "cond_was_true") - (does_not_reach_parent_before - (and - (expr_writes x_r1) - (is_read_structure "?") - (is_read_element "0" x) - (AX - (not - (EF - (expr_writes x_r1) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) -) -) -) -) -) -) -) -) -) -) -) -) -) +)))))) diff --git a/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro index b054c7f..09ef98b 100644 --- a/data/property/simple_flip_flop.pro +++ b/data/property/simple_flip_flop.pro @@ -9,7 +9,8 @@ (is_explicit_process ps) (is_in_sensitivity_list clk ps) (CTL_verifies ps - (AF + (AU + (not (expr_writes reg)) (and (kind "if") (or @@ -46,7 +47,7 @@ ) (EX (and - (has_option "COND_WAS_TRUE") + (has_option "cond_was_true") (does_not_reach_parent_before (and (expr_writes reg) |