Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders