A team of researchers spearheaded by graduate student Bo-Yuan Huang developed the first step in a model of uniform verification for next-generation hardware accelerators, bringing mathematical rigor to a rapidly evolving field. The work earned them an ACM Best Paper Award at the 2020 Design Automation Conference. Photo by Adi Goldstein.
Princeton researchers have received a 2020 Best Paper Award from the Association of Computing Machinery (ACM), recognizing their work in design verification. The paper proposed a formal model that provides a uniform way to analyze hardware designs in modern computing systems.
For computers to perform well, hardware engineers must be able to verify that their designs work exactly as intended at the software interface. While conventional processors benefit from well-studied formal verification methodologies — essentially a kind of mathematical proof — cutting edge chips don't yet have such a standard, according to electrical engineering graduate student Bo-Yuan Huang. Huang and fellow Ph.D. student Hongce Zhang are the lead authors on the paper. These chips contain highly specialized hardware accelerators that power our emerging computing systems – these are more complex and their designs more varied than conventional processors, creating challenging problems for engineers to solve.
"We're trying to extend what people did in the past for processors and try to generalize it for the new coming accelerators," Huang said.
Inspired by the specification of general-purpose processors, the researchers proposed modeling only the externally visible behavior of each command of the specialized accelerators. The model, called Instruction-Level Abstraction (ILA), works something like the blueprint for a house, giving both contractors and regulators a common set of specifications without overwhelming them with internal details. The ILA formal model provides a clean separation between software and hardware development and verification.
The paper, published in ACM Transactions on Design Automation of Electronic Systems, lays the foundation for a formal model that works across a wide range of hardware, including conventional general-purpose processors and more specialized accelerators.
In addition to describing the new model in formal detail, the researchers showcased its use in applications of machine learning, image processing and cryptography.
Huang first became interested in the topic as an undergraduate at National Taiwan University in Taipei. He came to Princeton in 2015 to work directly with Sharad Malik, the George Van Ness Lothrop Professor in Engineering, a leading authority on formal verification and the paper's senior author.
The paper is part of a broader set of projects led by Malik, who is also the chair of electrical engineering, aimed at developing a universal model for end-to-end verification. One of the paper's authors, Pramod Subramanyan, previously won an ACM SIGDA outstanding dissertation award for related work.
The authors also include Yakir Vizel, who worked on this project as part of his post-doctoral studies at Princeton, now a faculty member at the Technion in Israel; and Aarti Gupta, professor of computer science.
The research was supported by Applications Driving Architectures (ADA) Research Center, a Joint University Microelectronics Program co-sponsored by the Semiconductor Research Corporation and the Defense Advanced Research Projects Agency.
