About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
VLSID 2001
Conference paper
Design of provably correct storage arrays
Abstract
In this paper we describe a hardware design method for memory and register arrays that allows the application of formal equivalence checking for comparing a high-level register transfer level (RTL) specification with a low-level transistor implementation. Equivalence checking is increasingly applied in practical design flows to verify regular logic components. However, because of their specific organization and circuit techniques, high-performance implementations of large storage arrays require particular modifications to the general flow that make them suitable for formal equivalence checking. Two techniques are outlined in this paper. First, a special hierarchical verification scheme is described that allows the application of a partitioned comparison approach of the bit-wise organized transistor-level model with the word-wise organized RTL model. Second, a modified switch-level extraction technique is presented that extends the applicability of equivalence checking from regular dynamic CMOS circuits to self-resetting CMOS (SRCMOS) circuits.