- 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 1MB memory, 2KB FIFO
buffer and 800 registers (latches). To perform model checking on the switch,
we adopted several abstractions and reductions, and applied compositional
reasoning and property division approaches. For the verification in VIS,
we produced Verilog descriptions of the switch at different levels of design
hierarchy and defined a number of relevant properties in CTL. Using the
above techniques, we succeeded in verifying the switch at different hierarchy
levels within reasonable CPU time, and thus illustrated the applicability
of model checking to large designs containing a considerable number of
state-holding elements. In addition, we succeeded in discovering several
injected design errors in both the fabric and the port controllers.
 Download
postscript file (PS
File) |
| Send comments
and suggestions to:
tahar@ece.concordia.ca |