BDD variable order

Internally, data-based synthesis represents predicates using Binary Decision Diagrams (BDDs). CIF variables and automata are represented using one or more boolean variables (also called BDD variables or bits). For instance, a boolean CIF variable is represented using a single boolean/BDD variable, and a CIF variable of type int[0..8] is represented using four boolean/BDD variables (9 possible values, log2(9) ≈ 3.17). For each automaton with two or more locations, a location pointer variable is created, that represents the current or active location of that automaton. For instance, an automaton with three locations is represented using two boolean/BDD variables. Two boolean/BDD variables can represent 22 = 4 values, so one value is not used.

The CIF variables and location pointer variables for the automata (together called synthesis variables) can be ordered. This ordering can significantly influence the performance of synthesis. Synthesis variables that have a higher influence on the result of predicates (simply put, occur more frequently in predicates) should generally be put earlier in the ordering. Furthermore, in general, strongly related synthesis variables (e.g. by comparison, integer computation, or assignment) should be kept closely together in the order. For two synthesis variables x and y, examples of predicates that introduce relations are x = y (by comparison) and 5 < x + y (by integer computation), and examples of assignments that introduce relations are x := y and x := y + 1 (both by assignment).

For the initial variable ordering, it is possible to order the BDD variables per synthesis variable, or to interleave the BDD/boolean variables of some synthesis variables. This can significantly influences the performance of synthesis. Generally, strongly related synthesis variables should be interleaved.

For more information on ordering and its influence on performance, see Chapter 3 of [Minato (1996)].

For each CIF variable and location pointer, two synthesis variables are created, one storing the old/current value (before a transition), and one storing the new value (after a transition). For a single CIF variable or location pointer, the old and new synthesis variables are always kept together, and interleaved. The old synthesis variable is also always before the new synthesis variable.

The initial order of the boolean/BDD variables is determined by the BDD variable order option (see the options section). Several predefined orders exist, and it is also possible to define a custom order. By default, the sorted order is used. The following predefined orders exist:

Furthermore, a custom initial order can be defined. Custom orders consist of absolute names of variables and automata. That is, for an automaton a, with a discrete variable x, the absolute name of the variable is a.x. The * character can be used as wildcard in those names, and indicates zero or more characters. In case of multiple matches, the matches are sorted increasingly on their absolute names, and interleaved.

Multiple names can be separated with ; characters. The synthesis variables matching the name pattern before the ; are ordered before the synthesis variables matching the name pattern after the ;. The ; separator does not introduce interleaving. The , separator can be used instead of the ; separator to introduce order but also introduce interleaving.

Each name pattern in the order must match at least one variable or automaton. A variable or automaton may not be included more than once in the order. Every variable and automaton (with two or more locations) needs to be included in the order. It is not possible to specify new variables, as they are always directly after their corresponding old variables, and they are always interleaved.

For instance, consider two automata: a and b, each with three variables of type int[0..3]: x1, x2, and x3. The automata have three locations each, so location pointers are created for them. We thus have six discrete variables: a.x1, a.x2, a.x3, b.x1, b.x2, and b.x3, and two location pointer variables: a and b. Consider the following custom order: b*;a.x3,a.x1;a.x2,a. Pattern b* matches location pointer variable b as well as the three discrete variables of automaton b (b.x1, b.x2, and b.x3). They are ordered in increasing alphabetic order, and are interleaved. Variables a.x3 and a.x1 are also interleaved, with a.x3 before a.x1. Finally, variable a.x2 is ordered before the location pointer for automaton a, and they are interleaved as well. This results in the following initial boolean/BDD variable ordering, with bits whose name ends with + representing bits of new variables rather than current/old variables, and x#0 representing bit zero of variable x:

b#0
b+#0
b.x1#0
b.x1+#0
b.x2#0
b.x2+#0
b.x3#0
b.x3+#0
b#1
b+#1
b.x1#1
b.x1+#1
b.x2#1
b.x2+#1
b.x3#1
b.x3+#1

a.x3#0
a.x3+#0
a.x1#0
a.x1+#0
a.x3#1
a.x3+#1
a.x1#1
a.x1+#1

a.x2#0
a.x2+#0
a#0
a+#0
a.x2#1
a.x2+#1
a#1
a+#1

The default 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 initial variable ordering, and try to improve it using a fast heuristic. Some algorithms search for a local optimum. A better initial variable ordering may then result in a better final variable ordering (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, they typically do 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.

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. 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):

All hyper-edge creators take variables that occur indirectly via algebraic variables into account.

More detailed information about the various representations of variable relations may be obtained during synthesis by enabling debug output.

The following variable ordering algorithms are available:

If enabled, the algorithms are applied in the order they are listed above.