Hardware modeling and verification of an ATM ring MAC protocol

摘要

In this paper, we describe the modeling and verification of the register transfer level (RTL) design of an ATM ring (ATMR) media access control (MAC) protocol using the VIS hardware verification model checking tool. We succeeded in verifying both a synchronous and an asynchronous design alternative of this MAC. Throughout the verification, we report the performance of hardware protocol verification in model checking, and discuss some modeling techniques we adopted in the verification.