Modern architecture designs are becoming more heterogeneous. In addition to general purpose processors, accelerators are widely used in System-on-Chips (SoCs). These computation units take advantage of the specialty of the computation to achieve higher performance and better energy efficiency.
The accelerator-rich architecture brings new challenges to verification. As more critical functions are moved to accelerators, our focus of verification needs to be extended from processor to accelerators and their interaction.
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.
We showed the utility of ILA-based equivalence checking via several examples, including both accelerators and processors. Our experiments discovered the MRET/SRET bug in the RISC-V Rocket core implementation.
The next step is to consider the equivalence checking on a system of ILAs, in which case, consistency and coherence behaviors on the shared states need to be addressed.