Fixes is_accessed_by. CNE_01700 is not working.

The BCE has been updated to include a group of items that should be
tagged by the CNE_01700 rule. However, it's not happening. I don't see
anything wrong with the way the CNE_01700 rule is written and a quick
overview of the generated model would lead me to conclude that it indeed
should tag something. Likely there are still issues with the way
properties are turned into Kodkod formulas.

1 files changed, 38 insertions, 38 deletions

diff --git a/data/property/cnes/CNE_01700.pro b/data/property/cnes/CNE_01700.pro
index a0cb792..d254ad1 100644
--- a/data/property/cnes/CNE_01700.pro
+++ b/data/property/cnes/CNE_01700.pro
@@ -3,10 +3,46 @@
       (x_re waveform CNE_01700_HAS_BAD_NAME)
    )
    (and
-      (not (string_matches [identifier x_re] ".*_re"))
+      (not (string_matches [identifier [is_waveform_of x_re]] ".*_re"))
       (exists x waveform
          (exists x_r1 waveform
             (and
+               (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
+                                 (and
+                                    (is_read_structure "(?(??)?)")
+                                    (is_read_element "1" "not")
+                                    (is_read_element "2" x_r1)
+                                    (is_read_element "3" x)
+                                 )
+                                 (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)
+                                    )
+                                 )
+                              )
+                           )
+                        )
+                     )
+                  )
+               )
                (exists ps1 process
                   (and
                      (is_accessed_by x_r1 ps1)
@@ -28,7 +64,7 @@
                                        (is_read_element "1" clk1)
                                        (EX
                                           (and
-                                             (has_option "COND_WAS_TRUE")
+                                             (has_option "cond_was_true")
                                              (does_not_reach_parent_before
                                                 (and
                                                    (expr_writes x_r1)
@@ -99,42 +135,6 @@
                      )
                   )
                )
-               (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
-                                 (and
-                                    (is_read_structure "(?(??)?)")
-                                    (is_read_element "1" "not")
-                                    (is_read_element "2" x_r1)
-                                    (is_read_element "3" x)
-                                 )
-                                 (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)
-                                    )
-                                 )
-                              )
-                           )
-                        )
-                     )
-                  )
-               )
             )
          )
       )