Verification-Driven Design for Asynchronous VLSI

Although verification has widespread use in hardware design, there is still a gap in verifying the functional description of hardware against its detailed design. In this paper, we present our effort to close that gap. Drawing an analogy from test-driven development in software development, we propose the idea of verification-driven design for hardware design—the hardware design flow should be engineered in a verification-friendly way. We showcase this idea by leveraging a methodology in asynchronous circuit design that is similar to software optimization—complicated, parallel microarchitectural optimizations are derived from a simple, sequential functional description through iterative rewriting. We propose a technique to formally verify these transformations of hardware designs by extending the state-of-the-art translation validation algorithm for software verification. This approach is demonstrated by a superscalar processor example. We assert that our parallel superscalar processor design is equivalent to a sequential non-superscalar processor specification using the translation validation technique presented in this paper.