| |
Xiang Wu and Rajit Manohar
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.
|
|
