A theory of abstraction for arrays

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.