| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | data/property/async_reset_flip_flop.pro | 81 | ||||
| -rw-r--r-- | data/property/flip_flop.pro | 19 | ||||
| -rw-r--r-- | data/template/async_reset_flip_flop.pp | 6 | ||||
| -rw-r--r-- | data/template/flip_flop.pp | 4 |
4 files changed, 110 insertions, 0 deletions
diff --git a/data/property/async_reset_flip_flop.pro b/data/property/async_reset_flip_flop.pro new file mode 100644 index 0000000..0d50a47 --- /dev/null +++ b/data/property/async_reset_flip_flop.pro @@ -0,0 +1,81 @@ +(tag_existing + ( + (reg waveform STRUCT_ASYNC_RST_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_ASYNC_RST_FLIP_FLOP_CLOCK) + (rst waveform STRUCT_ASYNC_RST_FLIP_FLOP_CLOCK) + (ps process STRUCT_ASYNC_RST_FLIP_FLOP_PROCESS) + ) + (and + (not (eq clk reg)) + (not (eq rst reg)) + (not (eq rst clk)) + (is_explicit_process ps) + (is_in_sensitivity_list clk ps) + (is_in_sensitivity_list rst ps) + (CTL_verifies ps + (AU + (not (expr_writes reg)) + (and + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (is_read_element _ rst) + (EX + (and + (not (has_option "cond_was_true")) + (or + (and + (is_read_structure "(??)") + (or + (is_read_element "0" "falling_edge") + (is_read_element "0" "rising_edge") + ) + (is_read_element "1" clk) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" clk) + (is_read_element "3" "=") + (or + (is_read_element "4" clk) + (is_read_element "5" clk) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (is_read_element "2" clk) + (is_read_element "3" clk) + ) + (is_read_element "4" "event") + (is_read_element "5" 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/flip_flop.pro b/data/property/flip_flop.pro new file mode 100644 index 0000000..9e7989e --- /dev/null +++ b/data/property/flip_flop.pro @@ -0,0 +1,19 @@ +#require "simple_flip_flop" +#require "async_reset_flip_flop" + +(tag_existing + ( + (reg waveform STRUCT_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_FLIP_FLOP_CLOCK) + (ps process STRUCT_FLIP_FLOP_PROCESS) + ) + (and + (not (eq reg clk)) +;; (is_accessed_by reg ps) +;; (is_accessed_by clk ps) + (or + (_simple_flip_flop reg clk ps) + (_async_reset_flip_flop reg clk _ ps) + ) + ) +) diff --git a/data/template/async_reset_flip_flop.pp b/data/template/async_reset_flip_flop.pp new file mode 100644 index 0000000..d484d12 --- /dev/null +++ b/data/template/async_reset_flip_flop.pp @@ -0,0 +1,6 @@ +The process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$) +describes a flip-flop controlled by $clk.IDENTIFIER$ (declared in +$clk.FILE$, l. $clk.LINE$, c. $clk.COLUMN$), with asynchronous reset +$rst.IDENTIFIER$ (declared in $rst.FILE$, l. $rst.LINE$, c. $rst.COLUMN$), and +with output $reg.IDENTIFIER$ (declared in $reg.FILE$, l. $reg.LINE$, +c. $reg.COLUMN$). diff --git a/data/template/flip_flop.pp b/data/template/flip_flop.pp new file mode 100644 index 0000000..061ee2d --- /dev/null +++ b/data/template/flip_flop.pp @@ -0,0 +1,4 @@ +The process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$) +describes some kind of 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$). |