Automatic variable ordering

The CIF data-based synthesis tool’s predefined initial variable orders are often not optimal performance-wise. 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 hyper-edges, and another is graph edges, which are derived from the hyper-edges.

For basic configuration, the variable relations that are used to construct the hyper-edges can be configured using the BDD hyper-edge creation algorithm option (see the options section). By default, the Default relations are used. The following variable relations can be used:

  • Legacy

    The legacy hyper-edge creator creates the following hyper-edges:

    • Per invariant, a hyper-edge for the variables that occur in the invariant.

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

    • Per assignment, a hyper-edge for the variables that occur in the addressable and value of the assignment.

    • Per event, a hyper-edge for the variables that occur in the guards and updates of all edges for that event in the entire specification.

  • Linearized

    The linearized hyper-edge creator creates the following hyper-edges:

    • Per linearized edge, a hyper-edge 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 hyper-edge creator for the FORCE and sliding window variable ordering algorithms, and the legacy hyper-edge creator otherwise.

All hyper-edge 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 DSM-based Cuthill-McKee-Sloan variable ordering Heuristic, or DCSH algorithm, of [Lousberg et al. (2020)] aims to find good global variable orders.

    DCSH applies two algorithms, the Weighted Cuthill-McKee bandwidth-reducing algorithm and the Sloan profile/wavefront-reducing 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(loge(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 fixed-length 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 be a;b;c, at index 1 it would be b;c;d, and at index 2 it would be c;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.