A method of designing an electronic circuit executed by one or more computing devices, comprising: accessing a binary decision diagram stored in a storage device, the BDD representing a function implemented by the electronic circuit or a property to be satisfied by the electronic circuit, the BDD having n variables, where n ≥2, wherein the BDD comprises n layers corresponding to the n variables, respectively; characterised by reordering the n variables of the BDD by iteratively moving k variables of the n variables to their locally optimum layers, wherein each iteration comprises: selecting from the n layers k layers that currently have the k largest sizes among the n layers, wherein the k variables are currently positioned at the k layers; iteratively and concurrently moving the k variables to different layers of the BDD until each of the k variables has been at all the n layers to determine a locally optimum layer for each of the k variables, wherein the locally optimum layer of a variable during each iteration is one of the n layers that currently yields a smallest size among the n layers with the variable at each of the n layers; and concurrently moving the k variables to their respective locally optimum layers; wherein the reordering is repeated until a size of the BDD has reached a desired threshold; and by using the transformed BDD to generate an electronic circuit or to formally verify the circuit design. accessing a binary decision diagram stored in a storage device, the BDD representing a function implemented by the electronic circuit or a property to be satisfied by the electronic circuit, the BDD having n variables, where n ≥2, wherein the BDD comprises n layers corresponding to the n variables, respectively; characterised by reordering the n variables of the BDD by iteratively moving k variables of the n variables to their locally optimum layers, wherein each iteration comprises: selecting from the n layers k layers that currently have the k largest sizes among the n layers, wherein the k variables are currently positioned at the k layers; iteratively and concurrently moving the k variables to different layers of the BDD until each of the k variables has been at all the n layers to determine a locally optimum layer for each of the k variables, wherein the locally optimum layer of a variable during each iteration is one of the n layers that currently yields a smallest size among the n layers with the variable at each of the n layers; and concurrently moving the k variables to their respective locally optimum layers; wherein the reordering is repeated until a size of the BDD has reached a desired threshold; and by selecting from the n layers k layers that currently have the k largest sizes among the n layers, wherein the k variables are currently positioned at the k layers; iteratively and concurrently moving the k variables to different layers of the BDD until each of the k variables has been at all the n layers to determine a locally optimum layer for each of the k variables, wherein the locally optimum layer of a variable during each iteration is one of the n layers that currently yields a smallest size among the n layers with the variable at each of the n layers; and concurrently moving the k variables to their respective locally optimum layers; wherein the reordering is repeated until a size of the BDD has reached a desired threshold; and by using the transformed BDD to generate an electronic circuit or to formally verify the circuit design.