Merge branch 'instance-calculator'

6 files changed, 153 insertions, 0 deletions

diff --git a/data/level/instances.lvl b/data/level/instances.lvl
new file mode 100644
index 0000000..ad6e93f
--- /dev/null
+++ b/data/level/instances.lvl
@@ -0,0 +1,23 @@
+;; Instances
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(add_type wfm_instance)
+(add_type ps_instance)
+
+;; Redundancies
+(add_type entity)
+(add_type process)
+(add_type waveform)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(add_predicate is_wfm_instance_of wfm_instance waveform)
+(add_predicate is_visible_in wfm_instance entity)
+
+(add_predicate is_ps_instance_of ps_instance process)
+(add_predicate is_visible_in ps_instance entity)
+
+(add_predicate process_instance_maps ps_instance wfm_instance waveform)
diff --git a/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro
index e1621c1..b054c7f 100644
--- a/data/property/simple_flip_flop.pro
+++ b/data/property/simple_flip_flop.pro
@@ -5,6 +5,7 @@
       (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS)
    )
    (and
+      (not (eq clk reg))
       (is_explicit_process ps)
       (is_in_sensitivity_list clk ps)
       (CTL_verifies ps
diff --git a/data/property/test-case/fast.pp b/data/property/test-case/fast.pp
new file mode 100644
index 0000000..b460eec
--- /dev/null
+++ b/data/property/test-case/fast.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/test-case/fast.pro b/data/property/test-case/fast.pro
new file mode 100644
index 0000000..10bc135
--- /dev/null
+++ b/data/property/test-case/fast.pro
@@ -0,0 +1,57 @@
+(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
+      (not (eq reg clk))
+      (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
+                                          ;; using local_clk or local_reg here makes the property take forever to verify....
+                                          (kind "if")
+                                       )
+                                    )
+                                 )
+                              )
+                           )
+                        )
+                     )
+                  )
+               )
+            )
+         )
+      )
+   )
+)
diff --git a/data/property/test-case/slow.pp b/data/property/test-case/slow.pp
new file mode 100644
index 0000000..b460eec
--- /dev/null
+++ b/data/property/test-case/slow.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/test-case/slow.pro b/data/property/test-case/slow.pro
new file mode 100644
index 0000000..2566a6f
--- /dev/null
+++ b/data/property/test-case/slow.pro
@@ -0,0 +1,60 @@
+(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
+      (not (eq reg clk))
+      (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
+                                          ;; using local_clk or local_reg here makes the property take forever to verify....
+                                          (and
+                                             (kind "if")
+                                             (is_read_element "1" local_clk)
+                                          )
+                                       )
+                                    )
+                                 )
+                              )
+                           )
+                        )
+                     )
+                  )
+               )
+            )
+         )
+      )
+   )
+)