Source code for verf.DynamicGraphTree

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, parent, path): self.graph = graph self.node = node self.parent = parent self.parent_literal = None self.path = path self.children = dict()
[docs] def build(self): graph = self.graph # self.plot(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) for key in outgoing_edges.keys(): subgraph = graph.copy() outgoing_edge = outgoing_edges[key] literal = outgoing_edge["literal"] subgraph.remove_node(current_node) # Edges with negated selectorlines negated_edges = [(u, v, k) for u, v, k, d in subgraph.edges(data=True, keys=True) if d['literal'] == literal.negate()] # Remove edges with negated selectorlines for (u, v, k) in negated_edges: subgraph.remove_edge(u, v, k) # Edges with idempotent (same) selectorlines idempotent_edges = [(u, v, k) for u, v, k, d in subgraph.edges(data=True, keys=True) if d['literal'] == literal] while len(idempotent_edges) != 0: (u, v, k) = idempotent_edges[0] # We cannot remove the neighbor node, considering we loop over the neighbors if u == neighbor_node: victim = v victim_prime = u else: victim = u victim_prime = v victim_attr = subgraph.nodes[victim] # If the victim is an output node, we pass this property to the node into which the victim merges if victim_attr["output"]: subgraph.nodes[victim_prime]["output"] = True subgraph_copy = subgraph.copy() # Let u be the victim, i.e. the node to be removed such that all its edges are connected to v victim_neighbors = list(subgraph_copy.neighbors(victim)) subgraph_copy.remove_node(victim) for victim_neighbor in victim_neighbors: if victim_neighbor != victim_prime: outgoing_edges_sub = subgraph.get_edge_data(victim, victim_neighbor) for key_sub in outgoing_edges_sub.keys(): outgoing_edge_sub = outgoing_edges_sub[key_sub] literal_sub = outgoing_edge_sub["literal"] subgraph_copy.add_edge(victim_neighbor, victim_prime, literal=literal_sub) idempotent_edges = [(x, y, k) for x, y, k, d in subgraph_copy.edges(data=True, keys=True) if d['literal'] == literal] subgraph = subgraph_copy # The neighbor node has the output property. Hence, we can terminate this path # if subgraph.nodes[neighbor_node]["output"]: path = self.path.copy() path.append(literal) tree_child = Tree(subgraph, neighbor_node, self, path) tree_child.parent_literal = literal if neighbor_node in self.children: self.children[neighbor_node].append({"output": subgraph.nodes[neighbor_node]["output"], "path": path, "subtree": tree_child}) else: self.children[neighbor_node] = [{"output": subgraph.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 DynamicGraphTree(TreeBasedEquivalenceChecker): def __init__(self, crossbar: MemristorCrossbar, specification: VerilogBenchmark): super().__init__(crossbar, specification) config.log.add("Verification method: CHECK\n") config.log.add("Static/dynamic: dynamic\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) input_layer, input_nanowire = self.boolean_function.get_input_nanowire(input_function) output_layer, output_nanowire = self.boolean_function.get_output_nanowire(output_variable) # Verify whether the required input nanowire and output nanowire are in the graph if "L{}_{}".format(input_layer, input_nanowire) not in graph.nodes or "L{}_{}".format(output_layer, output_nanowire) not in graph.nodes: self.trees[output_variable] = None return False attrs = dict() # TODO: All input nanowires for l in range(self.boolean_function.layers + 1): if l % 2 == 0: for r in range(self.boolean_function.rows): if l == input_layer and r == input_nanowire: attrs["L{}_{}".format(l, r)] = {"output": True} else: attrs["L{}_{}".format(l, r)] = {"output": False} else: for c in range(self.boolean_function.columns): if l == input_layer and c == input_nanowire: attrs["L{}_{}".format(l, c)] = {"output": True} else: attrs["L{}_{}".format(l, c)] = {"output": False} networkx.set_node_attributes(graph, attrs) # Start a breadth-first search on a dynamic graph start_node = "L{}_{}".format(output_layer, output_nanowire) # For the dynamic graph, we use a tree for bookkeeping tree = Tree(graph, start_node, 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)