Work by Karem Sakallah, professor of computer science and engineering, and PhD student Aman Goel took first place at the 11th edition of the Hardware Model Checking Competition, an event hosted by the Conference on Formal Methods in Computer-Aided Design to determine the best current method for formally verifying a hardware system. The event featured nine categories composed of a total of 639 benchmarks; the pair earned gold medals in 7 categories and a silver and bronze in the remaining two, solving the most number of benchmarks including 23 of which were not solved by any other verifier.
Hardware design specifications like those tested at HWMCC are the logical descriptions of a proposed processor, including how the logical components are arrayed on the chip and how data “moves” between them. Researchers like Sakallah, Goel, and other competitors aim to prove that these designs are free of bugs and security flaws by reasoning about them as mathematical formulas. This line of work is called formal verification, and can be used to safeguard against bugs in both hardware and software.
