Source code for verf.StaticGraphTree
import networkx
from networkx import MultiGraph, Graph
from z3 import Not, Bool, Or, And
from utils import config
from core.benchmarks.Benchmark import VerilogBenchmark
from core.expressions.BooleanExpression import LITERAL
from core.hardware.Crossbar import MemristorCrossbar
from verf.TreeBasedEquivalenceChecker import TreeBasedEquivalenceChecker
[docs]
class Tree:
def __init__(self, graph: Graph, node, visited, parent, path):
self.graph = graph
self.node = node
self.parent = parent
self.parent_literal = None
self.path = path
self.visited = visited
self.visited.add(node)
self.children = dict()
[docs]
def build(self):
graph = self.graph
current_node = self.node
# Consider all the neighboring nodes of the current node
for neighbor_node in graph.neighbors(current_node):
outgoing_edges = graph.get_edge_data(current_node, neighbor_node)
if neighbor_node in self.visited:
continue
for key in outgoing_edges.keys():
outgoing_edge = outgoing_edges[key]
literal = outgoing_edge["literal"]
path = self.path.copy()
path.append(literal)
tree_child = Tree(self.graph, neighbor_node, self.visited.copy(), self, path)
tree_child.parent_literal = literal
if neighbor_node in self.children:
self.children[neighbor_node].append({"output": self.graph.nodes[neighbor_node]["output"], "path": path, "subtree": tree_child})
else:
self.children[neighbor_node] = [{"output": self.graph.nodes[neighbor_node]["output"], "path": path, "subtree": tree_child}]
for child_key in self.children.keys():
child_nodes = self.children[child_key]
for child_node in child_nodes:
if not child_node["output"]:
child_node["subtree"].build()
[docs]
class StaticGraphTree(TreeBasedEquivalenceChecker):
def __init__(self, crossbar: MemristorCrossbar, specification: VerilogBenchmark):
super().__init__(crossbar, specification)
config.log.add("Verification method: CHECK\n")
config.log.add("Static/dynamic: static\n")
[docs]
def to_formula(self, output_variable: str, input_function: str = "1") -> Bool:
assert isinstance(self.boolean_function, MemristorCrossbar)
# Construct a bipartite graph where the rows and columns are nodes, and the intersections are edges.
graph = MultiGraph()
for layer in range(self.boolean_function.layers):
for r in range(self.boolean_function.rows):
for c in range(self.boolean_function.columns):
memristor = self.boolean_function.get_memristor(r, c, layer)
if memristor.literal != LITERAL('False', False):
if layer % 2 == 0:
graph.add_edge("L_{}_{}".format(layer, r), "L_{}_{}".format(layer + 1, c),
literal=memristor.literal)
else:
graph.add_edge("L_{}_{}".format(layer, c), "L_{}_{}".format(layer + 1, r),
literal=memristor.literal)
# for r in range(self.crossbar.rows):
# for c in range(self.crossbar.columns):
# memristor = self.crossbar.get_memristor(r, c)
# if memristor.literal != LITERAL('False', False):
# graph.add_edge("R{}".format(r), "C{}".format(c), literal=memristor.literal)
input_layer, input_nanowire = self.boolean_function.get_input_nanowire(input_function)
output_layer, output_nanowire = self.boolean_function.get_output_nanowire(output_variable)
start_node = "L_{}_{}".format(output_layer, output_nanowire)
end_node = "L_{}_{}".format(input_layer, input_nanowire)
# # Verify whether the required input nanowire and output nanowire are in the graph
# Verify whether the required input nanowire and output nanowire are in the graph
if start_node not in graph.nodes or end_node not in graph.nodes:
return False
# if "R{}".format(self.crossbar.input_nanowires[input_nanowire]) not in graph.nodes or "R{}".format(self.crossbar.output_nanowires[output_variable]) not in graph.nodes:
# return False
attrs = dict()
# TODO: All input nanowires
for layer in range(self.boolean_function.layers + 1):
if layer % 2 == 0:
for r in range(self.boolean_function.rows):
if r == self.boolean_function.get_input_nanowire(input_function)[1]:
attrs["L_{}_{}".format(layer, r)] = {"output": True}
else:
attrs["L_{}_{}".format(layer, r)] = {"output": False}
else:
for c in range(self.boolean_function.columns):
attrs["L_{}_{}".format(layer, c)] = {"output": False}
networkx.set_node_attributes(graph, attrs)
# for r in range(self.crossbar.rows):
# if r == self.crossbar.get_input_nanowire(input_function)[1]:
# attrs["R{}".format(r)] = {"output": True}
# else:
# attrs["R{}".format(r)] = {"output": False}
# for c in range(self.crossbar.columns):
# attrs["C{}".format(c)] = {"output": False}
# networkx.set_node_attributes(graph, attrs)
# Start a breadth-first search on a dynamic graph
# start_node = "R{}".format(self.crossbar.output_nanowires[output_variable])
# For the dynamic graph, we use a tree for bookkeeping
tree = Tree(graph, start_node, set(), None, [])
tree.build()
self.trees[output_variable] = tree
return self._to_z3_formula(tree)
def _to_z3_formula(self, tree: Tree) -> Bool:
# Recursively build up the Boolean formula
child_expressions = []
for child_nodes in tree.children.values():
for child_node in child_nodes:
if child_node["output"]:
literal = child_node["subtree"].parent_literal
if literal != LITERAL("True", True):
if literal.positive:
child_expressions.append(Bool(literal.atom))
else:
child_expressions.append(Not(Bool(literal.atom)))
else:
child_expressions.append(True)
else:
child_expressions.append(self._to_z3_formula(child_node["subtree"]))
subtree_expression = Or(*child_expressions)
if tree.parent_literal is None:
return subtree_expression
else:
literal = tree.parent_literal
if literal != LITERAL("True", True):
if literal.positive:
literal_expression = Bool(literal.atom)
else:
literal_expression = Not(Bool(literal.atom))
else:
literal_expression = True
return And(literal_expression, subtree_expression)