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

Volume

2

fYear

2001

fDate

2001

Firstpage

907

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Electrical and Computer Engineering, 2001. Canadian Conference on

Conference_Location

Toronto, Ont.

ISSN

0840-7789

Print_ISBN

0-7803-6715-4

Type

conf

DOI

10.1109/CCECE.2001.933562

Filename

933562