Reduces the scalability issue.

It seems to take very long to find solutions for
simple_flip_flop_instance, but at least it no longer gives up right
away.

3 files changed, 108 insertions, 6 deletions

diff --git a/data/level/instances.lvl b/data/level/instances.lvl
index 5fdb42b..ad6e93f 100644
--- a/data/level/instances.lvl
+++ b/data/level/instances.lvl
@@ -3,7 +3,8 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(add_type instance)
+(add_type wfm_instance)
+(add_type ps_instance)
 
 ;; Redundancies
 (add_type entity)
@@ -13,10 +14,10 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(add_predicate is_waveform_instance instance waveform)
-(add_predicate is_visible_in instance waveform entity)
+(add_predicate is_wfm_instance_of wfm_instance waveform)
+(add_predicate is_visible_in wfm_instance entity)
 
-(add_predicate is_process_instance instance process)
-(add_predicate is_visible_in instance process entity)
+(add_predicate is_ps_instance_of ps_instance process)
+(add_predicate is_visible_in ps_instance entity)
 
-(add_predicate process_instance_maps instance process instance waveform waveform)
+(add_predicate process_instance_maps ps_instance wfm_instance waveform)
diff --git a/data/property/simple_flip_flop_instance.pp b/data/property/simple_flip_flop_instance.pp
new file mode 100644
index 0000000..b460eec
--- /dev/null
+++ b/data/property/simple_flip_flop_instance.pp
@@ -0,0 +1,6 @@
+The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$,
+line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the
+process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$),
+controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$,
+c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$,
+l. $reg.LINE$, c. $reg.COLUMN$).
diff --git a/data/property/simple_flip_flop_instance.pro b/data/property/simple_flip_flop_instance.pro
new file mode 100644
index 0000000..a3881aa
--- /dev/null
+++ b/data/property/simple_flip_flop_instance.pro
@@ -0,0 +1,95 @@
+(tag_existing
+   (
+      (ent entity STRUCT_ENTITY)
+      (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT)
+      (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK)
+      (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS)
+   )
+   (and
+      (is_explicit_process ps)
+;; debt: ))
+;; Get ps instance
+(exists i_ps ps_instance
+   (and
+      (is_visible_in i_ps ent)
+      (is_ps_instance_of i_ps ps)
+;; debt: )) ))
+;; Get a local waveform matching a clk instance
+(exists i_clk wfm_instance
+   (and
+      (process_instance_maps i_ps i_clk _)
+;;      (is_visible_in i_clk ent)
+      (is_wfm_instance_of i_clk clk)
+      (exists local_clk waveform
+         (and
+            (process_instance_maps i_ps i_clk local_clk)
+            (is_in_sensitivity_list local_clk ps)
+;; debt: )))) ))))
+;; Get a local waveform matching a reg instance
+(exists i_reg wfm_instance
+   (and
+      (process_instance_maps i_ps i_reg _)
+;;      (is_visible_in i_reg ent)
+      (is_wfm_instance_of i_reg reg)
+      (exists local_reg waveform
+         (and
+            (process_instance_maps i_ps i_reg local_reg)
+;; debt: )))) ))))))))
+;; Analyze ps using the local waveforms
+(CTL_verifies ps
+   (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" local_clk)
+            )
+            (and
+               (is_read_structure "(?(??)(???))")
+               (is_read_element "0" "and")
+               (is_read_element "1" "event")
+               (is_read_element "2" local_clk)
+               (is_read_element "3" "=")
+               (or
+                  (is_read_element "4" local_clk)
+                  (is_read_element "5" local_clk)
+               )
+            )
+            (and
+               (is_read_structure "(?(???)(??))")
+               (is_read_element "0" "and")
+               (is_read_element "1" "=")
+               (or
+                  (is_read_element "2" local_clk)
+                  (is_read_element "3" local_clk)
+               )
+               (is_read_element "4" "event")
+               (is_read_element "5" local_clk)
+            )
+         )
+         (EX
+            (and
+               (has_option "COND_WAS_TRUE")
+               (does_not_reach_parent_before
+                  (and
+                     (expr_writes local_reg)
+                     (AX
+                        (not
+                           (EF
+                              (expr_writes local_reg)
+                           )
+                        )
+                     )
+                  )
+               )
+            )
+         )
+      )
+   )
+)
+))))))))))))