# 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’]

classApplicationScheme¶Members:

sequential : Applies all gates from the first circuit, before proceeding with the second circuit. Referred to as

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

naivein [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 gategfrom the first circuit is appliedf(g)gates are applied from the second circuit. Referred to ascompilation_flowin [9].

- gate_cost
= <ApplicationScheme.gate_cost: 3>¶

- lookahead
= <ApplicationScheme.lookahead: 2>¶

propertyname¶

- one_to_one
= <ApplicationScheme.one_to_one: 1>¶

- proportional
= <ApplicationScheme.proportional: 4>¶

- sequential
= <ApplicationScheme.sequential: 0>¶

propertyvalue¶