Adds "real" property: Find combinational processes

1 files changed, 37 insertions, 0 deletions

diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro
new file mode 100644
index 0000000..9300672
--- /dev/null
+++ b/data/property/combinational_processes.pro
@@ -0,0 +1,37 @@
+(tag_existing
+   (
+      (ps process STRUCT_COMBINATIONAL_PROCESS)
+   )
+   (forall sl1 signal
+      (and
+         (CTL_verifies ps
+            (implies
+               (EF (expr_writes sl1))
+               (AF (expr_writes sl1))
+            )
+         )
+         (implies
+            (exists target signal
+               (CTL_verifies ps
+                  (EF
+                     (and
+                        (expr_reads sl1)
+                        (not
+                           (and
+                              (expr_writes target)
+                              (AX
+                                 (AF
+                                    (expr_writes target)
+                                 )
+                              )
+                           )
+                        )
+                     )
+                  )
+               )
+            )
+            (is_in_sensitivity_list ps sl1)
+         )
+      )
+   )
+)