I am currently working on applying the instruction-level abstraction (ILA) methodology to solve the software/hardware co-verification problem in systems-on-chip (SoC). ILA is a formal model that abstracts hardware modules at the architecture level and describes hardware functionalities as a set of instructions, as in processors. This universal formalism provides a nice interface between the firmware and the accelerators while abstracting out irrelevant implementation-dependent details. We are exploiting the benefits of this formalism in verifying firmware in the SoC, by using symbolic execution, bounded model checking, and also Horn clause based model checking, etc.