From d18ca72caf2004c7725b3de670c7397c5bf85eb4 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Fri, 4 Aug 2017 12:47:30 +0200 Subject: For some reason, CNE_01700 no longer works. --- data/property/simple_flip_flop.pro | 41 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 data/property/simple_flip_flop.pro (limited to 'data/property/simple_flip_flop.pro') 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) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) -- cgit v1.2.3-70-g09d2