Merge pull request #97 from MortezaRezaalipour/94-using-constants-for…

…-left-shift

Now constants are enabled through an argument

sxpat/config/config.py

@@ -57,6 +57,7 @@
 APPROXIMATE_OUTPUT_PREFIX = 'a'
 OUT = 'out'
 PRODUCT_PREFIX = 'p_o'
+CONSTANT_PREFIX = 'p_c'
 
 TO_Z3_GATE_DICT = {
     NOT: Z3_NOT,

sxpat/specifications.py

@@ -25,6 +25,9 @@ class TemplateType(enum.Enum):
     NON_SHARED = 'nonshared'
     SHARED = 'shared'
 
+class ConstantsType(enum.Enum):
+    NEVER = 'never'
+    ALWAYS = 'always'
 
 class EnumChoicesAction(argparse.Action):
     def __init__(self, *args, type: enum.Enum, **kwargs) -> None:
@@ -59,6 +62,7 @@ class Specifications:
     subxpat: bool
     template: TemplateType
     encoding: EncodingType
+    constants: ConstantsType
     wanted_models: int
     iteration: int = dc.field(init=False, default=None)  # rw
     # exploration (2)
@@ -217,6 +221,11 @@ def parse_args(cls):
                                     default=1,
                                     help='Wanted number of models to generate for each step')
 
+        _consts = parser.add_argument('--constants',
+                                      type=ConstantsType,
+                                      action=EnumChoicesAction,
+                                      default=ConstantsType.NEVER,
+                                      help='The way constants are used')
         # > error stuff
 
         _et = parser.add_argument('--max-error', '-e',

sxpat/synthesis.py

@@ -16,7 +16,7 @@
 from .annotatedGraph import AnnotatedGraph
 from .config import paths as sxpatpaths
 from .config import config as sxpatconfig
-from .specifications import Specifications, TemplateType
+from .specifications import Specifications, TemplateType, ConstantsType
 
 
 class Synthesis:
@@ -42,7 +42,7 @@ def __init__(self, template_specs: Specifications, graph_obj: AnnotatedGraph = N
         if json_obj == sxpatconfig.UNSAT or json_obj == sxpatconfig.UNKNOWN:
             pprint.error('ERROR!!! the json does not contain any models!')
         else:
-            self.__json_model: json = json_obj
+            self.__json_model: List[Dict] = json_obj
             self.__num_models = self.get_num_models_from_json(json_obj)
 
             self.__use_json_model: bool = None
@@ -366,25 +366,41 @@ def __json_model_lpp_and_subgraph_output_assigns(self, idx: int = 0):
 
         return lpp_assigns
 
-    def __intact_part_assigns(self):
-        intact_part = f'// intact gates assigns\n'
-        for n_idx in self.graph.constant_dict.keys():
-            n = self.graph.constant_dict[n_idx]
+    def __json_model_output_constants_assign(self, idx: int = 0):
+        model = self.json_model[idx]
 
-            sn = list(self.graph.graph.successors(n))
-            Value = self.graph.graph.nodes[n][LABEL]
+        text = '//json model constants rewrites\n'
+        for out_id, out_name in self.graph.output_dict.items():
+            out_pred = next(self.graph.graph.predecessors(out_name))
+            out_parameter = f'{sxpatconfig.CONSTANT_PREFIX}{out_id}'
 
-            if Value.upper() == 'FALSE':
-                Value = "1'b0"
-            else:
-                Value = "1'b1"
+            has_const = out_pred in self.graph.constant_dict.values()
+            has_parameter = out_parameter in model
+            assert has_const == has_parameter, f'Output `{out_name}` must be preceded by a constant if and only if it has a constant parameter'
+
+            if has_const:  # or has_parameter # they are equivalent
+                text += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{out_pred} = {self.verilog_bool_const(model[out_parameter])};\n'
+
+        return text
 
-            intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n} = {Value};\n'
+    def __intact_part_assigns(self):
+        intact_part = f'// intact gates assigns\n'
 
-        for n_idx in self.graph.graph_intact_gate_dict.keys():
-            n = self.graph.graph_intact_gate_dict[n_idx]
-            pn = list(self.graph.graph.predecessors(n))
-            gate = self.graph.graph.nodes[n][LABEL]
+        # write constants that are not output constants
+        for n_idx, n_name in self.graph.constant_dict.items():
+            const_succs = list(self.graph.graph.successors(n_name))
+            if len(const_succs) == 1 and const_succs[0] in self.graph.output_dict.values() and self.specs.constants == ConstantsType.ALWAYS:
+                # skip if it is a constant output
+                continue
+
+            value: str = self.graph.graph.nodes[n_name][LABEL]
+            value = f"1'b{'0' if value.upper() == 'FALSE' else '1'}"
+            intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n_name} = {value};\n'
+
+        #
+        for n_idx, n_name in self.graph.graph_intact_gate_dict.items():
+            pn = list(self.graph.graph.predecessors(n_name))
+            gate = self.graph.graph.nodes[n_name][LABEL]
             for idx, el in enumerate(pn):
                 if (
                     (el in list(self.graph.input_dict.values()) and el not in list(self.graph.subgraph_input_dict.values()))
@@ -395,47 +411,54 @@ def __intact_part_assigns(self):
                     pn[idx] = f'{sxpatconfig.VER_WIRE_PREFIX}{el}'
 
             if len(pn) == 1:
-                intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n} = {sxpatconfig.VER_NOT}{pn[0]};\n'
+                intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n_name} = {sxpatconfig.VER_NOT}{pn[0]};\n'
             elif len(pn) == 2:
                 if gate == sxpatconfig.AND:
 
