Equivalence checking can be used to ensure the correctness of hardware by comparing one implementation with another correct implementation or specification. This equivalence is not necessarily a cycle-to-cycle matching. Our methodology adopts the Instruction-level Abstraction (ILA) to model accelerators from the perspective of their interactions at the interface. In the abstraction, implementation specific details are abstracted away by explicitly separating the architectural state from the implementation. Verification is done in a per-instruction manner to break the big problem into smaller ones. And it checks on the lowest specification level. This allows us to compare designs with diverse microarchitectural implementation.