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
FMCAD 2011
Conference paper
A theory of abstraction for arrays
Abstract
We develop a theory for reasoning about temporal safety properties of systems with arrays. The theory leads to an automatic algorithm for constructing sound and complete abstractions. Our approach has advantages over previous approaches for important classes of digital designs, including designs with clock gating. We define a function that gives, in a certain sense, the size of the smallest sound and complete array abstraction of a system. This function is difficult to compute. However, we present a static analysis algorithm that efficiently computes a safe size of a sound and complete abstraction by overapproximating the minimum size. Our algorithm can often construct abstractions with small arrays for complex industrial designs. © 2011 FMCAD.