Model checking of the Fairisle ATM switch fabric using FormalCheck
Leila Barakatain, Sofiène Tahar · 2002
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.