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 |