aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-26 13:37:08 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-26 13:37:08 +0200
commit4e38a30f78a9fbe6287b310139ecc10aef6d398f (patch)
treea833442cbfeb50c384d6cc3793ee01eb2dca3f99
parent914e0dc50230a76f75ce3b9a7f4585b1e08316d2 (diff)
downloadtabellion-4e38a30f78a9fbe6287b310139ecc10aef6d398f.zip
tabellion-4e38a30f78a9fbe6287b310139ecc10aef6d398f.tar.bz2
Adds some missing files.
-rw-r--r--data/property/async_reset_flip_flop.pro81
-rw-r--r--data/property/flip_flop.pro19
-rw-r--r--data/template/async_reset_flip_flop.pp6
-rw-r--r--data/template/flip_flop.pp4
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$).