| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data')
| -rw-r--r-- | data/level/instances.lvl | 23 | ||||
| -rw-r--r-- | data/property/simple_flip_flop.pro | 1 | ||||
| -rw-r--r-- | data/property/test-case/fast.pp | 6 | ||||
| -rw-r--r-- | data/property/test-case/fast.pro | 57 | ||||
| -rw-r--r-- | data/property/test-case/slow.pp | 6 | ||||
| -rw-r--r-- | data/property/test-case/slow.pro | 60 |
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) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) |