Reduced Ordered BDDs coincide with the minimal DFAs that accept the language of bit vectors encoding the boolean assignments that satisfy the modeled predicate. That is, this holds if the BDD has not had the "skip test if both outcomes less to the same sub-bdd" optimization applied, which anyway only reduces its size by a constant factor.
