A Princeton research team has won a Best Paper Award from the 2021 Design, Automation and Test in Europe Conference (DATE), held in February. The paper laid out a generalized solution to a key problem in computer design verification.
For computers to perform well, hardware engineers must be able to verify that their designs work as intended at the software interface. While established verification methodologies — essentially a kind of mathematical proof — work for conventional processors, cutting edge chips don't yet have such an established standard.
Yue Xing, a graduate student in electrical and computer engineering and the paper's first author, said that many highly specialized, next-generation devices handle multiple software interfaces at once. Older models treat processors as monolithic designs and can't account for the complexity of nested modules in advanced systems.
Xing's work, advised by Sharad Malik, the George Van Ness Lothrop Professor in Engineering and ECE department chair, breaks the problem into its constituent parts.
"We needed an instruction-level model for each module," Xing said. "So we separated the monolithic reasoning and shifted to a hierarchical reasoning."
The result is a generalized extension of a model known as Instruction-Level Abstraction (ILA), previously developed by researchers in Malik's lab. 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.
Another recent paper from Malik's group, which extended ILA to hardware accelerators and helped pave the way for Xing's paper, won a 2020 Best Paper Award from the Association of Computing Machinery.
In addition to Xing and Malik, this paper's authors also include Huaxi Lu, an ECE graduate student, and Aarti Gupta, professor of computer science.