summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-26 14:45:43 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-26 14:45:43 +0200
commit694d42f9ca5e6728dc1170a740264ee98bf5cbe5 (patch)
tree4bacefafc5da24ce733d3d799000a3dd37d40620
parent5f06e34bc24876739c1d4af1d45f7cb322a19559 (diff)
New pr
-rw-r--r--data/property/likely_a_clock.pro25
1 files changed, 25 insertions, 0 deletions
diff --git a/data/property/likely_a_clock.pro b/data/property/likely_a_clock.pro
new file mode 100644
index 0000000..2aae4a4
--- /dev/null
+++ b/data/property/likely_a_clock.pro
@@ -0,0 +1,25 @@
+(tag_existing
+ (
+ (clock port LIKELY_A_CLOCK)
+ )
+ (exists wf waveform
+ (and
+ (is_waveform_of wf clock)
+ (exists ps process
+ (CTL_verifies ps
+ (EF
+ (and
+ (kind "if")
+ (is_read_structure "(??)")
+ (or
+ (is_read_element "0" "rising_edge")
+ (is_read_element "0" "falling_edge")
+ )
+ (is_read_element "1" wf)
+ )
+ )
+ )
+ )
+ )
+ )
+)