Model checking of a real ATM switch

In this paper we present our experience on model checking of an Asynchronous Transfer Mode (ATM) switch using the Verification Interacting with Synthesis (VIS) tool. The switch we considered is in use for real applications in the Cambridge Fairisle network. It is composed of four input/output port controllers and a switch fabric, and contains around 1 MB memory, 2 KB FIFO buffer and 800 registers (latches). To overcome state space explosion, we adopted several abstraction and reduction techniques to reduce the model, and applied compositional reasoning combined with a novel property division approach. Using the above techniques, we succeeded in verifying the entire switch at different hierarchy levels within reasonable CPU time