-                    intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n} = ' \
+                    intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n_name} = ' \
                                    f'{pn[0]} {sxpatconfig.VER_AND} ' \
                                    f'{pn[1]};\n'
                 elif gate == sxpatconfig.OR:
-                    intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n} = ' \
+                    intact_part += f'{sxpatconfig.VER_ASSIGN} {sxpatconfig.VER_WIRE_PREFIX}{n_name} = ' \
                                    f'{pn[0]} {sxpatconfig.VER_OR} ' \
                                    f'{pn[1]};\n'
             else:
-                pprint.error(f'ERROR!!! node {n} has more than two drivers!')
+                pprint.error(f'ERROR!!! node {n_name} has more than two drivers!')
                 exit(1)
 
         return intact_part
 
     def __output_assigns(self):
         output_assigns = f'// output assigns\n'
 
-        for n in self.graph.output_dict.values():
-            pn = list(self.graph.graph.predecessors(n))
-            gate = self.graph.graph.nodes[n][LABEL]
+        for out_name in self.graph.output_dict.values():
 
-            if len(pn) == 1:
+            preds = list(self.graph.graph.predecessors(out_name))
+            gate = self.graph.graph.nodes[out_name][LABEL]
+
+            # output is a rewritten expression
+            if len(preds) == 1:
                 if gate == sxpatconfig.NOT:
-                    output_assigns += f'{sxpatconfig.VER_ASSIGN} {n} = {sxpatconfig.VER_NOT}{sxpatconfig.VER_WIRE_PREFIX}{pn[0]};\n'
+                    # NOTE: this block is reached when an output node is also a gate, but this should never be the case.
+                    raise Exception('The code entered a block that should never have reached. (synthesis.__output_assigns if1)')
+                    output_assigns += f'{sxpatconfig.VER_ASSIGN} {out_name} = {sxpatconfig.VER_NOT}{sxpatconfig.VER_WIRE_PREFIX}{preds[0]};\n'
                 else:
-                    if pn[0] in list(self.graph.input_dict.values()) and pn[0] not in list(self.graph.subgraph_input_dict.values()):
-                        output_assigns += f'{sxpatconfig.VER_ASSIGN} {n} = {pn[0]};\n'
+                    if preds[0] in list(self.graph.input_dict.values()) and preds[0] not in list(self.graph.subgraph_input_dict.values()):
+                        output_assigns += f'{sxpatconfig.VER_ASSIGN} {out_name} = {preds[0]};\n'
                     else:
-                        output_assigns += f'{sxpatconfig.VER_ASSIGN} {n} = {sxpatconfig.VER_WIRE_PREFIX}{pn[0]};\n'
-            elif len(pn) == 2:
+                        output_assigns += f'{sxpatconfig.VER_ASSIGN} {out_name} = {sxpatconfig.VER_WIRE_PREFIX}{preds[0]};\n'
+
+            elif len(preds) == 2:
+                # NOTE: this block is reached when an output node is also a gate, but this should never be the case.
+                raise Exception('The code entered a block that should never have reached. (synthesis.__output_assigns if2)')
                 if gate == sxpatconfig.AND:
