Application Scheme

An application scheme describes the order in which the individual operations of both circuits are applied during the equivalence check.

In case of the alternating equivalence checker, this is the key component to allow the intermediate decision diagrams to remain close to the identity (as proposed in [2]). See Verifying the Results of Compilation Flows for more information on the dedicated application scheme for verifying compilation flow results (as proposed in [9]).

In case of the other checkers, which consider both circuits individually, using a non-sequential application scheme can significantly boost the operation caching performance in the underlying decision diagram package.

ApplicationSchemeName

alias of Literal[‘sequential’, ‘one_to_one’, ‘proportional’, ‘lookahead’, ‘gate_cost’]

class ApplicationScheme

Members:

sequential : Applies all gates from the first circuit, before proceeding with the second circuit. Referred to as reference in [2].

one_to_one : Alternates between applications from the first and the second circuit. Referred to as naive in [2].

proportional : For every gate of the first circuit, proportionally many are applied from the second circuit according to the difference in the number of gates.

lookahead : Looks whether an application from the first circuit or the second circuit yields the smaller decision diagram. Only works for the alternating checker.

gate_cost : Each gate of the first circuit is associated with a corresponding cost according to some cost function f(…). Whenever a gate g from the first circuit is applied f(g) gates are applied from the second circuit. Referred to as compilation_flow in [9].

gate_cost = <ApplicationScheme.gate_cost: 3>

lookahead = <ApplicationScheme.lookahead: 2>

property name

one_to_one = <ApplicationScheme.one_to_one: 1>

proportional = <ApplicationScheme.proportional: 4>

sequential = <ApplicationScheme.sequential: 0>

property value