initial commit

.gitignore

@@ -0,0 +1,135 @@
+# vscode
+.vscode
+
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+pip-wheel-metadata/
+share/python-wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+#  Usually these files are written by a python script from a template
+#  before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.nox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+*.py,cover
+.hypothesis/
+.pytest_cache/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+local_settings.py
+db.sqlite3
+db.sqlite3-journal
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# IPython
+profile_default/
+ipython_config.py
+
+# pyenv
+.python-version
+
+# pipenv
+#   According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
+#   However, in case of collaboration, if having platform-specific dependencies or dependencies
+#   having no cross-platform support, pipenv may install dependencies that don't work, or not
+#   install all needed dependencies.
+#Pipfile.lock
+
+# PEP 582; used by e.g. github.com/David-OConnor/pyflow
+__pypackages__/
+
+# Celery stuff
+celerybeat-schedule
+celerybeat.pid
+
+# SageMath parsed files
+*.sage.py
+
+# Environments
+.env
+.venv
+env/
+venv/
+ENV/
+env.bak/
+venv.bak/
+
+# Spyder project settings
+.spyderproject
+.spyproject
+
+# Rope project settings
+.ropeproject
+
+# mkdocs documentation
+/site
+
+# mypy
+.mypy_cache/
+.dmypy.json
+dmypy.json
+
+# Pyre type checker
+.pyre/
+
+brahma/
+brahma/*

example.py

@@ -0,0 +1,4 @@
+from main import create_module_from_constrain
+
+constrain = lambda O, I1_1, I2_2: O == (I1_1 & I2_2) + 1
+print(create_module_from_constrain(constrain))

main.py

@@ -0,0 +1,35 @@
+from preprocessing import list_function_inputs, get_oldest_references_from_lambda
+from postprocessing import generate_systemverilog
+import brahma
+
+# Example Usage
+
+
+def create_module_from_constrain(constrain):
+    inputs = list_function_inputs(constrain)
+    def svname(init_name):
+        if init_name.find("_") != -1:
+            name, offset = init_name.split("_")
+            return name + f"_reg[{offset}]"
+        else:
+            return init_name
+
+    def id2name(ident: int) -> str:
+        if ident < len(inputs) - 1: 
+            return svname(inputs[ident + 1])
+        else :
+            return f'v{ident - len(inputs) + 2}'
+
+    synth = brahma.Synthesizer(len(inputs) - 1, constrain)
+    res = synth.synthesize_shortest()
+    prog = []
+    n = 0
+    for ident, instr in enumerate(res.instructions):
+        if instr.reached :
+            n  = ident
+            print(ident)
+            prog.append(f'    v{ident} = ' + instr.component.expression(*map(id2name, instr.args), res.model))
+
+    prog.append(f"    O = v{ident}")
+
+    return generate_systemverilog(prog, get_oldest_references_from_lambda(constrain))

postprocessing.py

@@ -0,0 +1,62 @@
+def generate_systemverilog(
+    program_body, 
+    inputs,
+    module_name="GeneratedModule",
+    bit_width=32
+):
+    """
+    Generates a SystemVerilog template with loop-based shift registers and always_comb for logic.
+
+    Args:
+        synthesized_program (str): The synthesized program as a lambda function string.
+        module_name (str): Name of the generated SystemVerilog module.
+        bit_width (int): Bit width for inputs, outputs, and registers.
+
+    Returns:
+        str: A SystemVerilog template code as a string.
+    """
+    # Parse inputs and the body from the synthesized program
+    # Example: "lambda I1_1, I1_2: (I1_1 & I1_2) - 1"
+
+    # Generate input declarations
+    input_declarations = "\n".join([f"    input logic [{bit_width-1}:0] {base_name};" for base_name in inputs if base_name != "O"])
+
+    # Generate shift register logic using loops
+    shift_logic = []
+    for base_name, max_offset in inputs.items():
+        if max_offset > 0:
+            shift_logic.append(f"    logic [{bit_width-1}:0] {base_name}_reg [1:{max_offset}];")
+            shift_logic.append(
+                f"    always_ff @(posedge clk) begin\n"
+                f"        for (int i = {max_offset}; i > 1; i = i - 1) begin\n"
+                f"            {base_name}_reg[i] <= {base_name}_reg[i-1];\n"
+                f"        end\n"
+                f"        {base_name}_reg[1] <= {base_name};\n"
+                f"    end"
+            )
+
+    # Generate output logic in always_comb
+    output_declaration = f"    output logic [{bit_width-1}:0] O;"
+    comb_logic = "\n".join(program_body)
+
+    output_logic = f"""
+    always_comb begin
+{comb_logic}
+    end
+    """
+
+    # SystemVerilog module template
+    sv_template = f"""
+module {module_name} (
+    input logic clk,
+{input_declarations}
+{output_declaration}
+);
+
+{("\n   ".join(shift_logic))}
+
+{output_logic.strip()}
+
+endmodule
+"""
+    return sv_template.strip()

preprocessing.py

@@ -0,0 +1,69 @@
+import ast
+import inspect
+import z3
+import brahma
+
+
+def list_function_inputs(func):
+    """
+    Lists the input parameters of a given Python function.
+    
+    Args:
+        func (function): The Python function to inspect.
+    
+    Returns:
+        list: A list of strings representing the input parameter names.
+    """
+    if not callable(func):
+        raise ValueError("The provided argument is not a function.")
+    
+    # Get the signature of the function
+    signature = inspect.signature(func)
+    
+    # Extract the parameter names
+    inputs = [param.name for param in signature.parameters.values()
+              if param.kind in (param.POSITIONAL_OR_KEYWORD, param.KEYWORD_ONLY)]
+    
+    return inputs
+
+def get_oldest_references_from_lambda(func):
+    """
+    Extracts the oldest values referenced for each variable from a lambda function.
+
+    Args:
+        func (callable): A lambda function, such as (lambda I1_1, I1_2: (I1_1 & I1_2) - 1).
+
+    Returns:
+        dict: A dictionary where keys are variable names (e.g., "I1") and values are the oldest indices referenced.
+    """
+    # Get the source code of the lambda function
+    source = inspect.getsource(func).strip()
+    
+    # Parse the source code into an AST
+    tree = ast.parse(source)
+    
+    # Extract the lambda function node (should be the first node in the body)
+    lambda_node = tree.body[0].value
+
+    # Dictionary to store the oldest reference for each variable
+    oldest_references = {}
+
+    class ReferenceVisitor(ast.NodeVisitor):
+        def visit_Name(self, node):
+            # Check if the variable matches the naming pattern (e.g., I1_1, I1_2, etc.)
+            if "_" in node.id:
+                name, index = node.id.rsplit("_", 1)
+                if index.isdigit():
+                    index = int(index)
+                    if name not in oldest_references or index > oldest_references[name]:
+                        oldest_references[name] = index
+            else:
+                if node.id not in oldest_references:
+                    oldest_references[node.id] = 0
+
+    # Visit the AST nodes to extract variable references
+    ReferenceVisitor().visit(lambda_node)
+
+    return oldest_references
+
+

requirements.txt

@@ -0,0 +1,2 @@
+brahma
+z3