Formal Analysis in Post-silicon Verification

Background, Motivation, and Goals

The size and complexity of a modern hardware system precludes catching all design errors by functional verification (formal or otherwise) only on pre-silicon models. Indeed, an estimated 50% of modern SoC designs contain functional errors in the first fabricated silicon. Consequently, post-silicon verification has become a critical component of the overall verification flow. Post-silicon verification entails running simulation on first-pass fabricated silicon to detect functional bugs which are missed during pre-silicon validation. Simulations are performed at target clock speeds, which permits significant more runs than can be afforded pre-silicon. However, a key challenge in post-silicon verification is limited observability: only a few of the thousands of important internal signals are observable during normal chip operation. Observability is constrained by the number of pins and size of available internal buffers in the design. The situation is exacerbated by the current architectural trend away from global bus-based architectures towards multi-core processors with point-to-point interconnection links and no central observation point; many of the links exist within the ``sockets'' that hold multiple processor cores, and are thereby inaccessible.

In spite of its obvious importance, there has been little research on the use of formal techniques to improve post-silicon observability. Traditionally, improving observability entails on-chip instrumentation or hooks, for specific internal signals; that is, additional hardware is introduced to monitor internal registers and bus transactions. However, such hooks are typically added on-demand, without analysis of the invariants that are imposed by the protocols implemented by the design. Furthermore, once added, such hooks are subsequently carried over from one design to the next, even when they have become redundant.

The goal of this work is to make use of formal analysis on pre-silicon designs to improve observability of post-silicon events. In particular, we aim to develop techniques that can provide the following:

a formal guarantee on coverage of post-silicon events,
connection between pre-silicon and post-silicon verification in a unified tool flow, and
amelioration of the post-silicon observability problem without reduction in the quality of validation.

One of the techniques that we are exploring in pursuit of the above goals is to make use of formal analysis on pre-silicon designs to improve observability of post-silicon events. The events are extracted from checkers and coverage monitors already available in the post-silicon flow. Given a set of post-silicon coverage points and limits on available observability, our approach consists of two steps. In the first step, we use information flow computation to determine the signals necessary to observe in order to hit the requisite coverage points. The computation accounts for functional design invariants and dependencies among internal signals. In the second step, called checker partitioning, we compute the additional logic to winnow the set of observed signals to meet the observation bound. This is achieved through a logical partitioning of post-silicon checking into into two fragments, namely (1) a small on-chip integrity processor, and (2) an external partial trace analyzer. The integrity processor, being on-chip, has full observability. The external trace analyzer has partial observability but can assume that in-silicon analysis has succeeded for any (partial) trace presented for external analysis. The result is a streamlined methodology for post-silicon analysis, guaranteeing that the coverage points are hit under the given observability bounds. We have successfully used the approach above in the post-silicon analysis of a cache coherence protocol. We are currently extending the approach to other concurrent protocols.

Funding, Personnel, and Organizations

The research has been funded by the Semiconductor Research Corporation under Grant 08-TJ-1849.^[1] Here are the people who have been involved in this research so far in various capacities.

Warren A. Hunt, Jr. — UT Austin
Sandip Ray — UT Austin
Oswaldo Olivo — UT Austin
Arnab Bandyopadhyay — Advanced Micro Devices Inc.
Jayanta Bhadra — Freescale Semiconductor Inc.
Avi Ziv — IBM Corporation
Robert Krug (Alumnus) — UT Austin

We're looking for more help, so if you're interested in the work feel free to talk to us.

Publications

S. Ray and W. A. Hunt, Jr. Connecting Pre-silicon and Post-silicon Verification. In A. Biere and C. Pixley, editors, Proceedings of the 9th International Conference on Formal Methods in Computer-aided Design (FMCAD 2009), Austin, TX, November 2009, pages 160-163. IEEE Computer Society.

^[1] Any opinions, findings and conclusions or recomendations expressed in this material are those of the authors and do not necessarily reflect the views of the Semiconductor Research Corporation.