| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | data/level/instances.lvl | 13 | ||||
| -rw-r--r-- | data/property/simple_flip_flop_instance.pp | 6 | ||||
| -rw-r--r-- | data/property/simple_flip_flop_instance.pro | 95 | ||||
| -rw-r--r-- | instance-calculator/Makefile | 7 | ||||
| -rw-r--r-- | instance-calculator/src/Instances.java | 44 | ||||
| -rw-r--r-- | instance-calculator/src/Main.java | 1 | ||||
| -rw-r--r-- | instance-calculator/src/VHDLProcess.java | 31 | ||||
| -rw-r--r-- | instance-calculator/src/VHDLWaveform.java | 30 | ||||
| -rw-r--r-- | instr-to-kodkod/Makefile | 3 |
10 files changed, 157 insertions, 75 deletions
@@ -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<Integer, String> INSTANCES; - private static final OutputFile OUTPUT_FILE; - - static - { - INSTANCES = new HashMap<Integer, String>(); - 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<VHDLWaveform.Instance, VHDLWaveform> iwfm_map; @@ -122,13 +128,18 @@ public class VHDLProcess private Instance ( - final String id, final VHDLProcess parent, final VHDLEntity visibility, final Map<VHDLWaveform.Instance, VHDLWaveform> 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) |