Title :
Practical approaches to the automatic verification of an ATM switch fabric using VIS
Author :
Lu, Jianping ; Tahar, Sofiene
Author_Institution :
Dept. of Electr. & Comput. Eng., Concordia Univ., Montreal, Que., Canada
Abstract :
In this paper we present several practical methods for formally verifying an Asynchronous Transfer Mode (ATM) network switching fabric using the Verification Interacting with Synthesis (VIS) tool. We produced Verilog RTL behavioral and netlist structural descriptions of the switch fabric at different levels of hierarchy and established several abstracted models of the fabric. Using various techniques presented in the paper, we provided a number of relevant liveness and safety properties expressible in CTL, and accomplished their verification in reasonable CPU time. Moreover, we performed equivalence checking between the structural and behavioral descriptions of each submodule of the implementation hierarchy
Keywords :
asynchronous transfer mode; digital systems; formal verification; hardware description languages; telecommunication networks; ATM switch fabric; CTL; VIS; Verilog RTL behavioral descriptions; abstracted models; automatic verification; equivalence checking; implementation hierarchy; liveness properties; netlist structural descriptions; safety properties; verification interacting with synthesis; Asynchronous transfer mode; Circuits; Communication networks; Communication switching; Fabrics; Formal verification; Hardware design languages; Network synthesis; Routing; Safety; Switches;
Conference_Titel :
VLSI, 1998. Proceedings of the 8th Great Lakes Symposium on
Conference_Location :
Lafayette, LA
Print_ISBN :
0-8186-8409-7
DOI :
10.1109/GLSV.1998.665319