-                    output_assigns += f'{sxpatconfig.VER_ASSIGN}  = ' \
-                                      f'{sxpatconfig.VER_WIRE_PREFIX}{pn[0]} {sxpatconfig.VER_AND} ' \
-                                      f'{sxpatconfig.VER_WIRE_PREFIX}{pn[1]};\n'
+                    output_assigns += f'{sxpatconfig.VER_ASSIGN} {out_name} = ' \
+                                      f'{sxpatconfig.VER_WIRE_PREFIX}{preds[0]} {sxpatconfig.VER_AND} ' \
+                                      f'{sxpatconfig.VER_WIRE_PREFIX}{preds[1]};\n'
                 elif gate == sxpatconfig.OR:
-                    output_assigns += f'{sxpatconfig.VER_ASSIGN}  = ' \
-                                      f'{sxpatconfig.VER_WIRE_PREFIX}{pn[0]} {sxpatconfig.VER_OR} ' \
-                                      f'{sxpatconfig.VER_WIRE_PREFIX}{pn[1]};\n'
+                    output_assigns += f'{sxpatconfig.VER_ASSIGN} {out_name} = ' \
+                                      f'{sxpatconfig.VER_WIRE_PREFIX}{preds[0]} {sxpatconfig.VER_OR} ' \
+                                      f'{sxpatconfig.VER_WIRE_PREFIX}{preds[1]};\n'
 
         output_assigns += f'{sxpatconfig.VER_ENDMODULE}'
         return output_assigns
@@ -466,7 +489,7 @@ def __intact_gate_wires(self):
             intact_wires += f'{sxpatconfig.VER_WIRE} '
             for gate_idx, gate in enumerate(constant_intact_gate_list):
                 if gate_idx == len(constant_intact_gate_list) - 1:
-                    intact_wires += f'{sxpatconfig.VER_WIRE_PREFIX}{gate};'
+                    intact_wires += f'{sxpatconfig.VER_WIRE_PREFIX}{gate};\n'
                 else:
                     intact_wires += f'{sxpatconfig.VER_WIRE_PREFIX}{gate}, '
 
@@ -686,10 +709,27 @@ def __annotated_graph_to_verilog_shared(self):
             shared_assigns = self.__shared_logic_assigns_subxpat_shared(idx=idx)
             output_assigns = self.__output_assigns()
 
-            ver_str += (module_signature + io_declaration + intact_wires + annotated_graph_input_wires + json_input_wires
-                        + annotated_graph_input_wires + annotated_graph_output_wires + json_output_wires + json_model_wires)
-            ver_str += (json_input_assign + subgraph_to_json_input_mapping + intact_assigns
-                        + json_model_and_subgraph_outputs_assigns + shared_assigns + output_assigns)
+            #
+            json_model_constants_rewrite = self.__json_model_output_constants_assign(idx) if self.specs.constants == ConstantsType.ALWAYS else ''
+
+            ver_str += (
+                module_signature
+                + io_declaration
+                + intact_wires
+                + annotated_graph_input_wires
+                + json_input_wires
+                + annotated_graph_input_wires
+                + annotated_graph_output_wires
+                + json_output_wires
+                + json_model_wires
+                + json_input_assign
+                + subgraph_to_json_input_mapping
+                + intact_assigns
+                + json_model_and_subgraph_outputs_assigns
+                + shared_assigns
+                + json_model_constants_rewrite
+                + output_assigns
+            )
 
             ver_string.append(ver_str)
 
@@ -736,15 +776,24 @@ def __annotated_graph_to_verilog(self) -> List[AnyStr]:
             # 10. json_model_and_subgraph_outputs_assigns
             json_model_and_subgraph_outputs_assigns = self.__json_model_lpp_and_subgraph_output_assigns(idx)
 
+            #
+            json_model_constants_rewrite = self.__json_model_output_constants_assign(idx) if self.specs.constants == ConstantsType.ALWAYS else ''
+
             # 11. the intact assigns
             intact_assigns = self.__intact_part_assigns()
 
             # 12. output assigns
             output_assigns = self.__output_assigns()
 
-            assigns = subgraph_inputs_assigns + subgraph_to_json_input_mapping + json_model_and_subgraph_outputs_assigns + intact_assigns + output_assigns
-
             # assignments
