Updates Tests, fixes 2 properties & inferred/*.mod

3 files changed, 26 insertions, 175 deletions

diff --git a/data/property/CNE_01100.pro b/data/property/CNE_01100.pro
index 6ed2cff..ad94747 100644
--- a/data/property/CNE_01100.pro
+++ b/data/property/CNE_01100.pro
@@ -2,28 +2,19 @@
    (
       (pt port CNE_01100_BAD_NAME)
    )
-   (exists pt2 port
-      (and
-;; Goes into infinity:
-;;       (has_mode pt2 _)
-;;       (has_mode pt2 "in")
-;; Fixes all:
-         (eq pt2 pt)
-         (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")
-               )
-            )
+   (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/data/property/CNE_01700.pro b/data/property/CNE_01700.pro
index 7452a3c..2327afc 100644
--- a/data/property/CNE_01700.pro
+++ b/data/property/CNE_01700.pro
@@ -1,9 +1,11 @@
+#require "flip_flop"
+
 (tag_existing
    (
       (x_re waveform CNE_01700_HAS_BAD_NAME)
    )
    (and
-      (not (string_matches [identifier [is_waveform_of x_re]] ".*_re"))
+      (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
@@ -58,159 +60,16 @@
       (is_accessed_by x_r1 ps1)
       (is_accessed_by x ps1)
       (is_explicit_process ps1)
-;; 'clk1' is the clock controlling that flipflop
-(exists clk1 waveform
-   (and
-      (is_in_sensitivity_list clk1 ps1)
-      (not (eq clk1 x_re))
-      (not (eq clk1 x))
-      (not (eq clk1 x_r1))
-      (or
-;; 'ps1' could be a simple flipflop
-(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
+      (_flip_flop x_r1 _ ps1)
+      (CTL_verifies ps1
+         (EF
             (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)
-                           )
-                        )
-                     )
-                  )
-               )
+               (expr_writes x_r1)
+               (is_read_structure "?")
+               (is_read_element "0" x)
             )
          )
       )
    )
 )
-;; 'ps1' could be a flipflop with reset
-;; 'rst1' is that reset signal
-(exists rst1 waveform
-   (and
-      (is_in_sensitivity_list rst1 ps1)
-      (not (eq rst1 x_re))
-      (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/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro
index b054c7f..09ef98b 100644
--- a/data/property/simple_flip_flop.pro
+++ b/data/property/simple_flip_flop.pro
@@ -9,7 +9,8 @@
       (is_explicit_process ps)
       (is_in_sensitivity_list clk ps)
       (CTL_verifies ps
-         (AF
+         (AU
+            (not (expr_writes reg))
             (and
                (kind "if")
                (or
@@ -46,7 +47,7 @@
                )
                (EX
                   (and
-                     (has_option "COND_WAS_TRUE")
+                     (has_option "cond_was_true")
                      (does_not_reach_parent_before
                         (and
                            (expr_writes reg)