1. A method for satisfiability (SAT)-based bounded model checking (BMC), the method comprising: independent of an SAT solver, accessing a logic-level description of a circuit generated from a register transfer (RT)-level description of the circuit; and independent of the SAT solver, applying logic optimization to the logic-level description to simplify the logic-level description for SAT-based BMC of the circuit using the logic-level description.