Overall architecture update

.gitignore

@@ -17,10 +17,12 @@
 /*.sh
 
 #> generated
+/venv
 /.venv
 **/__pycache__
 **/yosys_graph.log
 **/yosys_log.txt
+.history_sta
 # input
 /input/*
 !/input/ver.bak

Makefile

@@ -2,6 +2,7 @@
 
 PY := python3
 ENV_NAME := .venv
+DELETION_DELAY ?= 10
 
 # computed
 
@@ -18,7 +19,7 @@ help:
 
 activate:
 	# warning: will not work (limitation of `make`), you need to run it manually
-	. $(ENV_NAME)/bin/activate
+	$(ACTIV_ENV)
 
 py_init:
 	@echo "\n[[ creating python environment if absent ]]"
@@ -29,22 +30,25 @@ py_dep: py_init
 	$(IN_ENV) python3 -m pip install --upgrade pip
 	$(IN_ENV) pip install --upgrade -r requirements.txt
 
-local_dep:
-	@echo "\n[[ generating local files ]]"
-	mkdir -p input/ver/ && cp -r input/ver.bak/* input/ver/
+setup: py_init py_dep
 
-setup: py_init py_dep local_dep
+rm_data:
+	@echo "\n[[   deleting all final and intermediary data   ]]\n[[ YOU HAVE $(DELETION_DELAY) SECONDS TO CANCEL THIS OPERATION ]]"
+	@sleep $(DELETION_DELAY)
+	rm -rf output/ test/
 
 rm_cache:
 	@echo "\n[[ removing all pycache folders ]]"
 	find . -name __pycache__ -prune -print -exec rm -rf {} \;
 
 rm_temp:
 	@echo "\n[[ removing generated temporary files ]]"
-	rm -f yosys_graph.log
+	rm -f yosys_graph.log .history_sta
 
 rm_pyenv:
 	@echo "\n[[ removing the virtual python environment ]]"
 	rm -rf $(ENV_NAME)
 
-clean: rm_pyenv rm_cache rm_temp
+clean: rm_cache rm_temp
+
+clean-all: rm_pyenv rm_data clean

README.md

@@ -34,7 +34,6 @@ To prepare the system for execution you will need to follow a few steps:
     # individual commands
     make py_init     # create python environment
     make py_dep      # install/update requirements
-    make local_dep   # create input folders and local files
     ```
 
 2. Activate the python environment:
@@ -47,13 +46,15 @@ To prepare the system for execution you will need to follow a few steps:
 
 - To remove temporary files and the virtual python environment:
     ```bash
-    # all together
-    make clean
-
     # individually
     make rm_cache # remove the pycache folders
     make rm_temp  # remove temporary files
     make rm_pyenv # remove the virtual python environment
+    make rm_data  # remove the output results
+
+    # all together
+    make clean     # rm_cache, rm_temp
+    make clean-all # clean, rm_pyenv, rm_data
     ```
 
 - To display the program help:
@@ -69,63 +70,74 @@ SubXPAT is used by running the following command:
 python3 main.py exact-benchmark [options]
 ```
 
+### Arguments
+
 Here are all the parameters with their arguments and descriptions:
-| **parameter**                                 | **argument**                         | **default value**                  | **description**                                                        |
-| :-------------------------------------------: | ------------------------------------ | ---------------------------------- | ---------------------------------------------------------------------- |
-| `exact-benchmark`                             | Verilog file in `input/ver/`         |                                    | Circuit to approximate                                                 |
-| `--current-benchmark` <br> `--curr`           | Verilog file in `input/ver/`         | the same as <br> `exact-benchmark` | Approximated circuit used to continue the execution                    |
-| `--max-labeling`                              |                                      |                                    | Nodes are weighted using their maximum error, instead of minimum error |
-| `--no-partial-labeling`                       |                                      |                                    | Weights are assigned to all nodes, not only the relevant ones          |
-| `--extraction-mode` <br> `--mode`             | { 1, 2, 3, 4, 5, 55, 6, 11, 12 }     | 55                                 | Subgraph extraction algorithm to use                                   |
-| `--input-max` <br> `--imax`                   | `int` > 0                            |                                    | Maximum allowed number of inputs to the subgraph                       |
-| `--output-max` <br> `--omax`                  | `int` > 0                            |                                    | Maximum allowed number of outputs from the subgraph                    |
-| `--max-sensitivity`                           | `int` > 0                            |                                    | Maximum partitioning sensitivity                                       |
-| `--min-subgraph-size`                         | `int` > 0                            |                                    | Minimum valid size for the subgraph                                    |
-| `--num-subgraphs`                             | `int` > 0                            | 1                                  | The number of attempts for subgraph extraction                         |
-| `--slash-to-kill`                             |                                      |                                    | Enable the slash pass for the first iteration                          |
-| `--error-for-slash`                           | `int` > 0                            |                                    | The error to use for the slash pass                                    |
-| `--subxpat`                                   |                                      |                                    | Run SubXPAT iteratively, instead of standard XPAT                      |
-| `--constants`                                 | { never, always }                    | always                             | Usage of constants                                                     |
-| `--template`                                  | { nonshared, shared }                | nonshared                          | Template logic                                                         |
-| `--max-lpp` <br> `--max-literals-per-product` | `int` > 0                            |                                    | The maximum number of literals per product                             |
-| `--max-ppo` <br> `--max-products-per-output`  | `int` > 0                            |                                    | The maximum number of products per output                              |
-| `--max-pit` <br> `--products-in-total`        | `int` > 0                            |                                    | The maximum number of products in total                                |
-| `--wanted-models`                             | `int` > 0                            | 1                                  | Wanted number of models to generate at each step                       |
-| `--max-error` <br> `-e`                       | `int` > 0                            |                                    | The maximum allowable error                                            |
-| `--error-partitioning` <br> `--epar`          | { asc, desc, smart_asc, smart_desc } | asc                                | The error partitioning algorithm to use                                |
-| `--encoding`                                  | { z3int, z3bvec, qbf }               | z3bvec                             | The encoding to use in solving                                         |
-| `--cell-library`                              |                                      | `config/gscl45nm.lib`              | The cell library file to use in the metrics estimation                 |
-| `--timeout`                                   | `float` > 0                          | 10800 (3h)                         | The maximum time each cell is given to run (in seconds)                |
-| `--parallel`                                  |                                      |                                    | Run in parallel whenever possible                                      |
-| `--clean`                                     |                                      |                                    | Reset the output folder before running                                 |
-| `--help` <br> `-h`                            |                                      |                                    | Show the help message and exit                                         |
 
+| **parameter**                                 | **argument**                            | **default value**                  | **description**                                                        |
+| :-------------------------------------------: | --------------------------------------- | ---------------------------------- | ---------------------------------------------------------------------- |
+| `exact-benchmark`                             | `path` to Verilog file                  |                                    | Circuit to approximate                                                 |
+| `--current-benchmark` <br> `--curr`           | `path` to Verilog file                  | the same as <br> `exact-benchmark` | Approximated circuit used to continue the execution                    |
+| `--max-labeling`                              |                                         |                                    | Nodes are weighted using their maximum error, instead of minimum error |
+| `--no-partial-labeling`                       |                                         |                                    | Weights are assigned to all nodes, not only the relevant ones          |
+| `--extraction-mode` <br> `--mode`             | { 1, 2, 3, 4, 5, 55, 6, 11, 12, 42 }    | 55                                 | Subgraph extraction algorithm to use                                   |
+| `--input-max` <br> `--imax`                   | `int` > 0                               |                                    | Maximum allowed number of inputs to the subgraph                       |
+| `--output-max` <br> `--omax`                  | `int` > 0                               |                                    | Maximum allowed number of outputs from the subgraph                    |
+| `--max-sensitivity`                           | `int` > 0                               |                                    | Maximum partitioning sensitivity                                       |
+| `--min-subgraph-size`                         | `int` > 0                               |                                    | Minimum valid size for the subgraph                                    |
+| `--num-subgraphs`                             | `int` > 0                               | 1                                  | The number of attempts for subgraph extraction                         |
+| `--slash-to-kill`                             |                                         |                                    | Enable the slash pass for the first iteration                          |
+| `--error-for-slash`                           | `int` > 0                               |                                    | The error to use for the slash pass                                    |
+| `--subxpat`                                   |                                         |                                    | Run SubXPAT iteratively, instead of standard XPAT                      |
+| `--constants`                                 | { never, always }                       | always                             | Usage of constants                                                     |
+| `--constant-false`                            | { output, product }                     | output                             | Representation of false constants from the subgraph                    |
+| `--template`                                  | { nonshared, shared }                   | nonshared                          | Template logic                                                         |
+| `--max-lpp` <br> `--max-literals-per-product` | `int` > 0                               |                                    | The maximum number of literals per product                             |
+| `--max-ppo` <br> `--max-products-per-output`  | `int` > 0                               |                                    | The maximum number of products per output                              |
+| `--max-pit` <br> `--products-in-total`        | `int` > 0                               |                                    | The maximum number of products in total                                |
+| `--wanted-models`                             | `int` > 0                               | 1                                  | Wanted number of models to generate at each step                       |
+| `--encoding`                                  | { z3int, z3bvec, z3dint, z3dbvec, qbf } | z3bvec                             | The encoding to use in solving                                         |
+| `--max-error` <br> `-e`                       | `int` > 0                               |                                    | The maximum allowable error                                            |
+| `--error-partitioning` <br> `--epar`          | { asc, desc, smart_asc, smart_desc }    | asc                                | The error partitioning algorithm to use                                |
+| `--output`                                    | `path` to folder                        | `output/`                          | The base directory for the output                                      |
+| `--cell-library`                              | `path` to lib file                      | `config/gscl45nm.lib`              | The cell library file to use in the metrics estimation                 |
+| `--archive`                                   |                                         |                                    | If the generated files should be archived at the end of the execution  |
+| `--debug`                                     |                                         | 10800 (3h)                         | The maximum time each cell is given to run (in seconds)                |
+| `--timeout`                                   | `float` > 0                             | 10800 (3h)                         | The maximum time each cell is given to run (in seconds)                |
+| `--parallel`                                  |                                         |                                    | Run in parallel whenever possible                                      |
+| `--help` <br> `-h` `-?`                       |                                         |                                    | Show the help message and exit                                         |
+
+### Results
+
+Once a command is finished executing, you can find the outputs in the `output/{#ID}/` folder, where `#ID` is a unique id assigned to the run, printed at the beginning of the execution.
+
+Inside the `output/{#ID}/` folder, the structure is as follow:
+- `run_details.csv`: the file containing the run specifications, such as arguments and global timings
+- `run_stats.csv`: the file containing details for every step of the execution
+- `verilog/`: the folder containing all generated circuits in Verilog format
+
+If the `--debug` flag is used, more folders will be available:
+- `graphviz/`: the folder containing a visual representation of the selected subgraph of each iteration
+- `scripts/`: the folder containing generated solver scripts
+- `tmp/`: the folder containing other temporary or intermediate products
 
 ### Examples
 
 To execute the framework with the XPAT algorithm in the standard configuration, run the following command:
 ```bash
-python3 main.py adder_i8_o5 --max-lpp=8 --max-ppo=32 --max-error=16
+python3 main.py benchmarks/v/adder_i8_o5.v --max-lpp=8 --max-ppo=32 --max-error=16
 ```
 
 To execute the framework with SubXPAT iterations, bit-vector logic encoding, and the defaults, run the following command:
 ```bash
-python3 main.py adder_i8_o5 --subxpat --encoding=z3bvec --max-lpp=8 --max-ppo=10 --imax=6 --omax=3 --max-error=16
+python3 main.py benchmarks/v/adder_i8_o5.v --subxpat --encoding=z3bvec --max-lpp=8 --max-ppo=10 --imax=6 --omax=3 --max-error=16
 ```
 
 To execute the framework with SubXPAT iterations, integer logic encoding, subgraph extraction mode 5 (all sub-outputs weight must be less than the error threshold), maximum labeling, ..., run the following command:
 ```bash
-python3 main.py adder_i8_o5 --subxpat --encoding=z3int --extraction-mode=5 --max-labeling --max-lpp=8 --max-ppo=10 --max-error=16 --imax=2 --omax=8
+python3 main.py benchmarks/v/adder_i8_o5.v --subxpat --encoding=z3int --extraction-mode=5 --max-labeling --max-lpp=8 --max-ppo=10 --max-error=16 --imax=2 --omax=8
 ```
 
-
-Once a command is finished executing, you can find the outputs in the following directories:
-
-`output/csv/` contains the log of execution and all information for each iteration.
-`output/ver/` contains the Verilog descriptions of all the approximate circuits found.
-`output/gv/` contains the information of all the subgraphs that have been selected, in a visual form.
-
-
 ## Known limitations
 
 - On Apple devices running M# architecture, you will have problems with some packages. \

Z3Log_patched/__init__.py

@@ -0,0 +1 @@
+

Z3Log_patched/argument.py

@@ -0,0 +1,4 @@
+# discarded:
+# from Z3Log.argument import Arguments
+
+raise RuntimeError('[DEPRECATED] talk with Marco if you need this')

Z3Log_patched/config/__init__.py

@@ -0,0 +1 @@
+

Z3Log_patched/config/config.py

@@ -0,0 +1,2 @@
+# not patched:
+from Z3Log.config.config import *

Z3Log_patched/config/path.py

@@ -0,0 +1,7 @@
+# discarded:
+# from Z3Log.config.path import INPUT_PATH
+# from Z3Log.config.path import OUTPUT_PATH
+# from Z3Log.config.path import TEST_PATH
+# from Z3Log.config.path import LOG_PATH
+
+raise RuntimeError('[DEPRECATED] talk with Marco if you need this')

Z3Log_patched/graph.py

@@ -0,0 +1,64 @@
+from typing import Mapping
+
+from .utils import get_pure_name
+
+# patched:
+from Z3Log.graph import Graph as _Graph
+
+__all__ = ['Graph']
+
+
+class Graph(_Graph):
+    def __init__(self, circuit_in_gv_path: str, is_clean: bool = False):
+        """
+        takes in a circuit and creates a networkx graph out of it
+        :param benchmark_name: the input benchmark in gv format
+        :param is_clean: leave empty for now
+        """
+
+        # reduced
+        self.__graph_name = get_pure_name(circuit_in_gv_path)
+        self.__graph_out_path = circuit_in_gv_path
+
+        self.__graph = self.import_graph()
+
+        self.__sorted_node_list = None
+        self.__is_clean = is_clean
+
+        if not self.is_clean:
+            self.clean_graph()
+            self.sort_graph()
+
+        self.remove_output_outgoing_edges()
+
+        self.__input_dict = self.sort_dict(self.extract_inputs())
+        self.__output_dict = self.sort_dict(self.extract_outputs())
+        self.__gate_dict = self.sort_dict(self.extract_gates())
+        self.__constant_dict = self.sort_dict(self.extract_constants())
+
+        self.__num_inputs = len(self.__input_dict)
+        self.__num_outputs = len(self.__output_dict)
+        self.__num_gates = len(self.__gate_dict)
+        self.__num_constants = len(self.__constant_dict)
+
+    @property
+    def in_path(self): raise RuntimeError('[DEPRECATED] talk with Marco if you need this')
+    @property
+    def verilog_in_path(self): raise RuntimeError('[DEPRECATED] talk with Marco if you need this')
+    @property
+    def dot_in_path(self): raise RuntimeError('[DEPRECATED] talk with Marco if you need this')
+
+    def sort_dict(self, mapping: Mapping) -> dict:
+        sorted_keys = sorted(mapping.keys())
+        return {k: mapping[k] for k in sorted_keys}
+
+    def __repr__(self):
+        return (
+            f'An object of class Graph\n'
+            f'{self.name = }\n'
+            # f'{self.in_path = }\n'
+            f'{self.out_path = }\n'
+            f'{self.num_inputs = }\n'
+            f'{self.num_outputs = }\n'
+            f'{self.num_gates = }\n'
+        )

Z3Log_patched/result.py

@@ -0,0 +1,4 @@
+# discarded:
+# from Z3Log.result import Result
+
+raise RuntimeError('[DEPRECATED] talk with Marco if you need this')

Z3Log_patched/specs.py

@@ -0,0 +1,5 @@
+# discarded:
+# from Z3Log.specs import Specs
+
+
+raise RuntimeError('[DEPRECATED] talk with Marco if you need this')

Z3Log_patched/stats.py

@@ -0,0 +1,4 @@
+# discarded:
+# from Z3Log.stats import Stats
+
+raise RuntimeError('[DEPRECATED] talk with Marco if you need this')