| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data')
| -rw-r--r-- | data/level/instances.lvl | 13 | ||||
| -rw-r--r-- | data/property/simple_flip_flop_instance.pp | 6 | ||||
| -rw-r--r-- | data/property/simple_flip_flop_instance.pro | 95 |
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) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) +)))))))))))) |