A method of designing an electronic circuit comprising: by one or more computing devices, 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 an electronic circuit or defining a property that the electronic circuit should satisfy, the function having n variables, where n ≥ 2, wherein the BDD comprises n layers corresponding to the n variables, respectively; characterized in that the method comprises the steps of: separating the n variables into n ! 2 ⌊ n / 2 ⌋ groups, wherein each group comprises ⌈ n 2 ⌉ ordered sets, wherein: when n is even, each of the ⌈ n 2 ⌉ ordered sets in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables; and when n is odd, each of the ⌈ n 2 ⌉ ordered sets, except a first set, in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables, and the first set in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 1 of the n variables and has a same position order among the ⌈ n 2 ⌉ ordered sets in that group among the n ! 2 ⌊ n / 2 ⌋ groups; for each of the n ! 2 ⌊ n / 2 ⌋ groups, determining a locally optimum variable order that yields a smallest size among 2 └ n /2┘ different variable orders of the BDD obtained within the group; selecting from n ! 2 ⌊ n / 2 ⌋ locally optimum variable orders corresponding to the n ! 2 ⌊ n / 2 ⌋ groups an optimum variable order of the BDD that yields a smallest size among the n ! 2 ⌊ n / 2 ⌋ locally optimum variable orders; and reordering the n variables of the BDD according to the optimum variable order of the BDD to transform one or more data of the BDD as embodied by the computer-readable non-transitory storage medium; and using the transformed BDD to generate an integrated circuit of to formally verify the circuit design. separating the n variables into n ! 2 ⌊ n / 2 ⌋ groups, wherein each group comprises ⌈ n 2 ⌉ ordered sets, wherein: when n is even, each of the ⌈ n 2 ⌉ ordered sets in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables; and when n is odd, each of the ⌈ n 2 ⌉ ordered sets, except a first set, in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables, and the first set in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 1 of the n variables and has a same position order among the ⌈ n 2 ⌉ ordered sets in that group among the n ! 2 ⌊ n / 2 ⌋ groups; when n is even, each of the ⌈ n 2 ⌉ ordered sets in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables; and when n is odd, each of the ⌈ n 2 ⌉ ordered sets, except a first set, in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 2 of the n variables, and the first set in each of the n ! 2 ⌊ n / 2 ⌋ groups comprises 1 of the n variables and has a same position order among the ⌈ n 2 ⌉ ordered sets in that group among the n ! 2 ⌊ n / 2 ⌋ groups; for each of the n ! 2 ⌊ n / 2 ⌋ groups, determining a locally optimum variable order that yields a smallest size among 2 └ n /2┘ different variable orders of the BDD obtained within the group; selecting from n ! 2 ⌊ n / 2 ⌋ locally optimum variable orders corresponding to the n ! 2 ⌊ n / 2 ⌋ groups an optimum variable order of the BDD that yields a smallest size among the n ! 2 ⌊ n / 2 ⌋ locally optimum variable orders; and reordering the n variables of the BDD according to the optimum variable order of the BDD to transform one or more data of the BDD as embodied by the computer-readable non-transitory storage medium; and using the transformed BDD to generate an integrated circuit of to formally verify the circuit design.