A method of designing an electronic circuit implemented by one or more computing devices, comprising the steps of: accessing a binary decision diagram which is data embodied by a computer-readable non-transitory storage medium, the BDD representing a function implemented by the design of the electronic circuit or defining a property to be satisfied by the electronic circuit, the function 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 and alternating reordering k consecutive layers, where 1< k ≤ n, wherein each first-level iteration comprises: selecting k consecutive layers from the n layers, wherein the k consecutive layers selected during a current first-level iteration differ from the k consecutive layers selected during a previous first-level iteration immediately preceding the current first-level iteration; determining a locally optimum variable order of the k consecutive layers, comprising iteratively and alternatingly swapping one or more first disjoint pairs of consecutive layers of the k consecutive layers during each odd second-level iteration and one or more second disjoint pairs of consecutive layers of the k consecutive layers during each even second-level iteration, until the locally optimum variable order of the k consecutive layers is determined; and reordering the k consecutive layers according to the locally optimum variable order of the k consecutive layers, the reordering the n variables of the BDD transforming data of the BDD as embodied by the computer-readable non-transitory storage medium 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 which is data embodied by a computer-readable non-transitory storage medium, the BDD representing a function implemented by the design of the electronic circuit or defining a property to be satisfied by the electronic circuit, the function 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 and alternating reordering k consecutive layers, where 1< k ≤ n, wherein each first-level iteration comprises: selecting k consecutive layers from the n layers, wherein the k consecutive layers selected during a current first-level iteration differ from the k consecutive layers selected during a previous first-level iteration immediately preceding the current first-level iteration; determining a locally optimum variable order of the k consecutive layers, comprising iteratively and alternatingly swapping one or more first disjoint pairs of consecutive layers of the k consecutive layers during each odd second-level iteration and one or more second disjoint pairs of consecutive layers of the k consecutive layers during each even second-level iteration, until the locally optimum variable order of the k consecutive layers is determined; and reordering the k consecutive layers according to the locally optimum variable order of the k consecutive layers, selecting k consecutive layers from the n layers, wherein the k consecutive layers selected during a current first-level iteration differ from the k consecutive layers selected during a previous first-level iteration immediately preceding the current first-level iteration; determining a locally optimum variable order of the k consecutive layers, comprising iteratively and alternatingly swapping one or more first disjoint pairs of consecutive layers of the k consecutive layers during each odd second-level iteration and one or more second disjoint pairs of consecutive layers of the k consecutive layers during each even second-level iteration, until the locally optimum variable order of the k consecutive layers is determined; and reordering the k consecutive layers according to the locally optimum variable order of the k consecutive layers, the reordering the n variables of the BDD transforming data of the BDD as embodied by the computer-readable non-transitory storage medium 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.