HVC2010 - When things go right
Sixth annual Haifa Verification Conference gathers verification experts from diverse countries and domains of expertise.
Verification, or the process of making sure things work as intended, is vital to any system. Methods for eliminating the bugs in hardware and software are very different, yet experts in Haifa have realized that sharing challenges and ideas has incredible potential for advancing the field as a whole.
As always, this year's international Haifa Verification Conference (HVC) provided a forum for academia, industry, and the research and development community to share their work, exchange ideas, and discuss the challenges and future directions of verification for hardware, software, and hybrid systems.
A special conference session on debugging was an ideal opportunity for hardware and software verification experts to learn from each other. The session took examples from hardware simulation, static analysis, software, pre-silicon, and post silicon debugging—sparking intense dialogs between the different groups. It's no coincidence that IBM Research - Haifa Israel has verification experts in all these areas. After seeing how beneficial collaboration and joint brainstorming has been within the lab, researchers are anxious to get these same conversations going outside in the industry and academia. Other popular program items included a tutorial on transaction memory and a session from Intel on firmware verification.
"Within each paradigm, different algorithms and techniques are used for hardware and software systems," explained Sharon Barner, research staff member in Haifa and general chair of this year's conference. "Yet, at their core, all of these techniques aim to achieve the same goal of ensuring the correct functionality of a complicated system. HVC is the only conference that brings together researchers from all fields of verification, thereby encouraging the migration of methods and ideas between domains."
Pioneers, old and new
Another highlight of the conference was the HVC award, honoring the work of professors from different organizations who established a new field for the study of Satisfiability Modulo Theory (SMT). This flourishing area is further testament to the importance of dialog and collaboration between different teams.
This year, numerous individuals from outside IBM contributed to the success of the conference, including program co-chairs Daniel Kroenig from Oxford and Ian Harris from the University of California - Irvine and the HVC award committee. Experts from Intel were especially active this year, and many participants expressed a desire to help with next year's conference.
This year's invited talks demonstrated the value of combining different verification domains. For example, Professor Valeria Bertacco combined dynamic hardware verification with formal methods in her talk "Verification Failures: What to Do When Things Go Wrong". Professor Helmut Veith presented "Did You Specify Your Test Suite," which combined formal methods with software testing.
Another one of the seminar highlights was a special session in memory of Amir Pnueli, a pioneer in the specification and verification of computer systems. Pnueli received the 1996 ACM Turing Award, the highest distinction that can be given to a computer scientist, for his seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification. Not only was Pnueli a great scientist, he was a special person who was admired by all and had many followers. David Harel, who was awarded the Israeli Prize, delivered personal remarks and gave a presentation. The session included three additional tutorial-style overviews in areas where Pnueli was influential.
What's new in the field of verification?
"The amount of time people spend today on debugging is huge," explained Barner. "Even though it sounds simple, it's anything but that." Information on what went wrong is available, but experts then need to analyze the information to see where the problem occurred and what exactly caused it. New algorithms are being developed all the time to help locate problems and innovative productivity tools are being introduced to graphically present the bugs so people can find solutions faster.
The relatively new area of post-silicon verification is also gaining momentum and has a lot of room for research. Pre-silicon verification includes the testing done before the actual prototype is created in the fab. Once the prototype is built, different processes of verification and debugging are needed to identify problems that come up in the silicon, where it becomes more difficult to pinpoint various glitches. In fact, the HVC Best Paper award was given for work in this area to Reaching Coverage Closure in Post-silicon Validation. The conference committee expects this paper will be quoted for years to come as one of the first major research contributions in this area.
Participants from all over Israel and abroad gave very positive feedback on both the content and organization of HVC 2010. Barner herself especially enjoyed the teamwork of the people who joined forces to give the conference the content and special flavor that makes it unique. With an overflow crowd of over 200 people filling the Haifa auditorium, this was no easy task.
"HVC 2010 was a tremendous vote of confidence for the Research Lab in Haifa as one of the leaders of the Israeli verification arena, one of the strongest spaces in the world verification domain," she continued. "Too bad we couldn't test the bus that broke down in the middle of our trip up north to Zippori National Park," she joked. Perhaps in time for HVC 2011.