Automatic variable ordering
The CIF databased synthesis toolâ€™s predefined initial variable orders are often not optimal performancewise. Manually specifying a custom order often requires specialist knowledge and can take quite some time. Luckily, there are algorithms that can automatically compute a decent variable order.
The algorithms all take an existing variable order as input, and try to improve it using a fast heuristic. Some algorithms search for a local optimum. A better input variable order may then result in a better final variable order (a better local optimum), and may also speed up the automatic variable ordering algorithm itself (reaching an optimum faster). Other algorithms search for a global optimum. However, the algorithms are all based on heuristics. The guarantees that they provide differ, but none of them guarantees that synthesis will actually be quicker. In practice however, using such algorithms can significantly improve synthesis performance, especially for larger and more complex models.
For the initial variable ordering, the CIF variables and location pointers may be arbitrarily interleaved. If an automatic variable ordering algorithm changes the initial order, no synthesis variables are interleaved, except for each old variable with its corresponding new variable.
The automatic variable ordering algorithms are not applied if the CIF model has less than two synthesis variables, as with zero variables there is nothing to order, and with one variable there is only one possible order. They are also not applied if the model has no guards, updates, or other predicates from which to derive relations between the variables. Without such relations, the algorithms lack the required input to search for improved variable orders.
Variable relations
The variable relations serve as input for the algorithms. Different algorithms may use different representations of the variable relations. One such representation is hyperedges, and another is graph edges, which are derived from the hyperedges.
For basic configuration, the variable relations that are used to construct the hyperedges can be configured using the BDD hyperedge creation algorithm option (see the options section). By default, the Default relations are used. The following variable relations can be used:

Legacy
The legacy hyperedge creator creates the following hyperedges:

Per invariant, a hyperedge for the variables that occur in the invariant.

Per edge in an automaton, per guard, per comparison binary expression, a hyperedge for the variables that occur in the binary expression.

Per assignment, a hyperedge for the variables that occur in the addressable and value of the assignment.

Per event, a hyperedge for the variables that occur in the guards and updates of all edges for that event in the entire specification.


Linearized
The linearized hyperedge creator creates the following hyperedges:

Per linearized edge, a hyperedge for the variables that occur in the guards and updates of that linearized edge. State/event exclusion invariants are taken into account, by first converting them to automata.


Default
Uses the linearized hyperedge creator for the FORCE and sliding window variable ordering algorithms, and the legacy hyperedge creator otherwise.
All hyperedge creators take into account variables that occur indirectly via algebraic variables.
More detailed information about the various representations of variable relations may be obtained during synthesis by enabling debug output.
For advanced configuration, see the separate section on advanced variable ordering configuration.
Variable orderers
The following variable ordering algorithms, or variable orderers, are available:

DCSH
The DSMbased CuthillMcKeeSloan variable ordering Heuristic, or DCSH algorithm, of [Lousberg et al. (2020)] aims to find good global variable orders.
DCSH applies two algorithms, the Weighted CuthillMcKee bandwidthreducing algorithm and the Sloan profile/wavefrontreducing algorithm. It then chooses the best order out of the orders produced by these two algorithms as well as their reverse orders, based on the Weighted Event Span (WES) metric.
The DCSH algorithm is enabled by default. For basic configuration, it can be disabled using the BDD DCSH variable ordering algorithm option (see the options section).

FORCE
The FORCE algorithm of [Aloul et al. (2003)] aims to optimize an existing variable order, but may get stuck in a local optimum.
FORCE iteratively computes new variable orders by considering relations between the variables. Conceptually, highly related variables 'pull' each other closer with more force than less related variables do. Each new order is promoted as the new best order, if it is better than the current best order, based on the total span metric. The iterative algorithm stops once a fixed point has been reached, or after at most 10 * ceil(log_{e}(n)) iterations of the algorithm have been performed, with
n
the number of synthesis variables.The FORCE algorithm is enabled by default. For basic configuration, it can be disabled using the BDD FORCE variable ordering algorithm option (see the options section).

Sliding window
The sliding window algorithm aims to locally optimize an existing variable order for each window.
The sliding window algorithm 'slides' over the variable order, from left to right, one variable at a time, using a fixedlength window. A window is a part of the entire order. For instance, for a variable order
a;b;c;d;e
and windows length 3, the window at index 0 would bea;b;c
, at index 1 it would beb;c;d
, and at index 2 it would bec;d;e
. For each window, it computes all possible variable permutations, and selects the best one based on the total span metric. It then replaces the window by the best permutation of that window, before moving on to the next window.The sliding window algorithm is enabled by default. For basic configuration, it can be disabled using the BDD sliding window variable ordering algorithm option (see the options section).
The default maximum length of the window that is used is 4. The actual window may be smaller, if less than 4 variables and/or location pointers are present in the model. For basic configuration, the maximum length of the window can be configured using the BDD sliding window size option (see the options section). The option to set the maximum length only has effect if the sliding window variable ordering algorithm is enabled. The size must be an integer number in the range [1 .. 12].
If enabled using basic configuration, the algorithms are applied in the order they are listed above. For advanced configuration, see the separate section on advanced variable ordering configuration.