| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | data/property/cnes/CNE_04500.pp | 6 | ||||
| -rw-r--r-- | data/property/cnes/CNE_04500.pro | 273 |
2 files changed, 279 insertions, 0 deletions
diff --git a/data/property/cnes/CNE_04500.pp b/data/property/cnes/CNE_04500.pp new file mode 100644 index 0000000..0a2ec8e --- /dev/null +++ b/data/property/cnes/CNE_04500.pp @@ -0,0 +1,6 @@ +The process $ps.LABEL$ (declared in $ps.FILE$, line $ps.LINE$, column +$ps.COLUMN$) assigns values to a both reset-initialized waveform, +$i_wfm.IDENTIFIER$ (declared in $i_wfm.FILE$, line $i_wfm.LINE$, column +$i_wfm.COLUMN$), and waveform not reset-initialized $ni_wfm.IDENTIFIER$ +(declared in $ni_wfm.FILE$, line $ni_wfm.LINE$, column $ni_wfm.COLUMN$), and +waveform not reset-initialized. This goes against CNE_04500. diff --git a/data/property/cnes/CNE_04500.pro b/data/property/cnes/CNE_04500.pro new file mode 100644 index 0000000..383aec0 --- /dev/null +++ b/data/property/cnes/CNE_04500.pro @@ -0,0 +1,273 @@ +(tag_existing + ( + ;; waveform initialized using a reset. + (i_wfm waveform CNE_04500_INITIALIZED_SIGNAL) + ;; waveform not initialized using a reset. + (ni_wfm waveform CNE_04500_NON_INITIALIZED_SIGNAL) + (ps process CNE_04500_BAD_PROCESS) + ) + (and + (is_accessed_by i_wfm ps) + (is_accessed_by ni_wfm ps) + (not (eq ni_wfm i_wfm)) + (exists clk1 waveform + (and + (is_accessed_by clk1 ps) + (not (eq clk1 i_wfm)) + (not (eq clk1 ni_wfm)) + (exists rst1 waveform + (and + (is_accessed_by rst1 ps) + (not (eq rst1 i_wfm)) + (not (eq rst1 ni_wfm)) + (not (eq rst1 clk1)) + (or + ;; With a synchronous reset. + (and + (not (is_in_sensitivity_list rst1 ps)) + (CTL_verifies ps + (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 + (and + (has_option "cond_was_true") + (does_not_reach_parent_before + (and + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (is_read_element _ rst1) + (EX + (and + (or + (has_option "cond_was_true") + (has_option "cond_was_false") + ) + (does_not_reach_parent_before + (and + (expr_writes i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (not + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + (EX + (and + (or + (has_option "cond_was_true") + (has_option "cond_was_false") + ) + (does_not_reach_parent_before + (and + (expr_writes i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ;; With an asynchronous reset. + (and + (is_in_sensitivity_list rst1 ps) + (CTL_verifies ps + (AF + (and + ;; if (rst = _) + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (is_read_element _ rst1) + (EX + (and + ;; then + (has_option "cond_was_true") + (does_not_reach_parent_before + (and + (expr_writes i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (not + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + (EX + (and + ;; else + (not (has_option "cond_was_true")) + (does_not_reach_parent_before + (and + ;; if (edge(clk)) + (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 i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) |