FMCAD 2008
Formal Methods in Computer Aided Design
Portland, OR, USA
November 17 - 20

Invited Tutorials


Analog and Mixed Signal Verification: The State of the Art and some Open Problems
Kevin Jones (Rambus)
Digital verification is an area of research that has produced many innovations and changes in paradigm over the past 25 years. Analog verification has changed very little. In this talk, I'll present the current tools and approaches in use in practice to set the base line. I'll talk about the state of the art in the field of applying formal methods to these problems, both from the traditional analog domain and some of the recent research applying more "digital" methods. I'll conclude by suggesting some open problems that are good candidates for research activity and indicate where I think the field is going over the next few years.


Building a Bridge: From Pre-Silicon Verification to Post-Silicon Validation
Moshe Levinger (IBM)
Pre-silicon functional verification techniques provide excellent dynamic observability, and static analysis of design models can dramatically increase coverage in selected areas. Yet, only a tiny fraction of the huge reachable state-space can be sampled and verified. Although substantial effort is invested in controlling and intelligently directing the verification resources, state-of-the-art pre-silicon techniques cannot cope with the increasing complexity of modern high-end designs. More bugs continue to escape into the silicon. Should we reset our quality expectation from the pre-silicon design? Can we better exploit silicon-casting samples as yet another verification platform? In this talk we will start by providing an overview of the key simulation-based verification technologies that are commonly used nowadays in the pre-silicon stage. We will then examine opportunities to exploit silicon-casting samples as a verification platform while illustrating which pre-silicon verification methodologies can be adapted to silicon. In addition, we will discuss trade-offs between the different platforms and will point out opportunities to bridge methodologies. Lastly, we will describe a novel post-silicon exerciser -- which is based on key concepts taken from the pre-silicon test generation domain -- that enables systematic implementation of functional-coverage oriented verification plans.


Computing bounds on space and time for hardware compilation
Byron Cook (Microsoft Research lab @ Cambridge)
The inability to automatically compute reasonable bounds on the space and time used by software has been the key problem precluding automatic compilation of software into hardware. However, recent advances now give us methods for automatically computing these bounds on space and time. This tutorial will survey these recent advances and show how they can be used when compiling software into hardware.


Considerations in the Design and Verification of Microprocessors for Safety-Critical and Security-Critical Applications
David S. Hardin (Advanced Technology Center, Rockwell Collins, Inc.)
In this tutorial, we will examine issues in the design and verification of microprocessors for safety-critical and security-critical applications. We will consider architectural and design alternatives to support high-assurance applications, and will describe techniques to improve secure system evaluation -- measured in terms of completeness, human effort required, time, and cost -- through the use of highly automated formal methods. We will describe practical techniques for creating executable formal computing platform models that can both be proved correct, and also function as high-speed simulators. This allows us to both verify the correctness of the models, as well as validate that the formalizations accurately model what was actually designed and built. As a case study, we will examine the design and verification of the Rockwell Collins AAMP7 microprocessor. The AAMP7, currently in use in Rockwell Collins high-assurance system products, supports strict time and space partitioning in hardware, and has received an NSA MILS (Multiple Independent Levels of Security) certificate based in part on proofs of correctness. We will discuss the AAMP7 verification effort, focusing on the proof architecture that enabled us to show that the AAMP7 separation kernel microcode implements a particular security policy, using the ACL2 theorem prover.