A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures