summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornsensfel <SpamShield0@noot-noot.org>2018-05-31 16:52:12 +0200
committernsensfel <SpamShield0@noot-noot.org>2018-05-31 16:52:12 +0200
commit9f784e5c285cdd2631b52a4299eeb193593e6c21 (patch)
treec87e912bf03d2c4eb907cd91bca11c0297d865a7
parente520f8b10fbb7b39c563bf626c8d7945a0b424c0 (diff)
downloadghdl2hastabel-9f784e5c285cdd2631b52a4299eeb193593e6c21.zip
ghdl2hastabel-9f784e5c285cdd2631b52a4299eeb193593e6c21.tar.bz2
Adds Tabellion's old properties.
-rw-r--r--property/CNE_00100.pro59
-rw-r--r--property/CNE_01100.pro21
-rw-r--r--property/CNE_01200.pro14
-rw-r--r--property/CNE_01400.pro8
-rw-r--r--property/CNE_01700.pro75
-rw-r--r--property/CNE_01800.pro203
-rw-r--r--property/CNE_01900.pro162
-rw-r--r--property/CNE_02100.pro12
-rw-r--r--property/CNE_02600.pro6
-rw-r--r--property/CNE_04500.pro273
-rw-r--r--property/CNE_05100.pro64
-rw-r--r--property/STD_04800.pro101
-rw-r--r--property/async_reset_flip_flop.pro81
-rw-r--r--property/combinational_processes.pro29
-rw-r--r--property/flip_flop.pro19
-rw-r--r--property/incrementer.pro16
-rw-r--r--property/likely_a_clock.pro56
-rw-r--r--property/simple_flip_flop.pro69
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)
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+)