+            assigns = (
+                subgraph_inputs_assigns
+                + subgraph_to_json_input_mapping
+                + json_model_and_subgraph_outputs_assigns
+                + json_model_constants_rewrite
+                + intact_assigns
+                + output_assigns
+            )
 
             # endmodule
             ver_str = module_signature + io_declaration + wire_declarations + assigns
@@ -819,6 +868,13 @@ def __magraph_to_verilog(self):
 
     # =========================
 
+    @staticmethod
+    def verilog_bool_const(value: bool) -> str:
+        assert isinstance(value, bool), 'value must be boolean'
+        return f"1'b{int(value)}"
+
+    # =========================
+
     def estimate_area(self, this_path: str = None):
         if this_path:
             design_path = this_path

sxpat/template_manager/template_manager.py

@@ -14,7 +14,7 @@
 from sxpat.annotatedGraph import AnnotatedGraph
 import sxpat.config.config as sxpat_cfg
 import sxpat.config.paths as sxpat_paths
-from sxpat.specifications import EncodingType, Specifications, TemplateType
+from sxpat.specifications import EncodingType, Specifications, TemplateType, ConstantsType
 from .encoding import Encoding
 from sxpat.utils.collections import mapping_inv, pairwise_iter
 
@@ -238,7 +238,12 @@ def _use_approx_var(self, node_name: str) -> str:
 
         # is constant
         if node_name in self.current_constants.values():
-            return sxpat_cfg.Z3_GATES_DICTIONARY[self._current_graph.graph.nodes[node_name][sxpat_cfg.LABEL]]
+            succs = list(self._current_graph.graph.successors(node_name))
+            if len(succs) == 1 and succs[0] in self._current_graph.output_dict.values() and self._specs.constants == ConstantsType.ALWAYS:
+                output_i = mapping_inv(self._current_graph.output_dict, succs[0])
+                return f'{sxpat_cfg.CONSTANT_PREFIX}{output_i}'
+            else:
+                return sxpat_cfg.Z3_GATES_DICTIONARY[self._current_graph.graph.nodes[node_name][sxpat_cfg.LABEL]]
 
         # is gate
         if node_name in self.current_gates.values():
@@ -287,6 +292,14 @@ def _generate_product(self, parameter_pair_gen: Callable[[int], Tuple[str, str]]
             multiplexers.append(f'Or(Not({p_s}), {p_l} == {(input_name)})')
         return f'And({", ".join(multiplexers)})'
 
+    def _generate_constants_parameters(self) -> Iterable[str]:
+        def get_single_predecessor(out_name): return next(self._current_graph.graph.predecessors(out_name))
+        return (
+            f'{sxpat_cfg.CONSTANT_PREFIX}{output_i}'
+            for output_i, output_name in self.outputs.items()
+            if get_single_predecessor(output_name) in self.current_constants.values()
+        )
+
     #
 
     def _update_builder(self, builder: Builder) -> None:
@@ -444,10 +457,14 @@ def _update_builder(self, builder: Builder) -> None:
 
         # params_declaration and params_list
         params = list(itertools.chain(
+            # constant outputs
+            self._generate_constants_parameters() if self._specs.constants == ConstantsType.ALWAYS else (),
+            # output parameters
             (
                 self._output_parameter(output_i)
                 for output_i in self.subgraph_outputs.keys()
             ),
+            # input parameters
             itertools.chain.from_iterable(
                 self._input_parameters(output_i, product_i, input_i)
                 for output_i in self.subgraph_outputs.keys()
@@ -587,16 +604,21 @@ def _update_builder(self, builder: Builder) -> None:
 
         # params_declaration and params_list
         params = list(itertools.chain(
-            (  # p_o#
+            # constant outputs
+            self._generate_constants_parameters(),
+            # p_o#
+            (
                 self._output_parameter(output_i)
                 for output_i in self.subgraph_outputs.keys()
             ),
-            itertools.chain.from_iterable(  # p_pr#_i#
+            # p_pr#_i#
+            itertools.chain.from_iterable(
                 self._input_parameters(None, product_i, input_i)
                 for product_i in range(self._specs.pit)
                 for input_i in self.subgraph_inputs.keys()
             ),
-            (  # p_pr#_o#
+            # p_pr#_o#
+            (
                 self._product_parameter(output_i, product_i)
                 for output_i in self.subgraph_outputs.keys()
                 for product_i in range(self._specs.pit)