| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data/property/cnes')
| -rw-r--r-- | data/property/cnes/CNE_00100.pp | 3 | ||||
| -rw-r--r-- | data/property/cnes/CNE_00100.pro | 4 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01700.pp | 3 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01700.pro | 4 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01800.pp | 3 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01800.pro | 4 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01900.pp | 3 | ||||
| -rw-r--r-- | data/property/cnes/CNE_01900.pro | 102 | ||||
| -rw-r--r-- | data/property/cnes/CNE_05100.pp | 3 | ||||
| -rw-r--r-- | data/property/cnes/STD_04800.pp | 3 |
10 files changed, 126 insertions, 6 deletions
diff --git a/data/property/cnes/CNE_00100.pp b/data/property/cnes/CNE_00100.pp new file mode 100644 index 0000000..e18ad85 --- /dev/null +++ b/data/property/cnes/CNE_00100.pp @@ -0,0 +1,3 @@ +The signal $wfm.IDENTIFIER (declared in $wfm.FILE, line $wfm.LINE, column +$wfm.COLUMN) is only tested for equality against '0'. CNE_00100 indicates such +signals should have names ending in "_n". diff --git a/data/property/cnes/CNE_00100.pro b/data/property/cnes/CNE_00100.pro index c5d0319..9cab7fc 100644 --- a/data/property/cnes/CNE_00100.pro +++ b/data/property/cnes/CNE_00100.pro @@ -3,7 +3,7 @@ (wfm waveform CNE_00100_HAS_BAD_NAME) ) (and - (not (string_matches [identifier wfm] ".*_n")) + (not (string_matches [identifier [is_waveform_of wfm]] ".*_n")) (exists p1 process (CTL_verifies p1 (EF @@ -14,7 +14,7 @@ (or (and (is_read_element "1" "'0'") - (is_read_element "2" wfm) + (IS_READ_Element "2" wfm) ) (and (is_read_element "1" wfm) diff --git a/data/property/cnes/CNE_01700.pp b/data/property/cnes/CNE_01700.pp new file mode 100644 index 0000000..b28585d --- /dev/null +++ b/data/property/cnes/CNE_01700.pp @@ -0,0 +1,3 @@ +The signal $x_re.IDENTIFIER (declared in $x_re.FILE, line $x_re.LINE, column +$x_re.COLUMN) is made to indicate the rising edge of another signal. CNE_01700 +indicates such signals should have names ending in "_re". diff --git a/data/property/cnes/CNE_01700.pro b/data/property/cnes/CNE_01700.pro index d254ad1..bc83c8c 100644 --- a/data/property/cnes/CNE_01700.pro +++ b/data/property/cnes/CNE_01700.pro @@ -96,7 +96,7 @@ (is_read_element _ rst1) (EX (and - (not (has_option "COND_WAS_TRUE")) + (not (has_option "cond_was_true")) (kind "if") (is_read_structure "(??)") (or @@ -106,7 +106,7 @@ (is_read_element "1" clk1) (EX (and - (has_option "COND_WAS_TRUE") + (has_option "cond_was_true") (does_not_reach_parent_before (and (expr_writes x_r1) diff --git a/data/property/cnes/CNE_01800.pp b/data/property/cnes/CNE_01800.pp new file mode 100644 index 0000000..0631fe6 --- /dev/null +++ b/data/property/cnes/CNE_01800.pp @@ -0,0 +1,3 @@ +The signal $x_fe.IDENTIFIER (declared in $x_fe.FILE, line $x_fe.LINE, column +$x_fe.COLUMN) is made to indicate the falling edge of another signal. CNE_01800 +indicates such signals should have names ending in "_fe". diff --git a/data/property/cnes/CNE_01800.pro b/data/property/cnes/CNE_01800.pro index 0666e8f..78e1094 100644 --- a/data/property/cnes/CNE_01800.pro +++ b/data/property/cnes/CNE_01800.pro @@ -96,7 +96,7 @@ (is_read_element _ rst1) (EX (and - (not (has_option "COND_WAS_TRUE")) + (not (has_option "cond_was_true")) (kind "if") (is_read_structure "(??)") (or @@ -106,7 +106,7 @@ (is_read_element "1" clk1) (EX (and - (has_option "COND_WAS_TRUE") + (has_option "cond_was_true") (does_not_reach_parent_before (and (expr_writes x_r1) diff --git a/data/property/cnes/CNE_01900.pp b/data/property/cnes/CNE_01900.pp new file mode 100644 index 0000000..1813358 --- /dev/null +++ b/data/property/cnes/CNE_01900.pp @@ -0,0 +1,3 @@ +The signal $x_r.IDENTIFIER (declared in $x_r.FILE, line $x_r.LINE, column +$x_r.COLUMN) is the result of another signal delayed using a flip-flop. +CNE_01900 indicates such signals should have names ending in "_r[0-9]*". diff --git a/data/property/cnes/CNE_01900.pro b/data/property/cnes/CNE_01900.pro new file mode 100644 index 0000000..0e11415 --- /dev/null +++ b/data/property/cnes/CNE_01900.pro @@ -0,0 +1,102 @@ +(tag_existing + ( + (x_r waveform CNE_01900_HAS_BAD_NAME) + ) + (and + (not (string_matches [identifier [is_waveform_of x_r]] ".*_r[0-9]*")) + (exists x waveform + (exists ps1 process + (and + (is_accessed_by x_r ps1) + (is_accessed_by x ps1) + (is_explicit_process ps1) + (exists clk1 waveform + (and + (is_in_sensitivity_list clk1 ps1) + (or + (CTL_verifies ps1 + (AF + (and + (kind "if") + (is_read_structure "(??)") + (or + (is_read_element "0" "falling_edge") + (is_read_element "0" "rising_edge") + ) + (is_read_element "1" clk1) + (EX + (and + (has_option "cond_was_true") + (does_not_reach_parent_before + (and + (expr_writes x_r) + (is_read_structure "?") + (is_read_element "0" x) + (AX + (not + (EF + (expr_writes x_r) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + (exists rst1 waveform + (and + (is_in_sensitivity_list rst1 ps1) + (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") + (is_read_structure "(??)") + (or + (is_read_element "0" "falling_edge") + (is_read_element "0" "rising_edge") + ) + (is_read_element "1" clk1) + (EX + (and + (has_option "cond_was_true") + (does_not_reach_parent_before + (and + (expr_writes x_r) + (is_read_structure "?") + (is_read_element "0" x) + (AX + (not + (EF + (expr_writes x_r) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/cnes/CNE_05100.pp b/data/property/cnes/CNE_05100.pp new file mode 100644 index 0000000..e120de2 --- /dev/null +++ b/data/property/cnes/CNE_05100.pp @@ -0,0 +1,3 @@ +The signal $wfm.IDENTIFIER (declared in $wfm.FILE, line $wfm.LINE, column +$wfm.COLUMN) is the output of a single process multiplexor, as defined by +CNE_05100. diff --git a/data/property/cnes/STD_04800.pp b/data/property/cnes/STD_04800.pp new file mode 100644 index 0000000..deb0baf --- /dev/null +++ b/data/property/cnes/STD_04800.pp @@ -0,0 +1,3 @@ +The signal $wfm.IDENTIFIER (declared in $wfm.FILE, line $wfm.LINE, column +$wfm.COLUMN) is tested with both the rising_edge and the falling_edge functions. +This goes against STD_04800. |