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 verifipproach 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...

• Type: Conference
• Year: 2007
• Where: FMCAD
• Authors: Xiaofang Chen, Steven M. German, Ganesh Gopalakrishnan
• Keywords: Atomic Guard/action Transitions, FMCAD 2007, Formal Methods, Implementation Transitions, Specification Transition