Modeling and formal verification of the Fairisle ATM switch fabric using MDGs

In this paper, we present several techniques for modeling and formal verification of the Fairisle asynchronous transfer mode (ATM) switch fabric using multiway decision graphs (MDGs). MDGs represent a new class of decision graphs which subsumes Bryant´s reduced ordered binary decision diagrams (ROBDDs) while accommodating abstract sorts and uninterpreted function symbols. The ATM device we investigated is in use for real applications in the Cambridge University Fairisle network. We modeled and verified the switch fabric at three levels of abstraction: behavior, and register transfer level (RTL) and gate levels. In a first stage, we validated the high-level specification by checking specific safety properties that reflect the behavior of the fabric in its real operating environment. Using the intermediate abstract RTL model, we hierarchically completed the verification of the original gate-level implementation of the switch fabric against the behavioral specification. Since MDGs avoid model explosion induced by data values, this work demonstrates the effectiveness of MDG based verification as an extension of ROBDD-based approaches. All the verifications were carried out automatically in a reasonable amount of CPU time