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:
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.
 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.