Connecting Pre-silicon and Post-silicon Verification

S. Ray and W. A. Hunt, Jr.

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.

© 2009 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

Abstract

We present a framework for post-silicon analysis, that provides a formal, bidirectional communication with pre-silicon verification. We show how to exploit the framework to provide a formal guarantee on post-silicon verification accuracy under limited observability. In particular, we partition a pre-silicon assertion checker (with full observability) into (1) a limited-observability checker and (2) an in-silicon integrity unit. The composition of the two units is guaranteed to provide the same accuracy as a pre-silicon checker. We apply the framework in the verification of a cache system.

Relevant files