verf package#

Submodules#

verf.DynamicGraphTree module#

class verf.DynamicGraphTree.DynamicGraphTree(crossbar: MemristorCrossbar, specification: VerilogBenchmark)[source]#

Bases: TreeBasedEquivalenceChecker

to_formula(output_variable: str, input_function: str = '1') → Bool[source]#
class verf.DynamicGraphTree.Tree(graph: Graph, node, parent, path)[source]#

Bases: object

build()[source]#

verf.Enumeration module#

class verf.Enumeration.Enumeration(boolean_function: BooleanFunctionInterface, specification: BooleanFunctionInterface)[source]#

Bases: EquivalenceChecker

is_equivalent(sampling_size: int = 0) → bool[source]#
to_formula(output_variable: str) → Bool[source]#

verf.EquivalenceChecker module#

class verf.EquivalenceChecker.EquivalenceChecker(boolean_function: BooleanFunctionInterface, specification: BooleanFunctionInterface)[source]#

Bases: ABC

get_execution_time()[source]#
abstract is_equivalent(sampling_size: int = 0) → bool[source]#
abstract to_formula(output_variable: str) → Bool[source]#

verf.GraphBasedEquivalenceChecker module#

class verf.GraphBasedEquivalenceChecker.GraphBasedEquivalenceChecker(crossbar: MemristorCrossbar, specification: VerilogBenchmark)[source]#

Bases: EquivalenceChecker

abstract get_simple_paths(output_variable: str) → List[List[str]][source]#
is_equivalent(sampling_size: int = 0) → bool[source]#
abstract to_formula(output_variable: str) → Bool[source]#

verf.SimplePathTree module#

class verf.SimplePathTree.Color(value)[source]#

Bases: Enum

An enumeration.

black = 2#
gray = 1#
white = 0#
class verf.SimplePathTree.SimplePathTree(boolean_function: BooleanFunction, specification: BooleanFunction)[source]#

Bases: EquivalenceChecker

is_equivalent(sampling_size: int = -1) → bool[source]#

Based on: https://www.usna.edu/Users/cs/wcbrown/courses/S18SI335/lec/l15/lec.html DFSVisit(vertex u)

color u gray for each neighbor v of u do

if v is white

DFSVisit(v)

color u black

DFS(graph G)

set the color of all vertices in G to white for each vertex u in G do

if u is white

DFSVisit(u)

Parameters:

sampling_size –

Returns:

Returns true if and only if the given Boolean function and specification are equivalent.

to_formula(output_variable: str) → Bool[source]#

verf.StaticGraph module#

class verf.StaticGraph.StaticGraph(crossbar: MemristorCrossbar, specification: VerilogBenchmark)[source]#

Bases: GraphBasedEquivalenceChecker

get_simple_paths(output_variable: str) → List[List[str]][source]#
to_formula(output_variable: str, input_function: str = '1') → Bool[source]#

verf.StaticGraphTree module#

class verf.StaticGraphTree.StaticGraphTree(crossbar: MemristorCrossbar, specification: VerilogBenchmark)[source]#

Bases: TreeBasedEquivalenceChecker

to_formula(output_variable: str, input_function: str = '1') → Bool[source]#
class verf.StaticGraphTree.Tree(graph: Graph, node, visited, parent, path)[source]#

Bases: object

build()[source]#

verf.TreeBasedEquivalenceChecker module#

class verf.TreeBasedEquivalenceChecker.TreeBasedEquivalenceChecker(crossbar: MemristorCrossbar, specification: VerilogBenchmark)[source]#

Bases: GraphBasedEquivalenceChecker

get_simple_paths(output_variable: str) → List[List[str]][source]#
abstract to_formula(output_variable: str) → Bool[source]#

verf.XSAT module#

class verf.XSAT.SubProblem(subgraph: MultiGraph, literals: List[LITERAL])[source]#

Bases: object

class verf.XSAT.XSAT(crossbar: Crossbar, specification: BooleanFunctionInterface, node_threshold: int = 250, depth_threshold: int = 5)[source]#

Bases: EquivalenceChecker

get_log() → Dict[str, Any][source]#
is_equivalent(sampling_size: int = 0) → bool[source]#
to_formula(output_variable: str) → Bool[source]#

Module contents#