FMCAD 2006 Workshop on
                 Pre- and Post-Silicon Verification:
                 Methods and Research Opportunities
 Sponsored by IEEE, CEDA (Council on Electronic Design Automation)
                  In cooperation with ACM SIGDA 
          (Special Interest Group on Design Automation)

                       http://fmcad.org/2006 


                       CALL FOR PARTICIPATION

                November 16, 2006, San Jose, California
              Note: FMCAD 2006 takes place from Nov. 12-16

             ----------------------------------------------
             Early Registration Deadline:  October 22, 2006
             Hotel Registration Deadline:  October 22, 2006
             ----------------------------------------------


Pre-silicon verification refers to the formal verification of detailed
computational structures such as datapaths and controllers, arithmetic
units, memory systems, etc., at the design representation level (e.g.,
register-transfer level). Post-silicon verification, on the other hand,
is the activity of checking whether these functions work correctly in
fabricated silicon.

The technology behind formal pre-silicon verification has been the
subject of decades of research in formal hardware verification.
Nevertheless, given the growing complexities of current designs,
new and efficient algorithms in this space are of critical importance 
to industry.  Post-silicon verification (or "silicon debugging") is 
perhaps an even harder a problem that is on the critical path to future
successes in large-scale integration. While chip testing is a form of
post-silicon verification, the quest for functional testing (beyond 
scan testing), especially under severe observability limitations due 
to packaging, is of growing importance.

This unique post-FMCAD workshop features five invited talks on these
topics by industrial experts with multiple years of experience.  This
workshop provides added confirmation (beyond the main FMCAD conference)
that hardware verification is far from being a solved problem, and that
continued attention must be devoted to this space.  The workshop will
feature an "open mike" session where the attendees can offer their
thoughts on these topics. It is also our intention to issue a workshop
summary report that can be used to alert funding agencies to research
needs in this area.


Workshop Program
========================================================================
Thursday, November 16


9:00-10:00    Christian Jacobi, IBM
              Formal Verification in Industry -- 
              Current State and Future Directions

10:00-11:00   Roope Kaivola, Intel
              Balancing Formal and Dynamic Techniques in
              Validation of Industrial Arithmetic Designs

11:00-11:30   Break

11:30-12:30   Piyush Desai, Intel
              Perils of Post-Si Validation

12:30-14:15   Lunch

14:15-15:15   Viresh Paruthi, IBM 
              Sequential Equivalence Checking across Arbitrary
              Design Transformations: Technologies and Applications

15:15-16:15   Rick Leatherman, MIPS

              On Chip Instrumentation as a Verification Tool

16:15-17:00   All
              Questions and open microphone. Topics of interest
              include discussion of future research directions,
              funding opportunities, and the creation of a
              workshop summary to send to funding agencies.


The workshop is part of FMCAD 2006, the sixth in a series of 
conferences on the theory and applications of formal methods in 
hardware and system verification. FMCAD provides a leading forum 
to researchers in academia and industry for presenting and discussing 
groundbreaking methods, technologies, theoretical results, and tools 
for reasoning formally about computing systems.  In addition to the 
technical program and workshop, FMCAD will offer a full day of 
tutorials, three invited talks, and a panel, as outlined below.


Tutorials (Full day, November 12, 2006)
========================================================================
Edmund M. Clarke (Carnegie Mellon University)
Model Checking with SAT

J Strother Moore (University of Texas at Austin)
Theorem Proving in Verification: The ACL2 System

Leonardo de Moura (Microsoft Research) 
SMT Solvers: Theory & Practice

Jason Baumgartner (IBM)
Integrating FV Into Main-Stream Verification: The IBM Experience


Invited Talks
========================================================================
Ken McMillan (Cadence Berkeley Labs)
What can the SAT Experience Teach us About Abstraction? 

Gerard Holzmann (NASA/JPL Laboratory for Reliable Software)
The Design of a Distributed Model Checking Algorithm for Spin

Amir Pnueli (New York University)
Synthesis of Designs from Property Specifications 


Panel 
========================================================================
Giving the Gorilla some Brains: How can Formal Complement Simulation?

Moderator       Andreas Kuehlmann (Cadence Berkeley Labs)

Invited         Robert Jones (Intel)
Presentations   Life in the Jungle: Simulation vs. Verification

                Wolfgang Roesner (IBM)
                Ecological Niche or Survival Gear? - Improving an
                Industrial Simulation Methodology with Formal Methods

Panelists       Edmund Clarke, Warren Hunt, Robert Jones, Robert Kurshan,
                Wolfgang Paul, Carl Pixley, and Wolfgang Roesner


Organization
========================================================================
Workshop Chair:         Ganesh Gopalakrishnan, Univ. Utah

FMCAD Chairs:           Aarti Gupta, NEC Labs America
                        Panagiotis Manolios, Georgia Tech

Local Arrangements:     Jeremy Levitt, Mentor Graphics
                        Vigyan Singhal, Oski Technology

Webmasters:             Sudarshan Srinivasan, Georgia Tech
                        Daron Vroon, Georgia Tech