| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data')
| -rw-r--r-- | data/property/combinational_processes.pp | 2 | ||||
| -rw-r--r-- | data/property/impossible_processes.pp | 2 | ||||
| -rw-r--r-- | data/property/incrementer.pp | 3 | ||||
| -rw-r--r-- | data/property/incrementer.pro | 15 | ||||
| -rw-r--r-- | data/property/likely_a_clock.pp | 3 | ||||
| -rw-r--r-- | data/property/simple_flip_flop.pp | 4 | ||||
| -rw-r--r-- | data/property/simple_flip_flop.pro | 41 | ||||
| -rw-r--r-- | data/property/unread_waveforms.pro | 10 |
8 files changed, 62 insertions, 18 deletions
diff --git a/data/property/combinational_processes.pp b/data/property/combinational_processes.pp new file mode 100644 index 0000000..7d73bf9 --- /dev/null +++ b/data/property/combinational_processes.pp @@ -0,0 +1,2 @@ +The processus $ps.LABEL$ (from file $ps.FILE$, line $ps.LINE$, column +$ps.COLUMN$) is combinational. diff --git a/data/property/impossible_processes.pp b/data/property/impossible_processes.pp new file mode 100644 index 0000000..a13e0e5 --- /dev/null +++ b/data/property/impossible_processes.pp @@ -0,0 +1,2 @@ +The process $ps.LABEL$ (from file $ps.FILE$, line $ps.LINE$, column +$ps.COLUMN$) does not write anything and is thus unlikely to have any effect. diff --git a/data/property/incrementer.pp b/data/property/incrementer.pp new file mode 100644 index 0000000..5fe3e96 --- /dev/null +++ b/data/property/incrementer.pp @@ -0,0 +1,3 @@ +The waveform associated with $wf.IDENTIFIER$ (from file $wf.FILE$, line $wf.LINE$ +column $wf.COLUMN$) is incremented by the process $ps.LABEL$ (from +$ps.FILE$, line $ps.line$, column $ps.COLUMN$). diff --git a/data/property/incrementer.pro b/data/property/incrementer.pro index ba8fc7a..4bc06ae 100644 --- a/data/property/incrementer.pro +++ b/data/property/incrementer.pro @@ -1,15 +1,14 @@ (tag_existing ( (wf waveform INCREMENTED_WAVEFORM) + (ps process INCREMENTER_PROCESS) ) - (exists ps process - (CTL_verifies ps - (EF - (and - (is_read_structure "(??L)") - (is_read_element "0" "+") - (is_read_element "1" wf) - ) + (CTL_verifies ps + (EF + (and + (is_read_structure "(??L)") + (is_read_element "0" "+") + (is_read_element "1" wf) ) ) ) diff --git a/data/property/likely_a_clock.pp b/data/property/likely_a_clock.pp new file mode 100644 index 0000000..aea7af2 --- /dev/null +++ b/data/property/likely_a_clock.pp @@ -0,0 +1,3 @@ +The port $clock.IDENTIFIER$ (from file $clock.FILE$, line $clock.LINE$, column +$clock.COLUMN$) is passed as parameter of either a rising_edge or a falling_edge +function, making it likely to be a clock. diff --git a/data/property/simple_flip_flop.pp b/data/property/simple_flip_flop.pp new file mode 100644 index 0000000..fbad237 --- /dev/null +++ b/data/property/simple_flip_flop.pp @@ -0,0 +1,4 @@ +The process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$) +describes a simple flip-flop 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.pro b/data/property/simple_flip_flop.pro new file mode 100644 index 0000000..ea67575 --- /dev/null +++ b/data/property/simple_flip_flop.pro @@ -0,0 +1,41 @@ +(tag_existing + ( + (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) + (is_in_sensitivity_list clk ps) + (CTL_verifies ps + (AF + (and + (kind "if") + (is_read_structure "(??)") + (or + (is_read_element "0" "falling_edge") + (is_read_element "0" "rising_edge") + ) + (is_read_element "1" clk) + (EX + (and + (has_option "COND_WAS_TRUE") + (does_not_reach_parent_before + (and + (expr_writes reg) + (AX + (not + (EF + (expr_writes reg) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/unread_waveforms.pro b/data/property/unread_waveforms.pro deleted file mode 100644 index b53862b..0000000 --- a/data/property/unread_waveforms.pro +++ /dev/null @@ -1,10 +0,0 @@ -(tag_existing - ( - (wf waveform UNREAD_WAVEFORM) - ) - (not - (exists ps process - (is_accessed_by wf ps) - ) - ) -) |