I. Introduction
With the growing complexity of the internal organization of modern processors and other digital systems, it is important to develop notations, verification methodologies and tools that ensure correctness as well as high performance of the overall design, and allow designers to make design choices. To put things into sharper focus, consider the design of a modern high performance cache coherence protocol as an example. A designer initially conceptualizes the design in terms of atomic transitions that fire under certain conditions, and move request/response packets between various directories, caches, and processor cores. Accumulated experience, starting from Yang et al's early work on UltraSparc-l [1] to more modern ones [2]–[4], shows that designs captured at this level of abstraction (specification level) in languages such as Murphi [5] and TLA+ [6] supporting guard/action style rules can be model checked to eliminate virtually all high level concurrency bugs. It is also widely known that the atomic transitions used at the specification level are implemented in hardware over multiple clock cycles (a transaction in our terminology), with one or more implementation steps happening in each clock cycle of the transaction. In addition, while the specification level models the desired computation according to the interleaving model where only one specification transition fires at a time, the implementation level often starts a second transaction before the first transaction has finished, again to maximize overlapped computation, pipelining, and to take advantage of internal buffers and split transaction buses. In today's design contexts, designers are seriously under-equipped concerning (i) notations that allow them to specify the designs of such aggressively optimized implementations, (ii) theories for formally relating such implementations against specifications, and (iii) compositional methods for verifying implementations against specifications that have already been verified at the interleaving model level for global properties.