Improving bit-level model checking algorithms for scalability through circuit-based reasoning