From ea11fdc81ed7a8df14868476c04bf2fe7c7b6393 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 29 Aug 2017 16:51:09 +0200 Subject: Most of the program's logic seems to be there... --- Makefile | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 19a69d8..ecaee82 100644 --- a/Makefile +++ b/Makefile @@ -12,6 +12,7 @@ SOL_DIR = $(TMP_DIR)/sol ## Sub-programs ################################################################ AST_TO_INSTR = ast-to-instr +INST_CALC = instance-calculator SOLVER = instr-to-kodkod PRETTY_PRINTER = sol-pretty-printer @@ -24,31 +25,37 @@ all: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) compile: $(MAKE) -C $(AST_TO_INSTR) compile + $(MAKE) -C $(INST_CALC) compile $(MAKE) -C $(SOLVER) compile $(MAKE) -C $(PRETTY_PRINTER) compile model: $(MAKE) -C $(AST_TO_INSTR) model + $(MAKE) -C $(INST_CALC) model $(MAKE) -C $(SOLVER) model $(MAKE) -C $(PRETTY_PRINTER) model solutions: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) $(MAKE) -C $(AST_TO_INSTR) solutions + $(MAKE) -C $(INST_CALC) solutions $(MAKE) -C $(SOLVER) solutions $(MAKE) -C $(PRETTY_PRINTER) solutions clean: $(MAKE) -C $(AST_TO_INSTR) clean + $(MAKE) -C $(INST_CALC) clean $(MAKE) -C $(SOLVER) clean $(MAKE) -C $(PRETTY_PRINTER) clean clean_model: $(MAKE) -C $(AST_TO_INSTR) clean_model + $(MAKE) -C $(INST_CALC) clean_model $(MAKE) -C $(SOLVER) clean_model $(MAKE) -C $(PRETTY_PRINTER) clean_model clean_solutions: $(MAKE) -C $(AST_TO_INSTR) clean_solutions + $(MAKE) -C $(INST_CALC) clean_solutions $(MAKE) -C $(SOLVER) clean_solutions $(MAKE) -C $(PRETTY_PRINTER) clean_solutions -- cgit v1.2.3-70-g09d2 From b715c825c0a36063e7b79248059263b438a0b5a6 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 30 Aug 2017 13:57:53 +0200 Subject: Gets stuck due to scaling issues. --- Makefile | 5 +++-- data/level/instances.lvl | 22 ++++++++++++++++++++++ instance-calculator/Makefile | 18 +++++++++--------- instr-to-kodkod/Makefile | 4 +++- 4 files changed, 37 insertions(+), 12 deletions(-) create mode 100644 data/level/instances.lvl (limited to 'Makefile') diff --git a/Makefile b/Makefile index ecaee82..4a18566 100644 --- a/Makefile +++ b/Makefile @@ -1,13 +1,14 @@ ## Makefile Parameters ######################################################### LEVEL_FILES = $(wildcard ${CURDIR}/data/level/*.lvl) PROPERTY_FILES = \ - $(wildcard ${CURDIR}/data/property/*.pro) \ - $(wildcard ${CURDIR}/data/property/cnes/*.pro) + $(wildcard ${CURDIR}/data/property/*.pro) +# $(wildcard ${CURDIR}/data/property/cnes/*.pro) AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml #AST_FILE = ${CURDIR}/data/ast/pong.xml TMP_DIR = /tmp/tabellion MODEL_DIR = $(TMP_DIR)/mod +MODEL_INSTANCES_DIR = $(TMP_DIR)/instance SOL_DIR = $(TMP_DIR)/sol ## Sub-programs ################################################################ diff --git a/data/level/instances.lvl b/data/level/instances.lvl new file mode 100644 index 0000000..5fdb42b --- /dev/null +++ b/data/level/instances.lvl @@ -0,0 +1,22 @@ +;; Instances + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_type instance) + +;; Redundancies +(add_type entity) +(add_type process) +(add_type waveform) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_waveform_instance instance waveform) +(add_predicate is_visible_in instance waveform entity) + +(add_predicate is_process_instance instance process) +(add_predicate is_visible_in instance process entity) + +(add_predicate process_instance_maps instance process instance waveform waveform) diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile index 25d31cc..5f25d1a 100644 --- a/instance-calculator/Makefile +++ b/instance-calculator/Makefile @@ -5,8 +5,8 @@ MODEL_DIR = endif #### Where to store the Instance model -ifndef INSTANCE_MODEL_DIR -INSTANCE_MODEL_DIR = $(MODEL_DIR)/instance/ +ifndef MODEL_INSTANCES_DIR +MODEL_INSTANCES_DIR = endif #### Binaries @@ -25,8 +25,8 @@ ifeq ($(strip $(MODEL_DIR)),) $(error No MODEL_DIR defined as parameter.) endif -ifeq ($(strip $(INSTANCE_MODEL_DIR)),) -$(error No INSTANCE_MODEL_DIR defined as parameter.) +ifeq ($(strip $(MODEL_INSTANCES_DIR)),) +$(error No MODEL_INSTANCES_DIR defined as parameter.) endif ifeq ($(strip $(JAVA)),) @@ -44,12 +44,12 @@ CLASSPATH = "./src/" SOURCES = $(wildcard src/*.java) CLASSES = $(SOURCES:.java=.class) MODEL_FILE = $(MODEL_DIR)/structural.mod -OUTPUT_FILE = $(INSTANCE_MODEL_DIR)/instances.mod +OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/instances.mod ## Makefile Rules ############################################################## compile: $(CLASSES) -model: $(CLASSES) $(INSTANCE_MODEL_DIR) $(OUTPUT_FILE) +model: $(CLASSES) $(MODEL_INSTANCES_DIR) $(OUTPUT_FILE) solutions: @@ -67,8 +67,8 @@ clean_solutions: $(JAVAC) -cp $(CLASSPATH) $< $(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) - $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(INSTANCE_MODEL_DIR) + $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(MODEL_INSTANCES_DIR) -$(INSTANCE_MODEL_DIR): - mkdir -p $(INSTANCE_MODEL_DIR) +$(MODEL_INSTANCES_DIR): + mkdir -p $(MODEL_INSTANCES_DIR) diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 03e451a..8543ee4 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -95,7 +95,9 @@ MODEL_FILES = \ $(MODEL_DIR)/structural.mod \ $(MODEL_DIR)/depths.mod \ $(MODEL_DIR)/string_to_instr.map \ - $(filter-out %structural.mod,$(wildcard $(MODEL_DIR)/cfg_*.mod)) + $(wildcard $(MODEL_DIR)/cfg_*.mod) \ + $(MODEL_INSTANCES_DIR)/instances.mod \ + $(wildcard $(MODEL_INSTANCESDIR)/instances_in_*.mod) PARSER_SOURCES = $(wildcard parser/*.g4) PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class) -- cgit v1.2.3-70-g09d2 From 99bbe050e57c50c5c21b849c1721fe9979894d8f Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 30 Aug 2017 15:15:02 +0200 Subject: Reduces the scalability issue. It seems to take very long to find solutions for simple_flip_flop_instance, but at least it no longer gives up right away. --- Makefile | 2 +- data/level/instances.lvl | 13 ++-- data/property/simple_flip_flop_instance.pp | 6 ++ data/property/simple_flip_flop_instance.pro | 95 +++++++++++++++++++++++++++++ instance-calculator/Makefile | 7 ++- instance-calculator/src/Instances.java | 44 ------------- instance-calculator/src/Main.java | 1 - instance-calculator/src/VHDLProcess.java | 31 ++++++---- instance-calculator/src/VHDLWaveform.java | 30 ++++++--- instr-to-kodkod/Makefile | 3 +- 10 files changed, 157 insertions(+), 75 deletions(-) create mode 100644 data/property/simple_flip_flop_instance.pp create mode 100644 data/property/simple_flip_flop_instance.pro delete mode 100644 instance-calculator/src/Instances.java (limited to 'Makefile') diff --git a/Makefile b/Makefile index 4a18566..116e4ec 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml TMP_DIR = /tmp/tabellion MODEL_DIR = $(TMP_DIR)/mod -MODEL_INSTANCES_DIR = $(TMP_DIR)/instance +MODEL_INSTANCES_DIR = $(MODEL_DIR)/instance SOL_DIR = $(TMP_DIR)/sol ## Sub-programs ################################################################ diff --git a/data/level/instances.lvl b/data/level/instances.lvl index 5fdb42b..ad6e93f 100644 --- a/data/level/instances.lvl +++ b/data/level/instances.lvl @@ -3,7 +3,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_type instance) +(add_type wfm_instance) +(add_type ps_instance) ;; Redundancies (add_type entity) @@ -13,10 +14,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_waveform_instance instance waveform) -(add_predicate is_visible_in instance waveform entity) +(add_predicate is_wfm_instance_of wfm_instance waveform) +(add_predicate is_visible_in wfm_instance entity) -(add_predicate is_process_instance instance process) -(add_predicate is_visible_in instance process entity) +(add_predicate is_ps_instance_of ps_instance process) +(add_predicate is_visible_in ps_instance entity) -(add_predicate process_instance_maps instance process instance waveform waveform) +(add_predicate process_instance_maps ps_instance wfm_instance waveform) diff --git a/data/property/simple_flip_flop_instance.pp b/data/property/simple_flip_flop_instance.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/simple_flip_flop_instance.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/simple_flip_flop_instance.pro b/data/property/simple_flip_flop_instance.pro new file mode 100644 index 0000000..a3881aa --- /dev/null +++ b/data/property/simple_flip_flop_instance.pro @@ -0,0 +1,95 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (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) +;; debt: )) +;; Get ps instance +(exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) +;; debt: )) )) +;; Get a local waveform matching a clk instance +(exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) +;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) +;; debt: )))) )))) +;; Get a local waveform matching a reg instance +(exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) +;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) +;; debt: )))) )))))))) +;; Analyze ps using the local waveforms +(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" local_clk) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" local_clk) + (is_read_element "3" "=") + (or + (is_read_element "4" local_clk) + (is_read_element "5" local_clk) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (is_read_element "2" local_clk) + (is_read_element "3" local_clk) + ) + (is_read_element "4" "event") + (is_read_element "5" local_clk) + ) + ) + (EX + (and + (has_option "COND_WAS_TRUE") + (does_not_reach_parent_before + (and + (expr_writes local_reg) + (AX + (not + (EF + (expr_writes local_reg) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) +)))))))))))) diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile index 5f25d1a..9dddc88 100644 --- a/instance-calculator/Makefile +++ b/instance-calculator/Makefile @@ -44,7 +44,7 @@ CLASSPATH = "./src/" SOURCES = $(wildcard src/*.java) CLASSES = $(SOURCES:.java=.class) MODEL_FILE = $(MODEL_DIR)/structural.mod -OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/instances.mod +OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/witness ## Makefile Rules ############################################################## compile: $(CLASSES) @@ -55,10 +55,10 @@ solutions: clean: rm -f $(CLASSES) - rm -f $(PATH_MODEL_DIR)/*.mod + rm -f $(MODEL_INSTANCES_DIR)/* clean_model: - rm -f $(PATH_MODEL_DIR)/*.mod + rm -f $(MODEL_INSTANCES_DIR)/* clean_solutions: @@ -68,6 +68,7 @@ clean_solutions: $(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(MODEL_INSTANCES_DIR) + touch $(OUTPUT_FILE) $(MODEL_INSTANCES_DIR): mkdir -p $(MODEL_INSTANCES_DIR) diff --git a/instance-calculator/src/Instances.java b/instance-calculator/src/Instances.java deleted file mode 100644 index d4954d9..0000000 --- a/instance-calculator/src/Instances.java +++ /dev/null @@ -1,44 +0,0 @@ -import java.util.*; - -public class Instances -{ - private static final Map INSTANCES; - private static final OutputFile OUTPUT_FILE; - - static - { - INSTANCES = new HashMap(); - OUTPUT_FILE = OutputFile.new_output_file("instances.mod"); - } - - public static String get_id_for (final int i) - { - final Integer j; - String result; - - j = new Integer(i); - - result = INSTANCES.get(j); - - if (result == null) - { - result = (Main.get_parameters().get_id_prefix() + i); - - INSTANCES.put(j, result); - } - - return result; - } - - public static void write_predicates () - { - for (final String id: INSTANCES.values()) - { - OUTPUT_FILE.write("(add_element instance "); - OUTPUT_FILE.write(id); - OUTPUT_FILE.write(")"); - - OUTPUT_FILE.insert_newline(); - } - } -} diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java index a23da06..6fc950f 100644 --- a/instance-calculator/src/Main.java +++ b/instance-calculator/src/Main.java @@ -37,7 +37,6 @@ public class Main } create_instances(); - Instances.write_predicates(); OutputFile.close_all(); } diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index eba5e46..07bac2e 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -102,7 +102,6 @@ public class VHDLProcess result = new VHDLProcess.Instance ( - Instances.get_id_for(instances_count), this, visibility, iwfm_map @@ -115,6 +114,13 @@ public class VHDLProcess public static class Instance { + private static int instances_count; + + static + { + instances_count = 0; + } + private final String id; private final VHDLProcess parent; private final Map iwfm_map; @@ -122,13 +128,18 @@ public class VHDLProcess private Instance ( - final String id, final VHDLProcess parent, final VHDLEntity visibility, final Map iwfm_map ) { - this.id = id; + this.id = + ( + Main.get_parameters().get_id_prefix() + + "ps_" + + instances_count + ); + this.parent = parent; this.visibility = visibility; this.iwfm_map = iwfm_map; @@ -168,7 +179,6 @@ public class VHDLProcess result = new VHDLProcess.Instance ( - Instances.get_id_for(parent.instances_count), parent, visibility, new_iwfm_map @@ -187,7 +197,12 @@ public class VHDLProcess try { - of.write("(is_process_instance "); + of.write("(add_element ps_instance "); + of.write(id); + of.write(")"); + of.insert_newline(); + + of.write("(is_ps_instance_of "); of.write(id); of.write(" "); of.write(parent.get_id()); @@ -197,8 +212,6 @@ public class VHDLProcess of.write("(is_visible_in "); of.write(id); of.write(" "); - of.write(parent.get_id()); - of.write(" "); of.write(visibility.get_id()); of.write(")"); of.insert_newline(); @@ -212,12 +225,8 @@ public class VHDLProcess of.write("(process_instance_maps "); of.write(id); of.write(" "); - of.write(parent.get_id()); - of.write(" "); of.write(iwfm.getKey().get_id()); of.write(" "); - of.write(iwfm.getKey().get_parent().get_id()); - of.write(" "); of.write(iwfm.getValue().get_id()); of.write(")"); of.insert_newline(); diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java index 74edc88..89cf945 100644 --- a/instance-calculator/src/VHDLWaveform.java +++ b/instance-calculator/src/VHDLWaveform.java @@ -74,7 +74,6 @@ public class VHDLWaveform result = new VHDLWaveform.Instance ( - Instances.get_id_for(instances_count), this, visibility ); @@ -104,18 +103,32 @@ public class VHDLWaveform public static class Instance { + private static int instances_count; + + static + { + instances_count = 0; + } + private final String id; private final VHDLWaveform parent; private final VHDLEntity visibility; private Instance ( - final String id, final VHDLWaveform parent, final VHDLEntity visibility ) { - this.id = id; + this.id = + ( + Main.get_parameters().get_id_prefix() + + "wfm_" + + instances_count + ); + + instances_count += 1; + this.parent = parent; this.visibility = visibility; } @@ -134,7 +147,12 @@ public class VHDLWaveform { try { - of.write("(is_waveform_instance "); + of.write("(add_element wfm_instance "); + of.write(id); + of.write(")"); + of.insert_newline(); + + of.write("(is_wfm_instance_of "); of.write(id); of.write(" "); of.write(parent.get_id()); @@ -144,8 +162,6 @@ public class VHDLWaveform of.write("(is_visible_in "); of.write(id); of.write(" "); - of.write(parent.get_id()); - of.write(" "); of.write(visibility.get_id()); of.write(")"); of.insert_newline(); @@ -166,7 +182,7 @@ public class VHDLWaveform @Override public String toString () { - return "<" + parent.get_id() + ", " + id + ">"; + return id; } } } diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 8543ee4..1a36fae 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -96,8 +96,7 @@ MODEL_FILES = \ $(MODEL_DIR)/depths.mod \ $(MODEL_DIR)/string_to_instr.map \ $(wildcard $(MODEL_DIR)/cfg_*.mod) \ - $(MODEL_INSTANCES_DIR)/instances.mod \ - $(wildcard $(MODEL_INSTANCESDIR)/instances_in_*.mod) + $(wildcard $(MODEL_INSTANCES_DIR)/*.mod) PARSER_SOURCES = $(wildcard parser/*.g4) PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class) -- cgit v1.2.3-70-g09d2 From 3466690e0a13a145d8d1eef89eba3f962f9f6e2b Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Fri, 1 Sep 2017 15:58:25 +0200 Subject: Adds test cases for the issue. --- Makefile | 2 +- data/property/simple_flip_flop.pro | 1 + data/property/simple_flip_flop_instance.pp | 6 -- data/property/simple_flip_flop_instance.pro | 95 ----------------------------- data/property/test-case/fast.pp | 6 ++ data/property/test-case/fast.pro | 57 +++++++++++++++++ data/property/test-case/slow.pp | 6 ++ data/property/test-case/slow.pro | 60 ++++++++++++++++++ 8 files changed, 131 insertions(+), 102 deletions(-) delete mode 100644 data/property/simple_flip_flop_instance.pp delete mode 100644 data/property/simple_flip_flop_instance.pro create mode 100644 data/property/test-case/fast.pp create mode 100644 data/property/test-case/fast.pro create mode 100644 data/property/test-case/slow.pp create mode 100644 data/property/test-case/slow.pro (limited to 'Makefile') diff --git a/Makefile b/Makefile index 116e4ec..c5a5601 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,7 @@ ## Makefile Parameters ######################################################### LEVEL_FILES = $(wildcard ${CURDIR}/data/level/*.lvl) PROPERTY_FILES = \ - $(wildcard ${CURDIR}/data/property/*.pro) + $(wildcard ${CURDIR}/data/property/test-case/*.pro) # $(wildcard ${CURDIR}/data/property/cnes/*.pro) AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml #AST_FILE = ${CURDIR}/data/ast/pong.xml diff --git a/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro index e1621c1..b054c7f 100644 --- a/data/property/simple_flip_flop.pro +++ b/data/property/simple_flip_flop.pro @@ -5,6 +5,7 @@ (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) ) (and + (not (eq clk reg)) (is_explicit_process ps) (is_in_sensitivity_list clk ps) (CTL_verifies ps diff --git a/data/property/simple_flip_flop_instance.pp b/data/property/simple_flip_flop_instance.pp deleted file mode 100644 index b460eec..0000000 --- a/data/property/simple_flip_flop_instance.pp +++ /dev/null @@ -1,6 +0,0 @@ -The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, -line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the -process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), -controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, -c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, -l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/simple_flip_flop_instance.pro b/data/property/simple_flip_flop_instance.pro deleted file mode 100644 index a3881aa..0000000 --- a/data/property/simple_flip_flop_instance.pro +++ /dev/null @@ -1,95 +0,0 @@ -(tag_existing - ( - (ent entity STRUCT_ENTITY) - (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) -;; debt: )) -;; Get ps instance -(exists i_ps ps_instance - (and - (is_visible_in i_ps ent) - (is_ps_instance_of i_ps ps) -;; debt: )) )) -;; Get a local waveform matching a clk instance -(exists i_clk wfm_instance - (and - (process_instance_maps i_ps i_clk _) -;; (is_visible_in i_clk ent) - (is_wfm_instance_of i_clk clk) - (exists local_clk waveform - (and - (process_instance_maps i_ps i_clk local_clk) - (is_in_sensitivity_list local_clk ps) -;; debt: )))) )))) -;; Get a local waveform matching a reg instance -(exists i_reg wfm_instance - (and - (process_instance_maps i_ps i_reg _) -;; (is_visible_in i_reg ent) - (is_wfm_instance_of i_reg reg) - (exists local_reg waveform - (and - (process_instance_maps i_ps i_reg local_reg) -;; debt: )))) )))))))) -;; Analyze ps using the local waveforms -(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" local_clk) - ) - (and - (is_read_structure "(?(??)(???))") - (is_read_element "0" "and") - (is_read_element "1" "event") - (is_read_element "2" local_clk) - (is_read_element "3" "=") - (or - (is_read_element "4" local_clk) - (is_read_element "5" local_clk) - ) - ) - (and - (is_read_structure "(?(???)(??))") - (is_read_element "0" "and") - (is_read_element "1" "=") - (or - (is_read_element "2" local_clk) - (is_read_element "3" local_clk) - ) - (is_read_element "4" "event") - (is_read_element "5" local_clk) - ) - ) - (EX - (and - (has_option "COND_WAS_TRUE") - (does_not_reach_parent_before - (and - (expr_writes local_reg) - (AX - (not - (EF - (expr_writes local_reg) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) -)))))))))))) diff --git a/data/property/test-case/fast.pp b/data/property/test-case/fast.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/test-case/fast.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/test-case/fast.pro b/data/property/test-case/fast.pro new file mode 100644 index 0000000..10bc135 --- /dev/null +++ b/data/property/test-case/fast.pro @@ -0,0 +1,57 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) + (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) + ) + (and + (not (eq reg clk)) + (is_explicit_process ps) + ;; debt: )) + ;; Get ps instance + (exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) + ;; debt: )) )) + ;; Get a local waveform matching a clk instance + (exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) + ;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) + ;; debt: )))) )))) + ;; Get a local waveform matching a reg instance + (exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) + ;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) + ;; debt: )))) )))))))) + ;; Analyze ps using the local waveforms + (CTL_verifies ps + (AF + ;; using local_clk or local_reg here makes the property take forever to verify.... + (kind "if") + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/test-case/slow.pp b/data/property/test-case/slow.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/test-case/slow.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/test-case/slow.pro b/data/property/test-case/slow.pro new file mode 100644 index 0000000..2566a6f --- /dev/null +++ b/data/property/test-case/slow.pro @@ -0,0 +1,60 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) + (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) + ) + (and + (not (eq reg clk)) + (is_explicit_process ps) + ;; debt: )) + ;; Get ps instance + (exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) + ;; debt: )) )) + ;; Get a local waveform matching a clk instance + (exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) + ;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) + ;; debt: )))) )))) + ;; Get a local waveform matching a reg instance + (exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) + ;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) + ;; debt: )))) )))))))) + ;; Analyze ps using the local waveforms + (CTL_verifies ps + (AF + ;; using local_clk or local_reg here makes the property take forever to verify.... + (and + (kind "if") + (is_read_element "1" local_clk) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) -- cgit v1.2.3-70-g09d2 From 77838a1342b53ca97d842ef47ff91f44f6a5bbeb Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 18 Sep 2017 10:33:11 +0200 Subject: Go back to the usual default properties. --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c5a5601..a959838 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,8 @@ ## Makefile Parameters ######################################################### LEVEL_FILES = $(wildcard ${CURDIR}/data/level/*.lvl) PROPERTY_FILES = \ - $(wildcard ${CURDIR}/data/property/test-case/*.pro) -# $(wildcard ${CURDIR}/data/property/cnes/*.pro) + $(wildcard ${CURDIR}/data/property/*.pro) \ + $(wildcard ${CURDIR}/data/property/cnes/*.pro) AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml #AST_FILE = ${CURDIR}/data/ast/pong.xml -- cgit v1.2.3-70-g09d2