Functionality

class Configuration.Functionality

Options for all checkers that consider the whole functionality of a circuit.

property trace_threshold

While decision diagrams are canonical in theory, i.e., equivalent circuits produce equivalent decision diagrams, numerical inaccuracies and approximations can harm this property. This can result in a scenario where two decision diagrams are really close to one another, but cannot be identified as such by standard methods (i.e., comparing their root pointers). Instead, for two decision diagrams U and U' representing the functionalities of two circuits G and G', the trace of the product of one decision diagram with the inverse of the other can be computed and compared to the trace of the identity. Alternatively, it can be checked, whether U*U`^-1 is “close enough” to the identity by recursively checking that each decision diagram node is close enough to the identity structure (i.e., the first and last successor have weights close to one, while the second and third successor have weights close to zero). Whenever any decision diagram node differs from this structure by more than the configured threshold, the circuits are concluded to be non-equivalent. Defaults to 1e-8.