In this paper we present our experience on model checking of an Asynchronous Transfer Mode (ATM) network switch fabric using the FormalCheck 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. For the verification in FormalCheck, we used the same Verilog code as in [1] with some modifications. We verified an abstracted (1-bit) model of the switch fabric (this model was already verified, using VIS), then verified a 4-bit model, and an 8-bit model of the switch fabric.

Download PS file (PS File)

Download Verilog code for the abstracted model (Verilog Code)

Download Verilog code for the 4-bit model (Verilog Code)

Download Verilog code for the 8-bit model (Verilog Code)

Download the comments appendix (PS File)

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