A method for verification of a system design represented by a model that
includes a plurality of variables. The method includes arranging the
variables in an Ordered Binary Decision Diagram (OBDD) according to an
initial order of the variables, the OBDD including a number of nodes
arranged in rows corresponding respectively to the plurality of the
variables. Each processor, among a group of two or more computer
processors, is assigned a respective variable among the plurality of the
variables. Using each processor, the rows of the OBDD are reordered by
varying a position in the OBDD of the row corresponding to the respective
variable that is assigned to the processor until at least one of the
processors identifies a new order for the OBDD. The new order of the OBDD
may be used to verify a characteristic of the model against a
specification.