Title :
Model checking of the Fairisle ATM switch fabric using FormalCheck
Author :
Barakatain, Leila ; Tahar, Sofiène
Author_Institution :
Dept. of Electr. & Comput. Eng., Concordia Univ., Montreal, Que., Canada
Abstract :
We describe the 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. For the current verification in FormalCheck, we used the same Verilog HDL code as Lu and Tahar (see Proc. IEEE 8th Great Lakes Symposium on VLSI, Lafayette, Louisiana, USA, p.368-73, 1998) with some modifications. We specified and verified in FormalCheck a set of liveness and safety properties against several model sizes of the switch fabric. First, we verified an abstracted (1-bit) model of the switch fabric, which was already verified using VIS. Then, we accomplished the verification of a 4-bit model, and the full 8-bit model. We furthermore provide a comparative study between the verification results in VIS and FormalCheck
Keywords :
asynchronous transfer mode; formal verification; hardware description languages; packet switching; telecommunication computing; telecommunication networks; 1 bit; 4 bit; 8 bit; ATM network switch fabric; Fairisle ATM switch fabric; FormalCheck tool; Verilog HDL code; abstracted model; asynchronous transfer mode; model checking; safety properties; Asynchronous transfer mode; Communication networks; Communication switching; Electronic mail; Fabrics; Formal verification; Hardware design languages; Safety; Switches; Transmission lines;
Conference_Titel :
Electrical and Computer Engineering, 2001. Canadian Conference on
Conference_Location :
Toronto, Ont.
Print_ISBN :
0-7803-6715-4
DOI :
10.1109/CCECE.2001.933562
