MC Competition Chairs
Paper Submission: March 26
Paper Notification: April 23
Benchmark Submission: May 28
Model Checker Submission: June 4
Competition Results: July 15
Workshop: July 15
Hardware Verification Workshop 2010
First International Workshop
Room 2.11 Thursday July 15th Appleton Tower.
Competition results available.
An interesting related post.
Why Work on Hardware Verification?
In recent years there has been a steady dwindling in the number of publications that specifically target formal verification of hardware. Yet hardware verification is a solved problem in theory only. In this talk I will present a number of real-life verification-related problems that may lend themsevles to a formal solution.
Managing State Explosion through Runtime Verification
The major challenge in hardware verification is managing the state explosion problem in pre-silicon verification. This is reflected in the high cost and low coverage of functional simulation and the capacity limitations of formal verification. Runtime verification offers an attack on this problem through on-the-fly property checking of the current trace and providing a recovery mechanism to deal with failure. There are several interesting examples of runtime verification that have been proposed in recent years in the computer architecture community. These have been largely motivated by the resiliency needs of future technology generations in the face of dynamic errors due to device failures.
I will first highlight the key ideas in hardware runtime verification through specific examples from the uni-processor and multi-processor contexts. Next, I will discuss the challenges in implementing some of these solutions. Finally I will discuss how the strengths of runtime verification and model checking can be used in a complementary fashion.
Remarkably 4 teams participated for the first time with 6 new model checkers respectively variants of model checkers. Among the 21 participating model checkers there were 8 new versions of already existing model checkers. The competition prompted model checking researchers in academia and industry to contribute about 173 new benchmarks in addition to the 645 benchmarks collected for the previous edition.
When model checking was first conceived it was a purely academic notion with no practical use. Through a series of breakthrough developments model checking, and formal verification in general, have become extensively used and relied upon in the semiconductor industry. However, the problem is far from being solved. In fact, the rate at which verification capabilities increase does not match the rate at which design complexity and size grow. This phenomenon is called the "verification gap", and it is one of the biggest concerns of the industry. Recently, however, we see a steady dwindling in the number of publications that specifically target hardware.
The purpose of this workshop is to rekindle some of the interest and enthusiasm towards hardware verification. Through this workshop we would like to encourage new and daring directions, to provide a stage for ideas in early developmental stages, and initiate discussions that define the challenges that remain to be tackled with.
The scope of the workshop will include both general research in formal verification techniques of hardware designs as well as specific issues related to the development of model checking tools. In addition, we will integrate the Hardware Model Checking Competition into the agenda of the workshop, which will further raise the level of interest in the workshop. Combining the competition with the workshop will help us attract papers that are related to the competing tools and make the event more complete in scope.
For more details on the competition and on the submission process for papers, benchmarks and model checkers, see the Call for Papers.
Malay Ganai and
Divjyot Sethi, Yogesh Mahajan and Sharad Malik.
Yongjian Li, William
Hung and Xiaoyu Song.
The slides are available through the links in the program below. Click on the title of the talk.
Thursday, July 15th
09:00‑10:00 Session 1
10:30‑12:30 Session 2
14:00‑15:00 Session 3
15:30‑17:30 Session 4