This work has developed new approaches for using symbolic simulation in formal hardware verification. These approaches enlarge the reach and improve the accessibility of formal verification in contemporary design practices. We have verified important aspects of major circuits from Intel microprocessor designs with BDD-based symbolic simulation. The results of Parts I and II significantly increase the effectiveness of BDD-based symbolic simulation for contemporary design practices. The techniques presented in Part III require a more abstract design representation.