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.
Schedule
10:00	Introduction Amir Nahir, IBM
10:10	Post-Silicon Validation: History, Trends, and Challenges Rand Gray, Intel
11:10	Break
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
13:00	Lunch

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.

• Avi Ziv

  General Chair

• Kedar Namjoshi

  Program Chair

• Andreas Zeller

  Program Chair

• Efrat Maimon

  Webmaster

Springer Lecture Notes in Computer Science