Modern computing platforms are becoming more and more heterogeneous. In addition to the general-purpose processors, domain-specific accelerators are now widely used in System-on-Chips (SoCs) to achieve higher performance and better energy efficiency. As more hardware functionalities are moving to the accelerators, we need to extend our focus of verification from processors to accelerators and their interactions. One notable verification challenge for accelerator-rich architectures is the lack of a modular specification that enables separation of concerns and allows modular verification for better scalability. This talk will present the instruction-level abstraction model, a uniform instruction-level specification for processors and accelerators. It will also cover the applications of instruction-level abstraction in scalable formal verification.

Speaker Bio:

Prof. Hongce Zhang is currently an assistant professor in the Microelectronics Thrust of the Hong Kong University of Science and Technology (Guangzhou). He received his PhD from the Electrical and Computer Engineering Department of Princeton University in 2021. His research is mainly around hardware formal verification. He has been working on the Pono model checker and the instruction-level abstraction (ILA) project. Both have been used in industrial applications.