Sciweavers

Share
FMCAD
2007
Springer

Transaction Based Modeling and Verification of Hardware Protocols

10 years 3 months ago
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...
Xiaofang Chen, Steven M. German, Ganesh Gopalakris
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where FMCAD
Authors Xiaofang Chen, Steven M. German, Ganesh Gopalakrishnan
Comments (0)
books