From 70b40bfb6c032c0dead7069b2178a43e63a8e563 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 19 Jul 2017 10:29:52 +0200 Subject: First shot at the framework (it does compile). --- data/instructions/example_process.pl.kk | 88 +++++++++++++++++++++++ data/level/control_flow_level.data | 19 ----- data/level/control_flow_level.lvl | 24 +++++++ data/level/control_flow_level_kodkod.data | 14 ---- data/level/control_flow_level_kodkod.lvl | 17 +++++ data/level/structural_level.data | 112 ------------------------------ data/level/structural_level.lvl | 112 ++++++++++++++++++++++++++++++ data/property/unread_waveforms.pro | 10 +++ 8 files changed, 251 insertions(+), 145 deletions(-) create mode 100644 data/instructions/example_process.pl.kk delete mode 100644 data/level/control_flow_level.data create mode 100644 data/level/control_flow_level.lvl delete mode 100644 data/level/control_flow_level_kodkod.data create mode 100644 data/level/control_flow_level_kodkod.lvl delete mode 100644 data/level/structural_level.data create mode 100644 data/level/structural_level.lvl create mode 100644 data/property/unread_waveforms.pro (limited to 'data') diff --git a/data/instructions/example_process.pl.kk b/data/instructions/example_process.pl.kk new file mode 100644 index 0000000..c4f07b3 --- /dev/null +++ b/data/instructions/example_process.pl.kk @@ -0,0 +1,88 @@ +(add_element path p237_0) +(is_path_of p237_0 237) +(contains_node p237_0 262) +(is_before p237_0 262 263) +(contains_node p237_0 263) +(add_element path p237_1) +(is_path_of p237_1 262) +(contains_node p237_1 263) +(add_element path p237_2) +(is_path_of p237_2 237) +(contains_node p237_2 260) +(is_before p237_2 260 261) +(contains_node p237_2 261) +(add_element path p237_3) +(is_path_of p237_3 260) +(contains_node p237_3 261) +(add_element path p237_4) +(is_path_of p237_4 237) +(contains_node p237_4 258) +(is_before p237_4 258 259) +(contains_node p237_4 259) +(add_element path p237_5) +(is_path_of p237_5 258) +(contains_node p237_5 259) +(add_element path p237_6) +(is_path_of p237_6 237) +(contains_node p237_6 256) +(is_before p237_6 256 257) +(contains_node p237_6 257) +(add_element path p237_7) +(is_path_of p237_7 256) +(contains_node p237_7 257) +(add_element path p237_8) +(is_path_of p237_8 237) +(contains_node p237_8 254) +(is_before p237_8 254 255) +(contains_node p237_8 255) +(add_element path p237_9) +(is_path_of p237_9 254) +(contains_node p237_9 255) +(add_element path p237_10) +(is_path_of p237_10 237) +(contains_node p237_10 252) +(is_before p237_10 252 253) +(contains_node p237_10 253) +(add_element path p237_11) +(is_path_of p237_11 252) +(contains_node p237_11 253) +(add_element path p237_12) +(is_path_of p237_12 237) +(contains_node p237_12 250) +(is_before p237_12 250 251) +(contains_node p237_12 251) +(add_element path p237_13) +(is_path_of p237_13 250) +(contains_node p237_13 251) +(add_element path p237_14) +(is_path_of p237_14 237) +(contains_node p237_14 248) +(is_before p237_14 248 249) +(contains_node p237_14 249) +(add_element path p237_15) +(is_path_of p237_15 248) +(contains_node p237_15 249) +(add_element path p237_16) +(is_path_of p237_16 237) +(contains_node p237_16 246) +(is_before p237_16 246 247) +(contains_node p237_16 247) +(add_element path p237_17) +(is_path_of p237_17 246) +(contains_node p237_17 247) +(add_element path p237_18) +(is_path_of p237_18 237) +(contains_node p237_18 244) +(is_before p237_18 244 245) +(contains_node p237_18 245) +(add_element path p237_19) +(is_path_of p237_19 244) +(contains_node p237_19 245) +(add_element path p237_20) +(is_path_of p237_20 237) +(contains_node p237_20 239) +(is_before p237_20 239 242) +(contains_node p237_20 242) +(add_element path p237_21) +(is_path_of p237_21 239) +(contains_node p237_21 242) diff --git a/data/level/control_flow_level.data b/data/level/control_flow_level.data deleted file mode 100644 index a7cc9c0..0000000 --- a/data/level/control_flow_level.data +++ /dev/null @@ -1,19 +0,0 @@ -;; Control Flow Level - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(add_type node) -(add_type node_depth) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_start_node node process) -(add_predicate has_kind node string) -(add_predicate has_option node string) -(add_predicate has_depth node node_depth) -(add_predicate node_connect node node) -(add_predicate expr_writes node waveform) -(add_predicate expr_reads node waveform) diff --git a/data/level/control_flow_level.lvl b/data/level/control_flow_level.lvl new file mode 100644 index 0000000..516f9ef --- /dev/null +++ b/data/level/control_flow_level.lvl @@ -0,0 +1,24 @@ +;; Control Flow Level + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type node) +(add_type node_depth) + +;; Redundancies +(add_type process) +(add_type string) +(add_type waveform) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_start_node node process) +(add_predicate has_kind node string) +(add_predicate has_option node string) +(add_predicate has_depth node node_depth) +(add_predicate node_connect node node) +(add_predicate expr_writes node waveform) +(add_predicate expr_reads node waveform) diff --git a/data/level/control_flow_level_kodkod.data b/data/level/control_flow_level_kodkod.data deleted file mode 100644 index ed11735..0000000 --- a/data/level/control_flow_level_kodkod.data +++ /dev/null @@ -1,14 +0,0 @@ -;; Control Flow Level, Kodkod additions - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(add_type path) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_path_of path node) -(add_predicate contains_node path node) -(add_predicate is_before path node node) diff --git a/data/level/control_flow_level_kodkod.lvl b/data/level/control_flow_level_kodkod.lvl new file mode 100644 index 0000000..949f69f --- /dev/null +++ b/data/level/control_flow_level_kodkod.lvl @@ -0,0 +1,17 @@ +;; Control Flow Level, Kodkod additions + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type path) + +;; Redundancies +(add_type node) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_path_of path node) +(add_predicate contains_node path node) +(add_predicate is_before path node node) diff --git a/data/level/structural_level.data b/data/level/structural_level.data deleted file mode 100644 index 75c4ac9..0000000 --- a/data/level/structural_level.data +++ /dev/null @@ -1,112 +0,0 @@ -;; Structural Level - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(add_type entity) -(add_type port) -(add_type port_mode) -(add_type generic) -(add_type architecture) -(add_type signal) -(add_type process) -(add_type file) -(add_type component) -(add_type waveform) -(add_type string) -(add_type type) -(add_type type_kind) -(add_type signal_kind) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;;; Entity ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_in_file entity file) -(add_predicate has_begin entity) -(add_predicate has_visible_flag entity) -(add_predicate end_has_reserved_id entity) -(add_predicate end_has_identifier entity) -(add_predicate is_simulation_scenario entity) - -;;;; Port ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_port_of port entity) -(add_predicate has_disconnect_flag port) -(add_predicate is_of_mode port string) -(add_predicate has_class port) -(add_predicate is_ref port) -(add_predicate has_active_flag port) -(add_predicate has_identifier_list port) -(add_predicate has_visible_flag port) -(add_predicate has_after_drivers_flag port) -(add_predicate has_use_flag port) -(add_predicate has_open_flag port) -(add_predicate has_guarded_signal_flag port) -(add_predicate is_of_kind port string) - -;;;; Generic ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_generic_of generic entity) -(add_predicate has_class generic) -(add_predicate is_ref generic) -(add_predicate has_identifier_list generic) -(add_predicate has_visible_flag generic) -(add_predicate has_after_drivers_flag generic) -(add_predicate is_of_type generic type) - -;;;; File ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_in_file architecture file) -(add_predicate is_architecture_of architecture entity) -(add_predicate has_foreign_flag architecture) -(add_predicate has_visible_flag architecture) -(add_predicate is_within_flag architecture) -(add_predicate end_has_reserved_id architecture) -(add_predicate end_has_identifier architecture) - -;;;; Signal ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate belongs_to_architecture signal architecture) -(add_predicate has_disconnect_flag signal) -(add_predicate is_ref signal) -(add_predicate has_active_flag signal) -(add_predicate has_identifier_list signal) -(add_predicate has_visible_flag signal) -(add_predicate has_after_drivers signal) -(add_predicate has_use_flag signal) -(add_predicate has_open_flag signal) -(add_predicate has_guarded_flag signal) -(add_predicate is_of_kind signal string) -(add_predicate is_of_type signal type) - -;;;; Process ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate belongs_to_architecture process architecture) -(add_predicate has_seen_flag process) -(add_predicate end_has_postboned process) -(add_predicate has_postboned_flag process) -(add_predicate is_ref process) -(add_predicate has_passive_flag process) -(add_predicate has_visible_flag process) -(add_predicate is_within_flag process) -(add_predicate has_label process) -(add_predicate has_is process) -(add_predicate end_has_reserved_id process) -(add_predicate end_has_identifier process) -(add_predicate is_explicit_process process) - -;;;; Component ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_component_of component entity) -(add_predicate belongs_to_architecture component architecture) -(add_predicate port_maps component waveform port) - -;;;; Waveform ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_in_sensitivity_list waveform process) -(add_predicate is_accessed_by waveform process) -(add_predicate is_waveform_of waveform signal) -(add_predicate is_waveform_of waveform port) - -;;;; String ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate string_matches string string) - -;;;; Type ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_approved_type type) -(add_predicate is_of_kind type string) diff --git a/data/level/structural_level.lvl b/data/level/structural_level.lvl new file mode 100644 index 0000000..75c4ac9 --- /dev/null +++ b/data/level/structural_level.lvl @@ -0,0 +1,112 @@ +;; Structural Level + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type entity) +(add_type port) +(add_type port_mode) +(add_type generic) +(add_type architecture) +(add_type signal) +(add_type process) +(add_type file) +(add_type component) +(add_type waveform) +(add_type string) +(add_type type) +(add_type type_kind) +(add_type signal_kind) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;;; Entity ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_in_file entity file) +(add_predicate has_begin entity) +(add_predicate has_visible_flag entity) +(add_predicate end_has_reserved_id entity) +(add_predicate end_has_identifier entity) +(add_predicate is_simulation_scenario entity) + +;;;; Port ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_port_of port entity) +(add_predicate has_disconnect_flag port) +(add_predicate is_of_mode port string) +(add_predicate has_class port) +(add_predicate is_ref port) +(add_predicate has_active_flag port) +(add_predicate has_identifier_list port) +(add_predicate has_visible_flag port) +(add_predicate has_after_drivers_flag port) +(add_predicate has_use_flag port) +(add_predicate has_open_flag port) +(add_predicate has_guarded_signal_flag port) +(add_predicate is_of_kind port string) + +;;;; Generic ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_generic_of generic entity) +(add_predicate has_class generic) +(add_predicate is_ref generic) +(add_predicate has_identifier_list generic) +(add_predicate has_visible_flag generic) +(add_predicate has_after_drivers_flag generic) +(add_predicate is_of_type generic type) + +;;;; File ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_in_file architecture file) +(add_predicate is_architecture_of architecture entity) +(add_predicate has_foreign_flag architecture) +(add_predicate has_visible_flag architecture) +(add_predicate is_within_flag architecture) +(add_predicate end_has_reserved_id architecture) +(add_predicate end_has_identifier architecture) + +;;;; Signal ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate belongs_to_architecture signal architecture) +(add_predicate has_disconnect_flag signal) +(add_predicate is_ref signal) +(add_predicate has_active_flag signal) +(add_predicate has_identifier_list signal) +(add_predicate has_visible_flag signal) +(add_predicate has_after_drivers signal) +(add_predicate has_use_flag signal) +(add_predicate has_open_flag signal) +(add_predicate has_guarded_flag signal) +(add_predicate is_of_kind signal string) +(add_predicate is_of_type signal type) + +;;;; Process ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate belongs_to_architecture process architecture) +(add_predicate has_seen_flag process) +(add_predicate end_has_postboned process) +(add_predicate has_postboned_flag process) +(add_predicate is_ref process) +(add_predicate has_passive_flag process) +(add_predicate has_visible_flag process) +(add_predicate is_within_flag process) +(add_predicate has_label process) +(add_predicate has_is process) +(add_predicate end_has_reserved_id process) +(add_predicate end_has_identifier process) +(add_predicate is_explicit_process process) + +;;;; Component ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_component_of component entity) +(add_predicate belongs_to_architecture component architecture) +(add_predicate port_maps component waveform port) + +;;;; Waveform ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_in_sensitivity_list waveform process) +(add_predicate is_accessed_by waveform process) +(add_predicate is_waveform_of waveform signal) +(add_predicate is_waveform_of waveform port) + +;;;; String ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate string_matches string string) + +;;;; Type ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_approved_type type) +(add_predicate is_of_kind type string) diff --git a/data/property/unread_waveforms.pro b/data/property/unread_waveforms.pro new file mode 100644 index 0000000..b53862b --- /dev/null +++ b/data/property/unread_waveforms.pro @@ -0,0 +1,10 @@ +(tag_existing + ( + (wf waveform UNREAD_WAVEFORM) + ) + (not + (exists ps process + (is_accessed_by wf ps) + ) + ) +) -- cgit v1.2.3-70-g09d2