Evaluation of static variable ordering heuristics for MDD construction [multi-valued decision diagrams]

After designing a multi-valued logic network (MVLN), the resulting circuit has to be verified to guarantee its functional correctness. The most promising technique to cope with increasing device size is formal methods. Ordered multi-valued decision diagrams (OMDDs) have been proposed for formal verification of MVLNs. But OMDDs are very sensitive to the chosen variable ordering, and several ordering heuristics have been proposed in the past. The most promising of these with respect to OMDD size are dynamic variable ordering techniques, but these algorithms often cannot be applied in formal verification approaches due to their long run-times. Alternatively, static variable ordering heuristics have been developed that determine an ordering from the circuit topology, but these heuristics often cannot guarantee good quality. In this paper, an evaluation technique is proposed that uses a pool of static variable ordering heuristics. Each heuristic is applied and the OMDD construction is started until a node or time limit is reached. Then the heuristic performed best so far is selected for the complete construction. The choice of the node and tine limit allows one to smoothly trade off run-time vs. quality. Experimental results are given to demonstrate the efficiency of the approach. The technique allows one to save time and memory, since only promising orders are considered