| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data')
| -rw-r--r-- | data/property/CNE_01100.pro | 35 | ||||
| -rw-r--r-- | data/property/CNE_01700.pro | 161 | ||||
| -rw-r--r-- | data/property/simple_flip_flop.pro | 5 | ||||
| -rw-r--r-- | data/test/Makefile | 7 |
4 files changed, 30 insertions, 178 deletions
diff --git a/data/property/CNE_01100.pro b/data/property/CNE_01100.pro index 6ed2cff..ad94747 100644 --- a/data/property/CNE_01100.pro +++ b/data/property/CNE_01100.pro @@ -2,28 +2,19 @@ ( (pt port CNE_01100_BAD_NAME) ) - (exists pt2 port - (and -;; Goes into infinity: -;; (has_mode pt2 _) -;; (has_mode pt2 "in") -;; Fixes all: - (eq pt2 pt) - (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") - ) - ) + (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_01700.pro b/data/property/CNE_01700.pro index 7452a3c..2327afc 100644 --- a/data/property/CNE_01700.pro +++ b/data/property/CNE_01700.pro @@ -1,9 +1,11 @@ +#require "flip_flop" + (tag_existing ( (x_re waveform CNE_01700_HAS_BAD_NAME) ) (and - (not (string_matches [identifier [is_waveform_of x_re]] ".*_re")) + (not (string_matches [identifier [is_waveform_of x_re]] ".*_re$")) ;; 'x' is the signal 'x_re' detects the rising edge of. (exists x waveform (and @@ -58,159 +60,16 @@ (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 + (_flip_flop x_r1 _ ps1) + (CTL_verifies ps1 + (EF (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) - ) - ) - ) - ) - ) + (expr_writes x_r1) + (is_read_structure "?") + (is_read_element "0" x) ) ) ) ) ) -;; '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) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) -) -) -) -) -) -) -) -) -) -) -) -) -) +)))))) diff --git a/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro index b054c7f..09ef98b 100644 --- a/data/property/simple_flip_flop.pro +++ b/data/property/simple_flip_flop.pro @@ -9,7 +9,8 @@ (is_explicit_process ps) (is_in_sensitivity_list clk ps) (CTL_verifies ps - (AF + (AU + (not (expr_writes reg)) (and (kind "if") (or @@ -46,7 +47,7 @@ ) (EX (and - (has_option "COND_WAS_TRUE") + (has_option "cond_was_true") (does_not_reach_parent_before (and (expr_writes reg) diff --git a/data/test/Makefile b/data/test/Makefile index 37769db..07f6a88 100644 --- a/data/test/Makefile +++ b/data/test/Makefile @@ -2,7 +2,7 @@ TABELLION_MAIN ?= ${CURDIR}/../../ AST_CREATOR = ghdl --file-to-xml #TEST_DIRS ?= $(addprefix ${CURDIR}/,$(wildcard */)) TEST_DIRS ?= $(patsubst %/,%,$(wildcard */)) -PROPERTY_DIR ?= ${CURDIR}/../property +PROPERTIES_DIR ?= ${CURDIR}/../property # TODO: Start using those variables... SOLUTION_DIR ?= /tmp/tabellion/sol/ ORACLE_CREATOR_SCRIPT = ${CURDIR}/oracle_creator.py @@ -44,6 +44,7 @@ clean: rm -f $(VLD_FILES) rm -f $(IVLD_FILES) rm -f $(SOL_FILES) + rm -f $(addprefix .ready,$(SOL_FILES)) rm -rf /tmp/tabellion_{,in}valid $(AST_FILES): %.xml : %.vhd @@ -62,7 +63,7 @@ $(VLD_FILES): %/valid.result: %/valid.ocl %/valid.xml $(MAKE) -C $(TABELLION_MAIN) \ TMP_DIR=/tmp/tabellion_valid \ AST_FILE=${PWD}/$(dir $@)/valid.xml \ - PROPERTY_FILES=$(PROPERTY_DIR)/$(patsubst %/,%,$(dir $@)).pro \ + PROPERTIES=$(patsubst %/,%,$(dir $@)) \ TEMPLATE_DIR=${PWD}/$(dir $@)/ \ NICE_MESSAGE=/tmp/tabellion_valid/result cat /tmp/tabellion_valid/result | sed '/^\s*$$/d' | sort > /tmp/tabellion_valid/result_clean @@ -78,7 +79,7 @@ $(IVLD_FILES): %/invalid.result: %/invalid.ocl %/invalid.xml $(MAKE) -C $(TABELLION_MAIN) \ TMP_DIR=/tmp/tabellion_invalid \ AST_FILE=${PWD}/$(dir $@)/invalid.xml \ - PROPERTY_FILES=$(PROPERTY_DIR)/$(patsubst %/,%,$(dir $@)).pro \ + PROPERTIES=$(patsubst %/,%,$(dir $@)) \ TEMPLATE_DIR=${PWD}/$(dir $@)/ \ NICE_MESSAGE=/tmp/tabellion_invalid/result cat /tmp/tabellion_invalid/result | sed '/^\s*$$/d' | sort > $@ |