From 9f784e5c285cdd2631b52a4299eeb193593e6c21 Mon Sep 17 00:00:00 2001
From: nsensfel <SpamShield0@noot-noot.org>
Date: Thu, 31 May 2018 16:52:12 +0200
Subject: Adds Tabellion's old properties.

---
 property/STD_04800.pro | 101 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 101 insertions(+)
 create mode 100644 property/STD_04800.pro

(limited to 'property/STD_04800.pro')

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)
+                  )
+               )
+            )
+         )
+      )
+   )
+)
-- 
cgit v1.2.3-70-g09d2