aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-20 13:40:40 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-09-20 13:40:40 +0200
commit71e7acf1ac104258a295a2662d6dc71f49ac77aa (patch)
tree4c05ab9471bbf7398355c52542d6170f13c5e3bb
parentfe20276ff74220a51bf8d30aa6190aa5ca6a957f (diff)
downloadtabellion-71e7acf1ac104258a295a2662d6dc71f49ac77aa.zip
tabellion-71e7acf1ac104258a295a2662d6dc71f49ac77aa.tar.bz2
Adds comments to CNE_01700.
-rw-r--r--data/property/CNE_01700.pro378
1 files changed, 194 insertions, 184 deletions
diff --git a/data/property/CNE_01700.pro b/data/property/CNE_01700.pro
index db5e676..7452a3c 100644
--- a/data/property/CNE_01700.pro
+++ b/data/property/CNE_01700.pro
@@ -4,194 +4,191 @@
)
(and
(not (string_matches [identifier [is_waveform_of x_re]] ".*_re"))
- (exists x waveform
- (and
- (not (eq x x_re))
- (exists x_r1 waveform
- (and
- (not (eq x_r1 x_re))
- (not (eq x_r1 x))
- (exists ps2 process
- (and
- (is_in_sensitivity_list x_r1 ps2)
- (is_in_sensitivity_list x ps2)
- (is_accessed_by x_re ps2)
- (CTL_verifies ps2
- (AF
- (and
- (expr_writes x_re)
- (is_read_element "0" "and")
- (or
- (and
- (is_read_structure "(?(??)?)")
- (is_read_element "1" "not")
- (is_read_element "2" x_r1)
- (is_read_element "3" x)
- )
- (and
- (is_read_structure "(??(??))")
- (is_read_element "1" x)
- (is_read_element "2" "not")
- (is_read_element "3" x_r1)
- )
- )
- (AX
- (not
- (EF
- (expr_writes x_r1)
- )
- )
- )
- )
+;; 'x' is the signal 'x_re' detects the rising edge of.
+(exists x waveform
+ (and
+ (not (eq x x_re))
+;; 'x_r1' is 'x' delayed by a flipflop
+(exists x_r1 waveform
+ (and
+ (not (eq x_r1 x_re))
+ (not (eq x_r1 x))
+;; 'ps2' is the process describing 'x_re' as the rising edge
+(exists ps2 process
+ (and
+ (is_in_sensitivity_list x_r1 ps2)
+ (is_in_sensitivity_list x ps2)
+ (is_accessed_by x_re ps2)
+ (CTL_verifies ps2
+ (AF
+ (and
+ (expr_writes x_re)
+ (is_read_element "0" "and")
+ (or
+ ;; x_re <= (not x_r1) and x
+ (and
+ (is_read_structure "(?(??)?)")
+ (is_read_element "1" "not")
+ (is_read_element "2" x_r1)
+ (is_read_element "3" x)
+ )
+ ;; x_re <= x and (not x_r1)
+ (and
+ (is_read_structure "(??(??))")
+ (is_read_element "1" x)
+ (is_read_element "2" "not")
+ (is_read_element "3" x_r1)
+ )
+ )
+ (AX
+ (not
+ (EF
+ (expr_writes x_r1)
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+)
+;; 'ps1' is the process describing 'x_r1' as a flipflop.
+(exists ps1 process
+ (and
+ (is_accessed_by x_r1 ps1)
+ (is_accessed_by x ps1)
+ (is_explicit_process ps1)
+;; 'clk1' is the clock controlling that flipflop
+(exists clk1 waveform
+ (and
+ (is_in_sensitivity_list clk1 ps1)
+ (not (eq clk1 x_re))
+ (not (eq clk1 x))
+ (not (eq clk1 x_r1))
+ (or
+;; 'ps1' could be a simple flipflop
+(CTL_verifies ps1
+ (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" clk1)
+ )
+ (and
+ (is_read_structure "(?(??)(???))")
+ (is_read_element "0" "and")
+ (is_read_element "1" "event")
+ (is_read_element "2" clk1)
+ (is_read_element "3" "=")
+ (or
+ (is_read_element "4" clk1)
+ (is_read_element "5" clk1)
+ )
+ )
+ (and
+ (is_read_structure "(?(???)(??))")
+ (is_read_element "0" "and")
+ (is_read_element "1" "=")
+ (or
+ (is_read_element "2" clk1)
+ (is_read_element "3" clk1)
+ )
+ (is_read_element "4" "event")
+ (is_read_element "5" clk1)
+ )
+ )
+ (EX
+ (and
+ (has_option "cond_was_true")
+ (does_not_reach_parent_before
+ (and
+ (expr_writes x_r1)
+ (is_read_structure "?")
+ (is_read_element "0" x)
+ (AX
+ (not
+ (EF
+ (expr_writes x_r1)
)
)
)
)
- (exists ps1 process
- (and
- (is_accessed_by x_r1 ps1)
- (is_accessed_by x ps1)
- (is_explicit_process ps1)
- (exists clk1 waveform
- (and
- (is_in_sensitivity_list clk1 ps1)
- (not (eq clk1 x_re))
- (not (eq clk1 x))
- (not (eq clk1 x_r1))
- (or
- (CTL_verifies ps1
- (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" clk1)
- )
- (and
- (is_read_structure "(?(??)(???))")
- (is_read_element "0" "and")
- (is_read_element "1" "event")
- (is_read_element "2" clk1)
- (is_read_element "3" "=")
- (or
- (is_read_element "4" clk1)
- (is_read_element "5" clk1)
- )
- )
- (and
- (is_read_structure "(?(???)(??))")
- (is_read_element "0" "and")
- (is_read_element "1" "=")
- (or
- (is_read_element "2" clk1)
- (is_read_element "3" clk1)
- )
- (is_read_element "4" "event")
- (is_read_element "5" clk1)
- )
- )
- (EX
- (and
- (has_option "cond_was_true")
- (does_not_reach_parent_before
- (and
- (expr_writes x_r1)
- (is_read_structure "?")
- (is_read_element "0" x)
- (AX
- (not
- (EF
- (expr_writes x_r1)
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )
- (exists rst1 waveform
- (and
- (is_in_sensitivity_list rst1 ps1)
- (not (eq rst1 x_re))
- (not (eq rst1 x))
- (not (eq rst1 x_r1))
- (not (eq rst1 clk1))
- (CTL_verifies ps1
- (AF
- (and
- (kind "if")
- (is_read_structure "(???)")
- (is_read_element "0" "=")
- (is_read_element _ rst1)
- (EX
- (and
- (not (has_option "cond_was_true"))
- (kind "if")
- (or
- (and
- (is_read_structure "(??)")
- (or
- (is_read_element "0" "falling_edge")
- (is_read_element "0" "rising_edge")
- )
- (is_read_element "1" clk1)
- )
- (and
- (is_read_structure "(?(??)(???))")
- (is_read_element "0" "and")
- (is_read_element "1" "event")
- (is_read_element "2" clk1)
- (is_read_element "3" "=")
- (or
- (is_read_element "4" clk1)
- (is_read_element "5" clk1)
- )
- )
- (and
- (is_read_structure "(?(???)(??))")
- (is_read_element "0" "and")
- (is_read_element "1" "=")
- (or
- (is_read_element "2" clk1)
- (is_read_element "3" clk1)
- )
- (is_read_element "4" "event")
- (is_read_element "5" clk1)
- )
- )
- (EX
- (and
- (has_option "cond_was_true")
- (does_not_reach_parent_before
- (and
- (expr_writes x_r1)
- (is_read_structure "?")
- (is_read_element "0" x)
- (AX
- (not
- (EF
- (expr_writes x_r1)
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )
+ )
+ )
+ )
+ )
+ )
+)
+;; 'ps1' could be a flipflop with reset
+;; 'rst1' is that reset signal
+(exists rst1 waveform
+ (and
+ (is_in_sensitivity_list rst1 ps1)
+ (not (eq rst1 x_re))
+ (not (eq rst1 x))
+ (not (eq rst1 x_r1))
+ (not (eq rst1 clk1))
+(CTL_verifies ps1
+ (AF
+ (and
+ (kind "if")
+ (is_read_structure "(???)")
+ (is_read_element "0" "=")
+ (is_read_element _ rst1)
+ (EX
+ (and
+ (not (has_option "cond_was_true"))
+ (kind "if")
+ (or
+ (and
+ (is_read_structure "(??)")
+ (or
+ (is_read_element "0" "falling_edge")
+ (is_read_element "0" "rising_edge")
+ )
+ (is_read_element "1" clk1)
+ )
+ (and
+ (is_read_structure "(?(??)(???))")
+ (is_read_element "0" "and")
+ (is_read_element "1" "event")
+ (is_read_element "2" clk1)
+ (is_read_element "3" "=")
+ (or
+ (is_read_element "4" clk1)
+ (is_read_element "5" clk1)
+ )
+ )
+ (and
+ (is_read_structure "(?(???)(??))")
+ (is_read_element "0" "and")
+ (is_read_element "1" "=")
+ (or
+ (is_read_element "2" clk1)
+ (is_read_element "3" clk1)
+ )
+ (is_read_element "4" "event")
+ (is_read_element "5" clk1)
+ )
+ )
+ (EX
+ (and
+ (has_option "cond_was_true")
+ (does_not_reach_parent_before
+ (and
+ (expr_writes x_r1)
+ (is_read_structure "?")
+ (is_read_element "0" x)
+ (AX
+ (not
+ (EF
+ (expr_writes x_r1)
)
)
)
@@ -204,3 +201,16 @@
)
)
)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)
+)