| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data/property/test-case')
| -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 |
4 files changed, 129 insertions, 0 deletions
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) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) |