In this report, we present the practical 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.

Download PDF file (PDF File)

Download source files (Verilog-files.tar.gz)

Send comments and suggestions to: tahar@ece.concordia.ca