Adds Tabellion's old properties.

1 files changed, 29 insertions, 0 deletions

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))
+            )
+         )
+      )
+   )
+)