Verification Driven Formal Architecture and Microarchitecture Modeling

Our ability to verify complex hardware lags far behind our capacity to design and fabricate it. We argue that this gap is partly due to the limitations of RTL models when used for verification. Higher level models such as SystemC and SystemVerilog aim to raise the level of abstraction to enhance designer productivity; however, they largely provide for executable but not analyzable descriptions. We propose the use of formally analyzable design models at two distinct levels above RTL: the architecture and the microarchitecture level. At both these levels, we describe concurrent units of data computation termed transactions. The architecture level describes the computation/state updates in the transactions and their interaction through shared data. The microarchitecture level adds to this the resource usage in the transactions as well as their interaction based on shared resources. We then illustrate the applicability of these models in a top-down verification methodology which addresses several concerns of current methodologies.