Well, there are a lot of ways how to check the equivalence of formulas, and each one of them can be used here, once you read the Boolean functions from the two BDDs. An alternative would be to apply the swap operation to swap variables x1 and x2 in the ordering that must convert one BDD into the other one.

However, the simplest way would be to compare the high- and low-subtrees of the root node. As high-subtrees, you find x2&!x1 | !x2 and !x1 | x1&!x2 which are same which you can see by a Shannon decomposition of both:

- x2&!x1 | !x2 = (x1 => !x2 | 1)
- !x1 | x1&!x2 = (x1 => !x2 | 1)

Same way, the low-trees are x2&x1 in both cases, and therefore trivially the same.