| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data/property')
| -rw-r--r-- | data/property/cnes/CNE_01700.pro | 127 |
1 files changed, 66 insertions, 61 deletions
diff --git a/data/property/cnes/CNE_01700.pro b/data/property/cnes/CNE_01700.pro index 6b77fa1..a0cb792 100644 --- a/data/property/cnes/CNE_01700.pro +++ b/data/property/cnes/CNE_01700.pro @@ -7,34 +7,38 @@ (exists x waveform (exists x_r1 waveform (and - (exists clk1 waveform - (exists ps1 process - (and - (is_explicit_process ps1) - (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_r1) - (is_read_structure "?") - (is_read_element "0" x) - (AX - (not - (EF - (expr_writes x_r1) + (exists ps1 process + (and + (is_accessed_by x_r1 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_r1) + (is_read_structure "?") + (is_read_element "0" x) + (AX + (not + (EF + (expr_writes x_r1) + ) ) ) ) @@ -44,39 +48,39 @@ ) ) ) - ) - (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_r1) - (is_read_structure "?") - (is_read_element "0" x) - (AX - (not - (EF - (expr_writes x_r1) + (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_r1) + (is_read_structure "?") + (is_read_element "0" x) + (AX + (not + (EF + (expr_writes x_r1) + ) ) ) ) @@ -99,6 +103,7 @@ (and (is_in_sensitivity_list x_r1 ps2) (is_in_sensitivity_list x ps2) + (is_accessed_by x_re ps2) (CTL_verifies ps2 (AF (and |