Speed separates Chaff from the rest Steven Schultz Princeton, NJ -- 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. "It is an excellent piece of research," said Malik. "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 C.... When the number of variables is large, finding a solution that satisfies all the conditions can be very difficult. 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 an important tool 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 Moskewicz and Madigan 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. 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." 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 wakeup call for the whole industry," said Bryant. "They've invested a lot of money in verification. Boolean satisfiability is really at the heart of that whole process." Moskewicz and Madigan were not expecting to develop a new industry standard when they began their senior independent research projects. They were working with Malik, his graduate student Ying Zhao and another professor, Margaret Martinosi, on ideas for speeding up the chip verification process. 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. 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," said Madigan. So they urged 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 naiveté about the difficulty of the problem. "It took a really long time just to understand enough about how these solvers work," said Moskewicz, who is pursuing a Ph.D. in computer science at the University of California-Berkeley. "We had many, many conversations late at night," said Madigan, now a graduate student at the Massachusetts Institute of Technology. "If you live with something long enough, it starts to become clear." Although Moskewicz was working directly with Malik as his adviser, Madigan was officially working on a different project and was just squeezing in the time to work on Chaff. By the end of the semester, said Malik, "it became clear that the ideas they had were pretty interesting and could really pay off." He hired Moskewicz to work for him over the summer. Madigan 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 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," said Moskewicz. "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. 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, 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. Malik is continuing to work on hardware solutions with Ying and on software solutions with another graduate student, Lintao Zhang. "There is significant untapped potential on both sides," he said. He said that Moskewicz's and Madigan'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," said Bryant. "There's nothing wrong with simple ideas." 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," said Malik. "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." top		[an error occurred while processing this directive]