7/9/2014 Katie Carr, CSL
Written by Katie Carr, CSL
Smartphones, tablets, laptops, and wearable technology today all have one motto – faster, cheaper, slicker, smaller. But what else do the ultra sophisticated Samsung Galaxy, iPhone 5, Fitbit Flex, and MacBook Air all have in common?
A system-on-a-chip (SoC) with a CPU, graphics IP cores, memory, high speed I/O, and the fact that they are extremely hard to verify.
Even when there were several hundred thousand transistors per computer chip, the number of design points that required verification was more than the number of protons in the universe. Now, with billions of transistors in computer chips being integrated into SoCs in handheld and mobile devices, the complexity of designing computer systems is among the most daunting engineering tasks known to man.
"Even though there is a paucity of computing capacity and resources to ensure correctness of design, the gap between design and verification continues to widen. We build systems that we do not know how to verify. Verification has been identified as one of the grand challenges of computing for this reason."
Vasudevan, along with her students, Viraj Athavale, Sai Ma, and Samuel Hertz, recently received the Best Paper Award at the 2014 Design Automation Conference (DAC), for their research in code coverage of assertions using register transfer level (RTL) source code analysis, which will help with accuracy and speed during the verification process.
Vasudevan also won the Best Paper Award at the International Conference on VLSI Design earlier this year.
DAC, which was held in San Francisco on June 7 – 11, is the premier conference for design and automation of electronic systems and is attended by several thousand researchers, academics, engineers, and designers each year. This year, there were 760 papers submitted, 144 accepted, 12 nominated for best paper awards, and two papers eventually received this highly coveted award. The award was presented at the keynote address with several thousand people attending the function.
“To be recognized at DAC, with its wide-angle research scope and diverse audience, is a great honor,” Vasudevan said. “I am humbled to join the lineup of prominent researchers in design automation who have won this award before me.”
Writing good properties or assertions that describe specification intent is the cornerstone of verification. Determining the value of properties is a classical problem in verification, but in the recent past, the growing popularity of assertion based verification has led to many non-experts writing assertions. Automatic assertion generation tools, like Vasudevan's pioneering GoldMine and several others in this space, have also given rise to a need for assessing the value of the generated assertions.
In this research, Vasudevan and her students provide an automatic method to evaluate how good a design property or assertion is. This is in terms of statements of the RTL source code, or code coverage. RTL is the abstraction layer used for designing these systems. Their method defines and computes code coverage of an assertion. Code coverage, which is an important parameter in determining the quality of verification results, measures the fraction of elements of source code executed while simulating the test suite. Scale is the single largest challenge verification researchers face. Vasudevan’s method's most attractive feature is its ability to scale, due to its hybridization of statistical analysis and formal analysis.
"RTL debugging can take six to eight months for a 20 person expert team, according to our industry collaborators," Vasudevan said.
Vasudevan began this research in 2011 with Viraj, one of her master’s students. At the time, they were trying multiple solutions, one of which was eventually implemented inside GoldMine by Hertz. Ma rejuvenated the research over a year ago, as her first project she undertook as a graduate student.
"As a second year master's student, I learned a lot from my advisor and the team about developing great research, thanks to their guidance and help throughout the process," said Ma (BSEE '12). "Hopefully my experience will motivate other students to continue graduate education with our world class faculty."
"Sai has demonstrated persistence and zeal in her desire to conduct path-breaking research," Vasudevan said. "I hope she serves as an example to other bright female undergraduates in ECE to realize their potential in academic research and not be discouraged by their numbers. It was a proud moment for me to receive this award on stage with my first female graduate student."
Vasudevan, Ma, and their team are looking forward to electronic design automation (EDA) tool companies, such as Cadence or Synopsys, incorporating their ideas in their tool suite, to expedite and improve the confidence in verification.
Vasudevan added that their algorithms comprise “critical back-end technology that affects the process of designing modern systems.” If verification researchers are able to ascribe a figure of merit to a property, “we can enhance the productivity of the whole industry,” she said.
Vasudevan plans to continue working in this area of coverage analysis and debugging of RTL designs. She has an ongoing collaboration with AMD Inc. to devise new algorithms in this area for their next generation chip designs.
“Our method for identifying code coverage can be applied to debugging, but is not the complete solution,” Vasudevan said. “Ideally, we should be able to relate a failing/passing property to the design source code, as well as to the design state and the original intent of the designer. This was an important first step, but there are many miles to go.”