| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'property')
| -rw-r--r-- | property/CNE_00100.pro | 59 | ||||
| -rw-r--r-- | property/CNE_01100.pro | 21 | ||||
| -rw-r--r-- | property/CNE_01200.pro | 14 | ||||
| -rw-r--r-- | property/CNE_01400.pro | 8 | ||||
| -rw-r--r-- | property/CNE_01700.pro | 75 | ||||
| -rw-r--r-- | property/CNE_01800.pro | 203 | ||||
| -rw-r--r-- | property/CNE_01900.pro | 162 | ||||
| -rw-r--r-- | property/CNE_02100.pro | 12 | ||||
| -rw-r--r-- | property/CNE_02600.pro | 6 | ||||
| -rw-r--r-- | property/CNE_04500.pro | 273 | ||||
| -rw-r--r-- | property/CNE_05100.pro | 64 | ||||
| -rw-r--r-- | property/STD_04800.pro | 101 | ||||
| -rw-r--r-- | property/async_reset_flip_flop.pro | 81 | ||||
| -rw-r--r-- | property/combinational_processes.pro | 29 | ||||
| -rw-r--r-- | property/flip_flop.pro | 19 | ||||
| -rw-r--r-- | property/incrementer.pro | 16 | ||||
| -rw-r--r-- | property/likely_a_clock.pro | 56 | ||||
| -rw-r--r-- | property/simple_flip_flop.pro | 69 |
18 files changed, 1268 insertions, 0 deletions
diff --git a/property/CNE_00100.pro b/property/CNE_00100.pro new file mode 100644 index 0000000..1078938 --- /dev/null +++ b/property/CNE_00100.pro @@ -0,0 +1,59 @@ +(seek + ( + (wfm waveform) + ) + (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. +) diff --git a/property/CNE_01100.pro b/property/CNE_01100.pro new file mode 100644 index 0000000..08e4bb4 --- /dev/null +++ b/property/CNE_01100.pro @@ -0,0 +1,21 @@ +(seek + ( + (pt port) + ) + (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/property/CNE_01200.pro b/property/CNE_01200.pro new file mode 100644 index 0000000..1497bd7 --- /dev/null +++ b/property/CNE_01200.pro @@ -0,0 +1,14 @@ +(seek + ( + (ps process) + ) + (and + (is_explicit_process ps) + (not + (and + (has_label ps) + (string_matches [label ps] "^P_.*") + ) + ) + ) +) diff --git a/property/CNE_01400.pro b/property/CNE_01400.pro new file mode 100644 index 0000000..715f7d2 --- /dev/null +++ b/property/CNE_01400.pro @@ -0,0 +1,8 @@ +(seek + ( + (gc generic) + ) + (not + (string_matches [identifier gc] "^g_.*") + ) +) diff --git a/property/CNE_01700.pro b/property/CNE_01700.pro new file mode 100644 index 0000000..83a80a4 --- /dev/null +++ b/property/CNE_01700.pro @@ -0,0 +1,75 @@ +#require "flip_flop" + +(seek + ( + (x_re waveform) + ) + (and + (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 + (not (eq x x_re)) +;; 'x_r1' is 'x' delayed by a flipflop +(exists x_r1 waveform + (and + (not (eq x_r1 x_re)) + (not (eq x_r1 x)) +;; 'ps2' is the process describing 'x_re' as the rising edge +(exists ps2 process + (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 + (expr_writes x_re) + (is_read_element "0" "and") + (or + ;; x_re <= (not x_r1) and x + (and + (is_read_structure "(?(??)?)") + (is_read_element "1" "not") + (is_read_element "2" x_r1) + (is_read_element "3" x) + ) + ;; x_re <= x and (not x_r1) + (and + (is_read_structure "(??(??))") + (is_read_element "1" x) + (is_read_element "2" "not") + (is_read_element "3" x_r1) + ) + ) + (AX + (not + (EF + (expr_writes x_r1) + ) + ) + ) + ) + ) + ) + ) +) +;; 'ps1' is the process describing 'x_r1' as a flipflop. +(exists ps1 process + (and + (is_accessed_by x_r1 ps1) + (is_accessed_by x ps1) + (is_explicit_process ps1) + (flip_flop x_r1 _ ps1) + (CTL_verifies ps1 + (EF + (and + (expr_writes x_r1) + (is_read_structure "?") + (is_read_element "0" x) + ) + ) + ) + ) +) +)))))) diff --git a/property/CNE_01800.pro b/property/CNE_01800.pro new file mode 100644 index 0000000..d358224 --- /dev/null +++ b/property/CNE_01800.pro @@ -0,0 +1,203 @@ +(seek + ( + (x_fe waveform) + ) + (and + (not (string_matches [identifier [is_waveform_of x_fe]] ".*_fe")) + (exists x waveform + (and + (not (eq x x_fe)) + (exists x_r1 waveform + (and + (not (eq x_r1 x_fe)) + (not (eq x_r1 x)) + (exists ps2 process + (and + (is_in_sensitivity_list x_r1 ps2) + (is_in_sensitivity_list x ps2) + (is_accessed_by x_fe ps2) + (CTL_verifies ps2 + (AF + (and + (expr_writes x_fe) + (is_read_element "0" "and") + (or + (and + (is_read_structure "(?(??)?)") + (is_read_element "1" "not") + (is_read_element "2" x) + (is_read_element "3" x_r1) + ) + (and + (is_read_structure "(??(??))") + (is_read_element "1" x_r1) + (is_read_element "2" "not") + (is_read_element "3" 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") + (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) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + (exists rst1 waveform + (and + (is_in_sensitivity_list rst1 ps1) + (not (eq rst1 x_fe)) + (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/property/CNE_01900.pro b/property/CNE_01900.pro new file mode 100644 index 0000000..e889232 --- /dev/null +++ b/property/CNE_01900.pro @@ -0,0 +1,162 @@ +(seek + ( + (x_r waveform) + ) + (and + (not (string_matches [identifier [is_waveform_of x_r]] ".*_r[0-9]*")) + (exists x waveform + (and + (not (eq x x_r)) + (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) + (not (eq clk1 x_r)) + (not (eq clk1 x)) + (or + (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 + (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) + (not (eq rst1 x_r)) + (not (eq rst1 x)) + (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_r) + (is_read_structure "?") + (is_read_element "0" x) + (AX + (not + (EF + (expr_writes x_r) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/property/CNE_02100.pro b/property/CNE_02100.pro new file mode 100644 index 0000000..b60f48e --- /dev/null +++ b/property/CNE_02100.pro @@ -0,0 +1,12 @@ +(seek + ( + (arch architecture) + ) + (not + (or + (identifier arch "Behavioral") + (identifier arch "RTL") + (identifier arch "Simulation") + ) + ) +) diff --git a/property/CNE_02600.pro b/property/CNE_02600.pro new file mode 100644 index 0000000..86cc7a5 --- /dev/null +++ b/property/CNE_02600.pro @@ -0,0 +1,6 @@ +(seek + ( + (sl signal) + ) + (string_matches [identifier sl] ".{21,}") +) diff --git a/property/CNE_04500.pro b/property/CNE_04500.pro new file mode 100644 index 0000000..6c3867a --- /dev/null +++ b/property/CNE_04500.pro @@ -0,0 +1,273 @@ +(seek + ( + ;; waveform initialized using a reset. + (i_wfm waveform) + ;; waveform not initialized using a reset. + (ni_wfm waveform) + (ps 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) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/property/CNE_05100.pro b/property/CNE_05100.pro new file mode 100644 index 0000000..c8184b3 --- /dev/null +++ b/property/CNE_05100.pro @@ -0,0 +1,64 @@ +(seek + ( + (wfm waveform) + ) + (exists ps process + (and + (is_explicit_process ps) + (forall sl1 waveform + (and + (CTL_verifies ps + (implies + (EF (expr_writes sl1)) + (AF (expr_writes sl1)) + ) + ) + (implies + (exists target waveform + (CTL_verifies ps + (EF + (and + (is_read_element _ sl1) + (not + (and + (expr_writes target) + (AX + (AF + (expr_writes target) + ) + ) + ) + ) + ) + ) + ) + ) + (is_in_sensitivity_list sl1 ps) + ) + ) + ) + (CTL_verifies ps + (AF + (and + (or + (kind "case") + (kind "if") + ) + (does_not_reach_parent_before + (and + (expr_writes wfm) + (AX + (not + (EF + (expr_writes wfm) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/property/STD_04800.pro b/property/STD_04800.pro new file mode 100644 index 0000000..0b46d8b --- /dev/null +++ b/property/STD_04800.pro @@ -0,0 +1,101 @@ +(seek + ( + (wfm waveform) + ) + (and + (exists ps_re process + (CTL_verifies ps_re + (EF + (or + (and + (is_read_structure "(??)") + (is_read_element "0" "rising_edge") + (is_read_element "1" wfm) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" wfm) + (is_read_element "3" "=") + (or + (and + (is_read_element "4" wfm) + (is_read_element "5" "'1'") + ) + (and + (is_read_element "4" "'1'") + (is_read_element "5" wfm) + ) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (and + (is_read_element "2" wfm) + (is_read_element "3" "'1'") + ) + (and + (is_read_element "2" "'1'") + (is_read_element "3" wfm) + ) + ) + (is_read_element "4" "event") + (is_read_element "5" wfm) + ) + ) + ) + ) + ) + (exists ps_fe process + (CTL_verifies ps_fe + (EF + (or + (and + (is_read_structure "(??)") + (is_read_element "0" "falling_edge") + (is_read_element "1" wfm) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" wfm) + (is_read_element "3" "=") + (or + (and + (is_read_element "4" wfm) + (is_read_element "5" "'0'") + ) + (and + (is_read_element "4" "'0'") + (is_read_element "5" wfm) + ) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (and + (is_read_element "2" wfm) + (is_read_element "3" "'0'") + ) + (and + (is_read_element "2" "'0'") + (is_read_element "3" wfm) + ) + ) + (is_read_element "4" "event") + (is_read_element "5" wfm) + ) + ) + ) + ) + ) + ) +) diff --git a/property/async_reset_flip_flop.pro b/property/async_reset_flip_flop.pro new file mode 100644 index 0000000..729a224 --- /dev/null +++ b/property/async_reset_flip_flop.pro @@ -0,0 +1,81 @@ +(seek + ( + (reg waveform) + (clk waveform) + (rst waveform) + (ps process) + ) + (and + (not (eq clk reg)) + (not (eq rst reg)) + (not (eq rst clk)) + (is_explicit_process ps) + (is_in_sensitivity_list clk ps) + (is_in_sensitivity_list rst ps) + (CTL_verifies ps + (AU + (not (expr_writes reg)) + (and + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (is_read_element _ rst) + (EX + (and + (not (has_option "cond_was_true")) + (or + (and + (is_read_structure "(??)") + (or + (is_read_element "0" "falling_edge") + (is_read_element "0" "rising_edge") + ) + (is_read_element "1" clk) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" clk) + (is_read_element "3" "=") + (or + (is_read_element "4" clk) + (is_read_element "5" clk) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (is_read_element "2" clk) + (is_read_element "3" clk) + ) + (is_read_element "4" "event") + (is_read_element "5" clk) + ) + ) + (EX + (and + (has_option "COND_WAS_TRUE") + (does_not_reach_parent_before + (and + (expr_writes reg) + (AX + (not + (EF + (expr_writes reg) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/property/combinational_processes.pro b/property/combinational_processes.pro new file mode 100644 index 0000000..d4068ab --- /dev/null +++ b/property/combinational_processes.pro @@ -0,0 +1,29 @@ +(seek + ( + (ps process) + ) + (forall sl1 waveform + (and + (implies + ;; If a signal is read, + (exists target waveform + (CTL_verifies ps + (EF + (is_read_element _ sl1) + ) + ) + ) + ;; Then it must be in the sensitivity list. + (is_in_sensitivity_list sl1 ps) + ) + (CTL_verifies ps + (implies + ;; If a signal is somehow assigned by this process, + (EF (expr_writes sl1)) + ;; Then it is assigned at every execution of the process. + (AF (expr_writes sl1)) + ) + ) + ) + ) +) diff --git a/property/flip_flop.pro b/property/flip_flop.pro new file mode 100644 index 0000000..97baa15 --- /dev/null +++ b/property/flip_flop.pro @@ -0,0 +1,19 @@ +#require "simple_flip_flop" +#require "async_reset_flip_flop" + +(seek + ( + (reg waveform) + (clk waveform) + (ps process) + ) + (and + (not (eq reg clk)) +;; (is_accessed_by reg ps) +;; (is_accessed_by clk ps) + (or + (simple_flip_flop reg clk ps) + (async_reset_flip_flop reg clk _ ps) + ) + ) +) diff --git a/property/incrementer.pro b/property/incrementer.pro new file mode 100644 index 0000000..c9d66db --- /dev/null +++ b/property/incrementer.pro @@ -0,0 +1,16 @@ +(seek + ( + (wf waveform) + (ps process) + ) + (CTL_verifies ps + (EF + (and + (is_read_structure "(???)") + (is_read_element "0" "+") + (is_read_element _ wf) + (is_read_element _ "L") + ) + ) + ) +) diff --git a/property/likely_a_clock.pro b/property/likely_a_clock.pro new file mode 100644 index 0000000..d5acaed --- /dev/null +++ b/property/likely_a_clock.pro @@ -0,0 +1,56 @@ +(seek + ( + (clock port) + ) + (exists wf waveform + (and + (is_waveform_of wf clock) + (exists ps process + (and + (is_accessed_by wf ps) + (is_in_sensitivity_list wf ps) + (CTL_verifies ps + (EF + (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" wf) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" wf) + (is_read_element "3" "=") + (or + (is_read_element "4" wf) + (is_read_element "5" wf) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (is_read_element "2" wf) + (is_read_element "3" wf) + ) + (is_read_element "4" "event") + (is_read_element "5" wf) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/property/simple_flip_flop.pro b/property/simple_flip_flop.pro new file mode 100644 index 0000000..53b8f03 --- /dev/null +++ b/property/simple_flip_flop.pro @@ -0,0 +1,69 @@ +(seek + ( + (reg waveform) + (clk waveform) + (ps process) + ) + (and + (not (eq clk reg)) + (is_explicit_process ps) + (is_in_sensitivity_list clk ps) + (CTL_verifies ps + (AU + (not (expr_writes reg)) + (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" clk) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" clk) + (is_read_element "3" "=") + (or + (is_read_element "4" clk) + (is_read_element "5" clk) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (is_read_element "2" clk) + (is_read_element "3" clk) + ) + (is_read_element "4" "event") + (is_read_element "5" clk) + ) + ) + (EX + (and + (has_option "cond_was_true") + (does_not_reach_parent_before + (and + (expr_writes reg) + (AX + (not + (EF + (expr_writes reg) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) |