From f2b7e406b8e77df22ef379a5e880f64d1e5043b9 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 19 Sep 2017 14:05:52 +0200 Subject: Fixes case/when models, regroups properties. --- Makefile | 4 +- ast-to-instr/src/VHDLCSNode.java | 30 +++++ ast-to-instr/src/VHDLSSCNode.java | 32 ++++- data/property/CNE_00100.pro | 59 ++++++++ data/property/CNE_01100.pro | 21 +++ data/property/CNE_01200.pro | 9 ++ data/property/CNE_01400.pro | 8 ++ data/property/CNE_01700.pro | 206 ++++++++++++++++++++++++++++ data/property/CNE_01800.pro | 203 ++++++++++++++++++++++++++++ data/property/CNE_01900.pro | 162 ++++++++++++++++++++++ data/property/CNE_02100.pro | 12 ++ data/property/CNE_02600.pro | 6 + data/property/CNE_04500.pro | 273 ++++++++++++++++++++++++++++++++++++++ data/property/CNE_05100.pro | 64 +++++++++ data/property/STD_04800.pro | 101 ++++++++++++++ data/property/cnes/CNE_00100.pro | 59 -------- data/property/cnes/CNE_01100.pro | 21 --- data/property/cnes/CNE_01200.pro | 9 -- data/property/cnes/CNE_01400.pro | 8 -- data/property/cnes/CNE_01700.pro | 206 ---------------------------- data/property/cnes/CNE_01800.pro | 203 ---------------------------- data/property/cnes/CNE_01900.pro | 162 ---------------------- data/property/cnes/CNE_02100.pro | 12 -- data/property/cnes/CNE_02600.pro | 6 - data/property/cnes/CNE_04500.pro | 273 -------------------------------------- data/property/cnes/CNE_05100.pro | 64 --------- data/property/cnes/STD_04800.pro | 101 -------------- data/test/Makefile | 13 +- 28 files changed, 1189 insertions(+), 1138 deletions(-) create mode 100644 data/property/CNE_00100.pro create mode 100644 data/property/CNE_01100.pro create mode 100644 data/property/CNE_01200.pro create mode 100644 data/property/CNE_01400.pro create mode 100644 data/property/CNE_01700.pro create mode 100644 data/property/CNE_01800.pro create mode 100644 data/property/CNE_01900.pro create mode 100644 data/property/CNE_02100.pro create mode 100644 data/property/CNE_02600.pro create mode 100644 data/property/CNE_04500.pro create mode 100644 data/property/CNE_05100.pro create mode 100644 data/property/STD_04800.pro delete mode 100644 data/property/cnes/CNE_00100.pro delete mode 100644 data/property/cnes/CNE_01100.pro delete mode 100644 data/property/cnes/CNE_01200.pro delete mode 100644 data/property/cnes/CNE_01400.pro delete mode 100644 data/property/cnes/CNE_01700.pro delete mode 100644 data/property/cnes/CNE_01800.pro delete mode 100644 data/property/cnes/CNE_01900.pro delete mode 100644 data/property/cnes/CNE_02100.pro delete mode 100644 data/property/cnes/CNE_02600.pro delete mode 100644 data/property/cnes/CNE_04500.pro delete mode 100644 data/property/cnes/CNE_05100.pro delete mode 100644 data/property/cnes/STD_04800.pro diff --git a/Makefile b/Makefile index 80e587e..983e476 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,6 @@ ## Makefile Parameters ######################################################### LEVEL_FILES ?= $(wildcard ${CURDIR}/data/level/*.lvl) -PROPERTY_FILES ?= \ - $(wildcard ${CURDIR}/data/property/*.pro) \ - $(wildcard ${CURDIR}/data/property/cnes/*.pro) +PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/*.pro) AST_FILE ?= ${CURDIR}/data/ast/best_chronometer_ever.xml TEMPLATE_DIR ?= ${CURDIR}/data/template/ #AST_FILE = ${CURDIR}/data/ast/pong.xml diff --git a/ast-to-instr/src/VHDLCSNode.java b/ast-to-instr/src/VHDLCSNode.java index 6682613..2eaa435 100644 --- a/ast-to-instr/src/VHDLCSNode.java +++ b/ast-to-instr/src/VHDLCSNode.java @@ -196,6 +196,22 @@ public class VHDLCSNode extends VHDLNode for (int i = 0; i < when_branches_length; ++i) { + final Node child; + final String child_xml_id; + final IDs child_local_id; + + child = when_branches.item(i); + child_xml_id = XMLManager.get_attribute(child, "id"); + child_local_id = IDs.get_id_from_xml_id(output, child_xml_id, "node"); + + Predicates.add_entry + ( + output, + "node_connect", + local_id, + child_local_id + ); + waiting_list.add ( new VHDLWNode @@ -251,6 +267,20 @@ public class VHDLCSNode extends VHDLNode } else { + final String child_xml_id; + final IDs child_local_id; + + child_xml_id = XMLManager.get_attribute(others_branch, "id"); + child_local_id = IDs.get_id_from_xml_id(output, child_xml_id, "node"); + + Predicates.add_entry + ( + output, + "node_connect", + local_id, + child_local_id + ); + waiting_list.push ( new VHDLWNode diff --git a/ast-to-instr/src/VHDLSSCNode.java b/ast-to-instr/src/VHDLSSCNode.java index 641377f..97462c9 100644 --- a/ast-to-instr/src/VHDLSSCNode.java +++ b/ast-to-instr/src/VHDLSSCNode.java @@ -40,7 +40,7 @@ public class VHDLSSCNode extends VHDLNode attributes ); - this.prev_node = prev_node; + this.prev_node = prev_node; /* null when first node of the process */ } @Override @@ -54,6 +54,7 @@ public class VHDLSSCNode extends VHDLNode final int intermediary_nodes_count; int i; + /* Find all the nodes, in order, in this instruction chain */ sub_nodes = (NodeList) XPE_FIND_SUB_NODES.evaluate ( @@ -61,13 +62,19 @@ public class VHDLSSCNode extends VHDLNode XPathConstants.NODESET ); + /* Don't handle the last node in the 'for' loop, see below. */ intermediary_nodes_count = (sub_nodes.getLength() - 1); for (i = 0; i < intermediary_nodes_count; ++i) { - final IDs next_node; - - next_node = + /* Prepare the parsing of all those nodes throufh the waiting list. + * To do so, each node needs to be informed of the ID of the node that + * follows it. + */ + final IDs next_seq_node; + + /* Get the ID for the next node in the sequence */ + next_seq_node = IDs.get_id_from_xml_id ( output, @@ -79,11 +86,21 @@ public class VHDLSSCNode extends VHDLNode "node" ); - waiting_list.push(get_vhdl_node(sub_nodes.item(i), next_node, i)); + /* + * Add to the waiting list, 'i' indicates if the attributes inherited + * by the instruction sequence node should be passed along (it's only + * the case if i == 0). + */ + waiting_list.push(get_vhdl_node(sub_nodes.item(i), next_seq_node, i)); } + /* + * The last node of the sequence takes the node following the sequence + * as 'next_node', so it's handled separatly. + */ waiting_list.push(get_vhdl_node(sub_nodes.item(i), next_node, i)); + /* Handle the connection of the first node to the previous node. */ handle_backward_connection(sub_nodes.item(0)); } @@ -193,7 +210,10 @@ public class VHDLSSCNode extends VHDLNode } else { - /* First node of the process */ + /* + * Not the first node, so have the previous node connect to this one + * (which is the first of this instruction set). + */ Predicates.add_entry ( output, diff --git a/data/property/CNE_00100.pro b/data/property/CNE_00100.pro new file mode 100644 index 0000000..1b0893e --- /dev/null +++ b/data/property/CNE_00100.pro @@ -0,0 +1,59 @@ +(tag_existing + ( + (wfm waveform CNE_00100_HAS_BAD_NAME) + ) + (and + ;; If the name of the waveform does not end in "_n", + (not (string_matches [identifier [is_waveform_of wfm]] ".*_n")) + ;; and there is a process + (exists p1 process + ;; that. + (CTL_verifies p1 + ;; at some point, + (EF + (and + ;; has a condition which tests the the signal against '0'. + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (or + (and + (is_read_element "1" "'0'") + (is_read_element "2" wfm) + ) + (and + (is_read_element "1" wfm) + (is_read_element "2" "'0'") + ) + ) + ) + ) + ) + ) + ;; and that signal is never tested against '1'. + (not + (exists p2 process + (CTL_verifies p2 + (EF + (and + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (or + (and + (is_read_element "1" "'1'") + (is_read_element "2" wfm) + ) + (and + (is_read_element "1" wfm) + (is_read_element "2" "'1'") + ) + ) + ) + ) + ) + ) + ) + ) + ;; Then it is misnamed. +) diff --git a/data/property/CNE_01100.pro b/data/property/CNE_01100.pro new file mode 100644 index 0000000..ddeb4e3 --- /dev/null +++ b/data/property/CNE_01100.pro @@ -0,0 +1,21 @@ +(tag_existing + ( + (pt port CNE_01100_BAD_NAME) + ) + (not + (or + (and + (string_matches [identifier pt] "i_.*") + (has_mode pt "in") + ) + (and + (string_matches [identifier pt] "o_.*") + (has_mode pt "out") + ) + (and + (string_matches [identifier pt] "b_.*") + (has_mode pt "inout") + ) + ) + ) +) diff --git a/data/property/CNE_01200.pro b/data/property/CNE_01200.pro new file mode 100644 index 0000000..6649103 --- /dev/null +++ b/data/property/CNE_01200.pro @@ -0,0 +1,9 @@ +(tag_existing + ( + (ps process CNE_01200_BAD_NAME) + ) + (implies + (is_explicit_process ps) + (string_matches [label ps] "P_.*") + ) +) diff --git a/data/property/CNE_01400.pro b/data/property/CNE_01400.pro new file mode 100644 index 0000000..412650e --- /dev/null +++ b/data/property/CNE_01400.pro @@ -0,0 +1,8 @@ +(tag_existing + ( + (gc generic CNE_01400_BAD_NAME) + ) + (not + (string_matches [identifier gc] "g_.*") + ) +) diff --git a/data/property/CNE_01700.pro b/data/property/CNE_01700.pro new file mode 100644 index 0000000..db5e676 --- /dev/null +++ b/data/property/CNE_01700.pro @@ -0,0 +1,206 @@ +(tag_existing + ( + (x_re waveform CNE_01700_HAS_BAD_NAME) + ) + (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) + ) + ) + ) + ) + ) + ) + ) + ) + (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) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/CNE_01800.pro b/data/property/CNE_01800.pro new file mode 100644 index 0000000..fe69841 --- /dev/null +++ b/data/property/CNE_01800.pro @@ -0,0 +1,203 @@ +(tag_existing + ( + (x_fe waveform CNE_01800_HAS_BAD_NAME) + ) + (and + (not (string_matches [identifier [is_waveform_of x_fe]] ".*_fe")) + (exists x waveform + (and + (not (eq x x_fe)) + (exists x_r1 waveform + (and + (not (eq x_r1 x_fe)) + (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_fe ps2) + (CTL_verifies ps2 + (AF + (and + (expr_writes x_fe) + (is_read_element "0" "and") + (or + (and + (is_read_structure "(?(??)?)") + (is_read_element "1" "not") + (is_read_element "2" x) + (is_read_element "3" x_r1) + ) + (and + (is_read_structure "(??(??))") + (is_read_element "1" x_r1) + (is_read_element "2" "not") + (is_read_element "3" 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) + (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_fe)) + (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) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/CNE_01900.pro b/data/property/CNE_01900.pro new file mode 100644 index 0000000..51c373f --- /dev/null +++ b/data/property/CNE_01900.pro @@ -0,0 +1,162 @@ +(tag_existing + ( + (x_r waveform CNE_01900_HAS_BAD_NAME) + ) + (and + (not (string_matches [identifier [is_waveform_of x_r]] ".*_r[0-9]*")) + (exists x waveform + (and + (not (eq x x_r)) + (exists ps1 process + (and + (is_accessed_by x_r ps1) + (is_accessed_by x ps1) + (is_explicit_process ps1) + (exists clk1 waveform + (and + (is_in_sensitivity_list clk1 ps1) + (not (eq clk1 x_r)) + (not (eq clk1 x)) + (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_r) + (is_read_structure "?") + (is_read_element "0" x) + (AX + (not + (EF + (expr_writes x_r) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + (exists rst1 waveform + (and + (is_in_sensitivity_list rst1 ps1) + (not (eq rst1 x_r)) + (not (eq rst1 x)) + (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_r) + (is_read_structure "?") + (is_read_element "0" x) + (AX + (not + (EF + (expr_writes x_r) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/CNE_02100.pro b/data/property/CNE_02100.pro new file mode 100644 index 0000000..8b66f0b --- /dev/null +++ b/data/property/CNE_02100.pro @@ -0,0 +1,12 @@ +(tag_existing + ( + (arch architecture CNE_02100_BAD_NAME) + ) + (not + (or + (identifier arch "Behavioral") + (identifier arch "RTL") + (identifier arch "Simulation") + ) + ) +) diff --git a/data/property/CNE_02600.pro b/data/property/CNE_02600.pro new file mode 100644 index 0000000..f4f89ab --- /dev/null +++ b/data/property/CNE_02600.pro @@ -0,0 +1,6 @@ +(tag_existing + ( + (sl signal CNE_02600_BAD_NAME) + ) + (string_matches [identifier sl] ".{21,}") +) diff --git a/data/property/CNE_04500.pro b/data/property/CNE_04500.pro new file mode 100644 index 0000000..383aec0 --- /dev/null +++ b/data/property/CNE_04500.pro @@ -0,0 +1,273 @@ +(tag_existing + ( + ;; waveform initialized using a reset. + (i_wfm waveform CNE_04500_INITIALIZED_SIGNAL) + ;; waveform not initialized using a reset. + (ni_wfm waveform CNE_04500_NON_INITIALIZED_SIGNAL) + (ps process CNE_04500_BAD_PROCESS) + ) + (and + (is_accessed_by i_wfm ps) + (is_accessed_by ni_wfm ps) + (not (eq ni_wfm i_wfm)) + (exists clk1 waveform + (and + (is_accessed_by clk1 ps) + (not (eq clk1 i_wfm)) + (not (eq clk1 ni_wfm)) + (exists rst1 waveform + (and + (is_accessed_by rst1 ps) + (not (eq rst1 i_wfm)) + (not (eq rst1 ni_wfm)) + (not (eq rst1 clk1)) + (or + ;; With a synchronous reset. + (and + (not (is_in_sensitivity_list rst1 ps)) + (CTL_verifies ps + (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 + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (is_read_element _ rst1) + (EX + (and + (or + (has_option "cond_was_true") + (has_option "cond_was_false") + ) + (does_not_reach_parent_before + (and + (expr_writes i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (not + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + (EX + (and + (or + (has_option "cond_was_true") + (has_option "cond_was_false") + ) + (does_not_reach_parent_before + (and + (expr_writes i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ;; With an asynchronous reset. + (and + (is_in_sensitivity_list rst1 ps) + (CTL_verifies ps + (AF + (and + ;; if (rst = _) + (kind "if") + (is_read_structure "(???)") + (is_read_element "0" "=") + (is_read_element _ rst1) + (EX + (and + ;; then + (has_option "cond_was_true") + (does_not_reach_parent_before + (and + (expr_writes i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (not + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + (EX + (and + ;; else + (not (has_option "cond_was_true")) + (does_not_reach_parent_before + (and + ;; if (edge(clk)) + (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 i_wfm) + (not + (AX + (AF + (expr_writes i_wfm) + ) + ) + ) + ) + ) + (does_not_reach_parent_before + (and + (expr_writes ni_wfm) + (not + (AX + (AF + (expr_writes ni_wfm) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/CNE_05100.pro b/data/property/CNE_05100.pro new file mode 100644 index 0000000..dd8b2c1 --- /dev/null +++ b/data/property/CNE_05100.pro @@ -0,0 +1,64 @@ +(tag_existing + ( + (wfm waveform STRUCT_SINGLE_PROCESS_MULTIPLEXOR) + ) + (exists ps process + (and + (is_explicit_process ps) + (forall sl1 waveform + (and + (CTL_verifies ps + (implies + (EF (expr_writes sl1)) + (AF (expr_writes sl1)) + ) + ) + (implies + (exists target waveform + (CTL_verifies ps + (EF + (and + (is_read_element _ sl1) + (not + (and + (expr_writes target) + (AX + (AF + (expr_writes target) + ) + ) + ) + ) + ) + ) + ) + ) + (is_in_sensitivity_list sl1 ps) + ) + ) + ) + (CTL_verifies ps + (AF + (and + (or + (kind "case") + (kind "if") + ) + (does_not_reach_parent_before + (and + (expr_writes wfm) + (AX + (not + (EF + (expr_writes wfm) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/STD_04800.pro b/data/property/STD_04800.pro new file mode 100644 index 0000000..ae8e4c9 --- /dev/null +++ b/data/property/STD_04800.pro @@ -0,0 +1,101 @@ +(tag_existing + ( + (wfm waveform STD_04800_DOUBLE_SENSITIVITY_EDGE_CLOCK) + ) + (and + (exists ps_re process + (CTL_verifies ps_re + (EF + (or + (and + (is_read_structure "(??)") + (is_read_element "0" "rising_edge") + (is_read_element "1" wfm) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" wfm) + (is_read_element "3" "=") + (or + (and + (is_read_element "4" wfm) + (is_read_element "5" "'1'") + ) + (and + (is_read_element "4" "'1'") + (is_read_element "5" wfm) + ) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (and + (is_read_element "2" wfm) + (is_read_element "3" "'1'") + ) + (and + (is_read_element "2" "'1'") + (is_read_element "3" wfm) + ) + ) + (is_read_element "4" "event") + (is_read_element "5" wfm) + ) + ) + ) + ) + ) + (exists ps_fe process + (CTL_verifies ps_fe + (EF + (or + (and + (is_read_structure "(??)") + (is_read_element "0" "falling_edge") + (is_read_element "1" wfm) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" wfm) + (is_read_element "3" "=") + (or + (and + (is_read_element "4" wfm) + (is_read_element "5" "'0'") + ) + (and + (is_read_element "4" "'0'") + (is_read_element "5" wfm) + ) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (and + (is_read_element "2" wfm) + (is_read_element "3" "'0'") + ) + (and + (is_read_element "2" "'0'") + (is_read_element "3" wfm) + ) + ) + (is_read_element "4" "event") + (is_read_element "5" wfm) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/cnes/CNE_00100.pro b/data/property/cnes/CNE_00100.pro deleted file mode 100644 index 1b0893e..0000000 --- a/data/property/cnes/CNE_00100.pro +++ /dev/null @@ -1,59 +0,0 @@ -(tag_existing - ( - (wfm waveform CNE_00100_HAS_BAD_NAME) - ) - (and - ;; If the name of the waveform does not end in "_n", - (not (string_matches [identifier [is_waveform_of wfm]] ".*_n")) - ;; and there is a process - (exists p1 process - ;; that. - (CTL_verifies p1 - ;; at some point, - (EF - (and - ;; has a condition which tests the the signal against '0'. - (kind "if") - (is_read_structure "(???)") - (is_read_element "0" "=") - (or - (and - (is_read_element "1" "'0'") - (is_read_element "2" wfm) - ) - (and - (is_read_element "1" wfm) - (is_read_element "2" "'0'") - ) - ) - ) - ) - ) - ) - ;; and that signal is never tested against '1'. - (not - (exists p2 process - (CTL_verifies p2 - (EF - (and - (kind "if") - (is_read_structure "(???)") - (is_read_element "0" "=") - (or - (and - (is_read_element "1" "'1'") - (is_read_element "2" wfm) - ) - (and - (is_read_element "1" wfm) - (is_read_element "2" "'1'") - ) - ) - ) - ) - ) - ) - ) - ) - ;; Then it is misnamed. -) diff --git a/data/property/cnes/CNE_01100.pro b/data/property/cnes/CNE_01100.pro deleted file mode 100644 index ddeb4e3..0000000 --- a/data/property/cnes/CNE_01100.pro +++ /dev/null @@ -1,21 +0,0 @@ -(tag_existing - ( - (pt port CNE_01100_BAD_NAME) - ) - (not - (or - (and - (string_matches [identifier pt] "i_.*") - (has_mode pt "in") - ) - (and - (string_matches [identifier pt] "o_.*") - (has_mode pt "out") - ) - (and - (string_matches [identifier pt] "b_.*") - (has_mode pt "inout") - ) - ) - ) -) diff --git a/data/property/cnes/CNE_01200.pro b/data/property/cnes/CNE_01200.pro deleted file mode 100644 index 6649103..0000000 --- a/data/property/cnes/CNE_01200.pro +++ /dev/null @@ -1,9 +0,0 @@ -(tag_existing - ( - (ps process CNE_01200_BAD_NAME) - ) - (implies - (is_explicit_process ps) - (string_matches [label ps] "P_.*") - ) -) diff --git a/data/property/cnes/CNE_01400.pro b/data/property/cnes/CNE_01400.pro deleted file mode 100644 index 412650e..0000000 --- a/data/property/cnes/CNE_01400.pro +++ /dev/null @@ -1,8 +0,0 @@ -(tag_existing - ( - (gc generic CNE_01400_BAD_NAME) - ) - (not - (string_matches [identifier gc] "g_.*") - ) -) diff --git a/data/property/cnes/CNE_01700.pro b/data/property/cnes/CNE_01700.pro deleted file mode 100644 index db5e676..0000000 --- a/data/property/cnes/CNE_01700.pro +++ /dev/null @@ -1,206 +0,0 @@ -(tag_existing - ( - (x_re waveform CNE_01700_HAS_BAD_NAME) - ) - (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) - ) - ) - ) - ) - ) - ) - ) - ) - (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) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) diff --git a/data/property/cnes/CNE_01800.pro b/data/property/cnes/CNE_01800.pro deleted file mode 100644 index fe69841..0000000 --- a/data/property/cnes/CNE_01800.pro +++ /dev/null @@ -1,203 +0,0 @@ -(tag_existing - ( - (x_fe waveform CNE_01800_HAS_BAD_NAME) - ) - (and - (not (string_matches [identifier [is_waveform_of x_fe]] ".*_fe")) - (exists x waveform - (and - (not (eq x x_fe)) - (exists x_r1 waveform - (and - (not (eq x_r1 x_fe)) - (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_fe ps2) - (CTL_verifies ps2 - (AF - (and - (expr_writes x_fe) - (is_read_element "0" "and") - (or - (and - (is_read_structure "(?(??)?)") - (is_read_element "1" "not") - (is_read_element "2" x) - (is_read_element "3" x_r1) - ) - (and - (is_read_structure "(??(??))") - (is_read_element "1" x_r1) - (is_read_element "2" "not") - (is_read_element "3" 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) - (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_fe)) - (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) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) diff --git a/data/property/cnes/CNE_01900.pro b/data/property/cnes/CNE_01900.pro deleted file mode 100644 index 51c373f..0000000 --- a/data/property/cnes/CNE_01900.pro +++ /dev/null @@ -1,162 +0,0 @@ -(tag_existing - ( - (x_r waveform CNE_01900_HAS_BAD_NAME) - ) - (and - (not (string_matches [identifier [is_waveform_of x_r]] ".*_r[0-9]*")) - (exists x waveform - (and - (not (eq x x_r)) - (exists ps1 process - (and - (is_accessed_by x_r ps1) - (is_accessed_by x ps1) - (is_explicit_process ps1) - (exists clk1 waveform - (and - (is_in_sensitivity_list clk1 ps1) - (not (eq clk1 x_r)) - (not (eq clk1 x)) - (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_r) - (is_read_structure "?") - (is_read_element "0" x) - (AX - (not - (EF - (expr_writes x_r) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - (exists rst1 waveform - (and - (is_in_sensitivity_list rst1 ps1) - (not (eq rst1 x_r)) - (not (eq rst1 x)) - (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_r) - (is_read_structure "?") - (is_read_element "0" x) - (AX - (not - (EF - (expr_writes x_r) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) diff --git a/data/property/cnes/CNE_02100.pro b/data/property/cnes/CNE_02100.pro deleted file mode 100644 index 8b66f0b..0000000 --- a/data/property/cnes/CNE_02100.pro +++ /dev/null @@ -1,12 +0,0 @@ -(tag_existing - ( - (arch architecture CNE_02100_BAD_NAME) - ) - (not - (or - (identifier arch "Behavioral") - (identifier arch "RTL") - (identifier arch "Simulation") - ) - ) -) diff --git a/data/property/cnes/CNE_02600.pro b/data/property/cnes/CNE_02600.pro deleted file mode 100644 index f4f89ab..0000000 --- a/data/property/cnes/CNE_02600.pro +++ /dev/null @@ -1,6 +0,0 @@ -(tag_existing - ( - (sl signal CNE_02600_BAD_NAME) - ) - (string_matches [identifier sl] ".{21,}") -) diff --git a/data/property/cnes/CNE_04500.pro b/data/property/cnes/CNE_04500.pro deleted file mode 100644 index 383aec0..0000000 --- a/data/property/cnes/CNE_04500.pro +++ /dev/null @@ -1,273 +0,0 @@ -(tag_existing - ( - ;; waveform initialized using a reset. - (i_wfm waveform CNE_04500_INITIALIZED_SIGNAL) - ;; waveform not initialized using a reset. - (ni_wfm waveform CNE_04500_NON_INITIALIZED_SIGNAL) - (ps process CNE_04500_BAD_PROCESS) - ) - (and - (is_accessed_by i_wfm ps) - (is_accessed_by ni_wfm ps) - (not (eq ni_wfm i_wfm)) - (exists clk1 waveform - (and - (is_accessed_by clk1 ps) - (not (eq clk1 i_wfm)) - (not (eq clk1 ni_wfm)) - (exists rst1 waveform - (and - (is_accessed_by rst1 ps) - (not (eq rst1 i_wfm)) - (not (eq rst1 ni_wfm)) - (not (eq rst1 clk1)) - (or - ;; With a synchronous reset. - (and - (not (is_in_sensitivity_list rst1 ps)) - (CTL_verifies ps - (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 - (kind "if") - (is_read_structure "(???)") - (is_read_element "0" "=") - (is_read_element _ rst1) - (EX - (and - (or - (has_option "cond_was_true") - (has_option "cond_was_false") - ) - (does_not_reach_parent_before - (and - (expr_writes i_wfm) - (not - (AX - (AF - (expr_writes i_wfm) - ) - ) - ) - ) - ) - (not - (does_not_reach_parent_before - (and - (expr_writes ni_wfm) - (not - (AX - (AF - (expr_writes ni_wfm) - ) - ) - ) - ) - ) - ) - ) - ) - (EX - (and - (or - (has_option "cond_was_true") - (has_option "cond_was_false") - ) - (does_not_reach_parent_before - (and - (expr_writes i_wfm) - (not - (AX - (AF - (expr_writes i_wfm) - ) - ) - ) - ) - ) - (does_not_reach_parent_before - (and - (expr_writes ni_wfm) - (not - (AX - (AF - (expr_writes ni_wfm) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ;; With an asynchronous reset. - (and - (is_in_sensitivity_list rst1 ps) - (CTL_verifies ps - (AF - (and - ;; if (rst = _) - (kind "if") - (is_read_structure "(???)") - (is_read_element "0" "=") - (is_read_element _ rst1) - (EX - (and - ;; then - (has_option "cond_was_true") - (does_not_reach_parent_before - (and - (expr_writes i_wfm) - (not - (AX - (AF - (expr_writes i_wfm) - ) - ) - ) - ) - ) - (not - (does_not_reach_parent_before - (and - (expr_writes ni_wfm) - (not - (AX - (AF - (expr_writes ni_wfm) - ) - ) - ) - ) - ) - ) - ) - ) - (EX - (and - ;; else - (not (has_option "cond_was_true")) - (does_not_reach_parent_before - (and - ;; if (edge(clk)) - (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 i_wfm) - (not - (AX - (AF - (expr_writes i_wfm) - ) - ) - ) - ) - ) - (does_not_reach_parent_before - (and - (expr_writes ni_wfm) - (not - (AX - (AF - (expr_writes ni_wfm) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) diff --git a/data/property/cnes/CNE_05100.pro b/data/property/cnes/CNE_05100.pro deleted file mode 100644 index dd8b2c1..0000000 --- a/data/property/cnes/CNE_05100.pro +++ /dev/null @@ -1,64 +0,0 @@ -(tag_existing - ( - (wfm waveform STRUCT_SINGLE_PROCESS_MULTIPLEXOR) - ) - (exists ps process - (and - (is_explicit_process ps) - (forall sl1 waveform - (and - (CTL_verifies ps - (implies - (EF (expr_writes sl1)) - (AF (expr_writes sl1)) - ) - ) - (implies - (exists target waveform - (CTL_verifies ps - (EF - (and - (is_read_element _ sl1) - (not - (and - (expr_writes target) - (AX - (AF - (expr_writes target) - ) - ) - ) - ) - ) - ) - ) - ) - (is_in_sensitivity_list sl1 ps) - ) - ) - ) - (CTL_verifies ps - (AF - (and - (or - (kind "case") - (kind "if") - ) - (does_not_reach_parent_before - (and - (expr_writes wfm) - (AX - (not - (EF - (expr_writes wfm) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) diff --git a/data/property/cnes/STD_04800.pro b/data/property/cnes/STD_04800.pro deleted file mode 100644 index ae8e4c9..0000000 --- a/data/property/cnes/STD_04800.pro +++ /dev/null @@ -1,101 +0,0 @@ -(tag_existing - ( - (wfm waveform STD_04800_DOUBLE_SENSITIVITY_EDGE_CLOCK) - ) - (and - (exists ps_re process - (CTL_verifies ps_re - (EF - (or - (and - (is_read_structure "(??)") - (is_read_element "0" "rising_edge") - (is_read_element "1" wfm) - ) - (and - (is_read_structure "(?(??)(???))") - (is_read_element "0" "and") - (is_read_element "1" "event") - (is_read_element "2" wfm) - (is_read_element "3" "=") - (or - (and - (is_read_element "4" wfm) - (is_read_element "5" "'1'") - ) - (and - (is_read_element "4" "'1'") - (is_read_element "5" wfm) - ) - ) - ) - (and - (is_read_structure "(?(???)(??))") - (is_read_element "0" "and") - (is_read_element "1" "=") - (or - (and - (is_read_element "2" wfm) - (is_read_element "3" "'1'") - ) - (and - (is_read_element "2" "'1'") - (is_read_element "3" wfm) - ) - ) - (is_read_element "4" "event") - (is_read_element "5" wfm) - ) - ) - ) - ) - ) - (exists ps_fe process - (CTL_verifies ps_fe - (EF - (or - (and - (is_read_structure "(??)") - (is_read_element "0" "falling_edge") - (is_read_element "1" wfm) - ) - (and - (is_read_structure "(?(??)(???))") - (is_read_element "0" "and") - (is_read_element "1" "event") - (is_read_element "2" wfm) - (is_read_element "3" "=") - (or - (and - (is_read_element "4" wfm) - (is_read_element "5" "'0'") - ) - (and - (is_read_element "4" "'0'") - (is_read_element "5" wfm) - ) - ) - ) - (and - (is_read_structure "(?(???)(??))") - (is_read_element "0" "and") - (is_read_element "1" "=") - (or - (and - (is_read_element "2" wfm) - (is_read_element "3" "'0'") - ) - (and - (is_read_element "2" "'0'") - (is_read_element "3" wfm) - ) - ) - (is_read_element "4" "event") - (is_read_element "5" wfm) - ) - ) - ) - ) - ) - ) -) diff --git a/data/test/Makefile b/data/test/Makefile index f38526a..eec299d 100644 --- a/data/test/Makefile +++ b/data/test/Makefile @@ -22,6 +22,9 @@ all: $(AST_FILES) $(OCL_FILES) $(VLD_FILES) $(IVLD_FILES) clean: rm -f $(AST_FILES) rm -f $(OCL_FILES) + rm -f $(VLD_FILES) + rm -f $(IVLD_FILES) + rm -rf /tmp/tabellion_{,in}valid $(AST_FILES): %.xml : %.vhd $(AST_CREATOR) $< > $@ @@ -41,9 +44,9 @@ $(VLD_FILES): %/valid.result: %/valid.ocl %/valid.xml AST_FILE=${PWD}/$(dir $@)/valid.xml \ PROPERTY_FILES=$(PROPERTY_DIR)/$(patsubst %/,%,$(dir $@)).pro \ TEMPLATE_DIR=${PWD}/$(dir $@)/ \ - NICE_MESSAGE=/tmp/tabellion/valid_test_result - cat /tmp/tabellion/valid_test_result | sed '/^\s*$$/d' | sort > $@ - diff $@ $(dir $@)/valid.ocl || true > $@ + NICE_MESSAGE=/tmp/tabellion_valid/result + cat /tmp/tabellion_valid/result | sed '/^\s*$$/d' | sort > /tmp/tabellion_valid/result_clean + -diff /tmp/tabellion_valid/result_clean $(dir $@)/valid.ocl > $@ $(IVLD_FILES): %/invalid.result: %/invalid.ocl %/invalid.xml $(MAKE) -C $(TABELLION_MAIN) \ @@ -57,5 +60,5 @@ $(IVLD_FILES): %/invalid.result: %/invalid.ocl %/invalid.xml AST_FILE=${PWD}/$(dir $@)/invalid.xml \ PROPERTY_FILES=$(PROPERTY_DIR)/$(patsubst %/,%,$(dir $@)).pro \ TEMPLATE_DIR=${PWD}/$(dir $@)/ \ - NICE_MESSAGE=${PWD}/$@ - cat $@ | sed '/^\s*$$/d' | sort > $@ + NICE_MESSAGE=/tmp/tabellion_invalid/result + cat /tmp/tabellion_invalid/result | sed '/^\s*$$/d' | sort > $@ -- cgit v1.2.3-70-g09d2