Design Of Provably Correct Storage Arrays

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

• Type: Conference
• Year: 2001
• Where: VLSID
• Authors: Rajiv V. Joshi, Wei Hwang, Andreas Kuehlmann
• Keywords: Computer Architecture, Dynamic CMOS Circuits, Formal Equivalence Checking, VLSID 2001, Word-wise Organized Rtl