From 4669bdf7046c03200a28de4188075bee69571eb8 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 25 Sep 2017 12:48:44 +0200 Subject: Updates Tests, fixes 2 properties & inferred/*.mod --- Makefile | 6 +- data/property/CNE_01100.pro | 35 +++----- data/property/CNE_01700.pro | 161 +++---------------------------------- data/property/simple_flip_flop.pro | 5 +- data/test/Makefile | 7 +- instr-to-kodkod/Makefile | 4 +- sol-pretty-printer/Makefile | 2 +- 7 files changed, 37 insertions(+), 183 deletions(-) diff --git a/Makefile b/Makefile index 1f72ef0..e8242d7 100644 --- a/Makefile +++ b/Makefile @@ -42,21 +42,21 @@ all: $(ALL_DIRS) $(MAKE) model $(MAKE) solutions -compile: +compile: $(ALL_DIRS) $(MAKE) -C $(AST_TO_INSTR) compile $(MAKE) -C $(INST_CALC) compile $(MAKE) -C $(SOLVER) compile $(MAKE) -C $(PRETTY_PRINTER) compile $(MAKE) -C $(PROP_TO_PRED) compile -model: +model: $(ALL_DIRS) $(MAKE) -C $(AST_TO_INSTR) model $(MAKE) -C $(INST_CALC) model $(MAKE) -C $(SOLVER) model $(MAKE) -C $(PRETTY_PRINTER) model $(MAKE) -C $(PROP_TO_PRED) model -solutions: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) +solutions: $(ALL_DIRS) $(MAKE) -C $(AST_TO_INSTR) solutions $(MAKE) -C $(INST_CALC) solutions $(MAKE) -C $(SOLVER) solutions 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 > $@ diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 0523a46..cac9ffe 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -108,6 +108,7 @@ clean: $(MAKE) -C cfg-to-paths clean rm -f $(CLASSES) rm -f $(SOL_DIR)/*.sol + rm -f $(SOL_DIR)/*.sol.ready rm -f $(DEPENDENCY_FILES) rm -f $(wildcard $(MODEL_INFERRED_DIR)/*.mod) @@ -117,6 +118,7 @@ clean_model: clean_solutions: rm -f $(SOL_DIR)/*.sol + rm -f $(SOL_DIR)/*.sol.ready rm -f $(DEPENDENCY_FILES) ######## @@ -136,7 +138,7 @@ $(SOLUTION_FILES): $(SOL_DIR)/%.sol: $(PROPERTIES_DIR)/%.pro \ $< \ $(LEVEL_FILES) \ $(MODEL_FILES) \ - $(MODEL_INFERRED_DIR)/*.mod \ + `ls $(MODEL_INFERRED_DIR)/*.mod 2>/dev/null`\ $(wildcard $(PATH_MODEL_DIR)/*.mod) echo "" >> $@ $(MAKE) -C .. \ diff --git a/sol-pretty-printer/Makefile b/sol-pretty-printer/Makefile index f5c6e7a..262078b 100644 --- a/sol-pretty-printer/Makefile +++ b/sol-pretty-printer/Makefile @@ -48,7 +48,7 @@ CLASSES = $(SOURCES:.java=.class) SOLUTION_FILES = $(wildcard $(SOL_DIR)/*.sol) PROPERTY_PP_FILES = $(wildcard $(TEMPLATE_DIR)/*.pp) SOLUTION_PP_PAIRS = \ - $(foreach sf,$(SOLUTION_FILES),$(sf) $(filter %$(basename $(notdir $(sf))).pp,$(PROPERTY_PP_FILES))) + $(foreach sf,$(SOLUTION_FILES),$(sf) $(TEMPLATE_DIR)/$(basename $(notdir $(sf))).pp) ## Makefile Rules ############################################################## compile: $(CLASSES) -- cgit v1.2.3-70-g09d2