Transaction Based Modeling and Verification of Hardware Protocols

Modeling hardware through atomic guard/action transitions with interleaving semantics is popular, owing to the conceptual clarity of modeling and verifying the high level behavior of hardware. In mapping such specifications into hardware, designers often decompose each specification transition into sequences of implementation transitions taking one clock cycle each. Some implementation transitions realizing a specification transition overlap. The implementation transitions realizing different specification transitions can also overlap. We present a formal theory of refinement, showing how a collection of such implementation transitions can be shown to realize a specification. We present a modular refinement verification approach by developing abstraction and assume-guarantee principles that allow implementation transitions realizing a single specification transition to be situated in sufficiently general environments. Illustrated on a non-trivial VHDL cache coherence engine, our work may allow designers to design high performance controllers without being constrained by fixed automated synthesis scripts, and still conduct modular verification.