1 files changed, 75 insertions, 0 deletions
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)
+            )
+         )
+      )
+   )
+)
+))))))