Modeling and verification of an ATM port controller in VIS

In this paper we display a practical approach adopted for the formal verification of Fairisle ATM (asynchronous transfer mode) switch port controller using model checking. The ATM port controller is part of the Cambridge Fairisle ATM network and plays a key role in the ATM switching process. In particular, we present our experience on the model checking of the ATM port controller using the VIS tool from UC Berkeley. To this end, we successfully modeled the port controller behavior and structure in Verilog HDL, established the necessary verification environments and verified a number of relevant temporal properties on the port controller.