Behavioral verification of an ATM switch fabric using implicit abstract state enumeration

We investigate equivalence checking of the RTL hardware implementation of the Cambridge Fairisle Asynchronous Transfer Mode (ATM) 4 by 4 switch fabric against a high-level behavioral specification which has unrestricted frame size, cell length and word width. The verification is based on the reachability analysis of the product machine of the implementation and the specification, both modeled as Abstract State Machines (ASM). Multiway Decision Graphs (MDG) are used to encode both the output and transition relations of the ASMs and of the set of reachable abstract states, allowing implicit abstract state enumeration. Since MDGs avoid model explosion induced by data values, this experiment demonstrates the effectiveness of MDG-based verification as an extension of ROBDD-based approaches