Computer chips are so complicated these days that more than half the time it takes to design them is devoted to checking for errors, and even then designers can't be sure they've caught all the flaws. Entire businesses are built around developing mathematical and computing tools to verify that chips will perform as expected.

So it was a surprise to Professor of Electrical Engineering Sharad Malik when two undergraduate students participating in his research team developed chip checking software that is 10 to 100 times faster than any other tool in existence.

Their software, already being adopted by academic and commercial researchers, has the potential to increase significantly the reliability of new chips and may shorten the design cycle for some products.

Excellent research

"It is an excellent piece of research," Professor Malik said. "I am amazed that they did this when so many people had been looking at this problem for so long."

Matthew Moskewicz and Conor Madigan, both class of 2000, worked on the problem for their senior independent work projects and during the following summer. They addressed a common logical puzzle known as a Boolean satisfiability problem.

An example is the kind of conundrum that sometimes appears on standardized college admission tests: If 10 people are coming to dinner and guest A wants to sit with guest B or C, but B is friends with D, who does not like CS. When the number of variables is large, finding a solution that satisfies all the conditions can be very difficult.

SAT problems

Such puzzles, known to computer scientists as SAT problems, play a role in many businesses, from scheduling the season for a sports league to arranging the logistics of an assembly line. With a computer chip, the question of how it will perform in any of billions of situations can be stated as a small number of hugely complex SAT problems.

In recent years, computer programs known as SAT solvers have become important tools in the chip industry. As chips become more complicated, however, it is not uncommon for SAT solvers to require many days to churn through a problem.

The program Matthew and Conor wrote, which they named Chaff, can reduce days of calculations to minutes, and, more importantly, succeed in cases where other techniques are too time-consuming to be used at all.

"I think it's a real breakthrough," said Randal Bryant, chair of the computer science department at Carnegie Mellon University and an authority on chip verification and satisfiability. Professor Bryant said one of his graduate students tested Chaff against every other SAT solver he could find.

"It was really amazing how consistent it was," he said. "Usually it's more of a horse race. In this case it was just hands down the winner."

Professor Bryant said tools such as Chaff are important because chip makers are eager to avoid debacles such as the one that plagued Intel Corp. when it had to conduct a $475 million recall of a Pentium chip that made math mistakes in some circumstances.

"That was a real wake-up call for the whole industry," Professor Bryant said. "They've invested a lot of money in verification. Boolean satisfiability is really at the heart of that whole process."

Matthew and Conor were not expecting to develop a new industry standard when they began their senior independent research projects. They were working with Professor Malik, his graduate student Ying Zhao, and associate professor, Margaret Martonosi, on ideas for speeding up the chip verification process. Professor Malik saw that conventional computers do not have the optimum design for handling SAT problems, and set out to invent a computer specifically engineered for the task.

Flawed standards

In researching programming methods, or algorithms, on which to base this machine, the students became convinced that all the existing ideas were flawed.

"It occurred to us that if we had a lousy algorithm and spent all this time implementing it in hardware, then someone could come out with better software and blow our machine away," Conor said.

So they urged Professor Malik to let them write their own software, and he agreed. They set to work with what they now see was a large degree of naïveté about the difficulty of the problem.

"It took a really long time just to understand enough about how these solvers work," said Matthew, who is pursuing a Ph.D. in computer science at the University of California at Berkeley.

"We had many, many conversations late at night," said Conor, now a graduate student at the Massachusetts Institute of Technology. "If you live with something long enough, it starts to become clear." Although Matthew was working directly with Professor Malik as his adviser, Conor was officially working on a different project and was just squeezing in the time to work on Chaff.

Professor Malik said that by the end of the semester, "it became clear that the ideas they had were pretty interesting and could really pay off."

He hired Matthew to work for him over the summer. Conor stayed to work on a different project, but continued the collaboration. Throughout the summer, their program progressed from being much slower than the others to being much faster.

They named the software Chaff to evoke the image of sorting wheat from chaff. "I've got sort of a grain motif going on," Matthew said. "All the official release versions are named after types of grain: corn, rice, barley, wheat, and, most recently, spelt."

Creating a buzz

They will present their findings at a major conference in June, but news of their work already has created a buzz throughout the industry. Professor Malik has been receiving a steady stream of e-mails from researchers who want to try Chaff. He is making it available to academic researchers and, on a trial basis, to commercial developers while working with the University's Office of Technology Licensing to patent it.

"Absolutely, it will have an immediate impact," said James Kukula, a senior researcher at Synopsys Inc., one of the leading makers of automated chip design software. "We definitely have products in development or being sold where the SAT problem is very important."

Nonetheless, Mr. Kukula said Chaff alone will not revolutionize the industry. It is one more tool in a broad arsenal of approaches to chip verification, he said.

Professor Malik is continuing to work on hardware solutions with Ying and on software solutions with graduate student Lintao Zhang.

"There is significant untapped potential on both sides," he said, adding that Matthew's and Conor's success is not the result of a single breakthrough; rather "it was really just excellent engineering throughout."

"Their ideas were simple but quite clever," Professor Bryant said. "There's nothing wrong with simple ideas."

Professor Malik said he hopes the success sends undergraduates a clear message that their scientific research can make a difference.

"This is world-class, high-impact research," Professor Malik said. "I am so excited that this is the result of the senior independent work component of our program. It highlights the quality of our students, our program, and especially the opportunities available to them to make an impact."

"Their ideas were simple but quite clever," said Randal Bryant, chair of the computer science department at Carnegie Mellon University and an authority on chip verification and satisfiability.

Sharad Malik

Conor Madigan '00

Matthew Moskewicz '00

This story first appeared in the March 5, 2001, issue of the Princeton Weekly Bulletin and is reprinted here with permission.