Hardware Verification Workshop 2010

First International Workshop

July 15, Edinburgh, United Kingdom
affiliated with CAV'10 at next FLOC'10

[ cfp | invited | competition | overview | accepted | program | dates | slides ]

News

Room 2.11 Thursday July 15th Appleton Tower.

Competition results available.

An interesting related post.

The official Call for Papers is available also in ASCII.

Invited Talks

Why Work on Hardware Verification?
Cindy Eisner
IBM, Israel

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
Sharad Malik
Princeton University, USA

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.

Competition

A total of 21 solvers from 9 research teams participated in HWMCC'10. The results have been presented at the workshop. See the competition page HWMCC'10 for more details.

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.

Overview

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.

Accepted Papers

Malay Ganai and Weihong Li.
Bang for the Buck: Improvising and Scheduling Verification Engines for Effective Resource Utilization
presentation only

Matthias Raffelsieper and Mohammadreza Mousavi.
Efficient Verification of Verilog Cell Libraries
presentation only

Stefan Kupferschmid, Matthew Lewis, Bernd Becker and Tobias Schubert.
Incremental Preprocessing Methods for use in BMC
original paper

Souheib Baarir, Cecile Braunstein, Emmanuelle Encrenaz, Jean-Michel ILIE,
Tun Li, Isabelle Mounier, Denis Poitrenaud and Sana Younes.
Quantifying Robustness by Symbolic Model checking
original paper

Gianpiero Cabodi, Sergio Nocco and Stefano Quer.
Benchmarking a Model Checker for algorithmic improvements and tuning for performance
early stage paper

Divjyot Sethi, Yogesh Mahajan and Sharad Malik.
Specification and Encoding of Transaction Interaction Properties
original paper

Yongjian Li, William Hung and Xiaoyu Song.
Automatically Exploring Structural Symmetry in Symbolic Trajectory Evaluation
original paper

Slides

The slides are available through the links in the program below. Click on the title of the talk.

Program