Haifa Verification Conference 2009
October 19-22, 2009
Organized by IBM R&D Labs in Israel
|Tutorials    October 19, 2009|
|Tutorials program PDF version for printing (481 KB)|
|10:00 13:00||Morning Tutorial Post-Silicon 101|
Post-silicon verification is a necessary step in a design's verification process.
Pre-silicon techniques such as simulation and emulation are naturally limited in
scope and volume as compared with what can be achieved on the silicon itself.
Some parts of the verification, such as full-system functional verification,
cannot practically be covered with current simulation technologies. Even core
functional verification - traditionally a central part of simulation based
verification - cannot be fully taken care of before RIT.
In this tutorial the basic concepts and aspects of post-silicon validation will be presented. Speakers from both industry and academia will present the challenges faced by the bring-up team, and how these challenges are addressed.
Rand Gray (Intel) will examine strategies and methods for stimulating and debugging different classes of silicon bugs. A forward looking perspective of microprocessor silicon bugs will also be presented.
Brad Quinton (University of British Columbia) will look at a number of different hardware structures that can be used for post-silicon debug and investigate their area overhead and debug effectiveness.
Allon Adir and Amir Nahir will review the differences and similarities between pre- and post-silicon verification, and explore how the fundamental aspects of verification technologies, namely, stimuli generation, coverage, checking and debugging are affected by these differences.
|10:00||Introduction Amir Nahir, IBM|
|10:10||Post-Silicon Validation: History, Trends, and Challenges Rand Gray, Intel|
|11:30||Post-Silicon Debugging Brad Quinton, University of British Columbia|
|12:15||Bridging the pre/post-silicon gap: stimuli-generation, checking and coverage Amir Nahir and Allon Adir, IBM|
|14:30 16:00||Afternoon Tutorial I Satisfiability Modulo Theories (SMT)|
|Ofer Strichman, Technion|
The "Satisfiability Modulo Theories" (SMT) problem is to decide the satisfiability of
formulas with respect to a first-order background theory for which there exists a
decision procedure such as the theory of equalities, the theory of lists,
and the theory of linear arithmetic.
SMT solvers are routinely used in formal verification, compiler optimization, and scheduling, among others. Microsoft's Z3 SMT solver, for example, is used in many of their program analysis and verification tools.
The tutorial will begin by placing SMT in a broader context and compare it to other methodologies such as constraint solving and automated theorem proving, and will describe the various activities performed in the SMT community. It will then give a brief introduction to first-order theories, and focus on the state of the art in SMT solving.
|16:30 18:00||Afternoon Tutorial II Constraint Satisfaction Problems (CSP) for Verification|
|Eyal Bin, IBM|
Constraint Satisfaction problem (CSP) techniques are widely used in verification as
core engines for building test generators. CSPs focus on problems having variables with
finite discrete domains and constraints that limit the variables' legal assignments.
In this tutorial we will present the CSP's engine algorithms and the basic concepts of variables and constraints. A brief introduction will be given for advanced topics such as variables and values ordering, CSP languages, soft and hard constraints, the role of propagators, and local vs. global constraints.