ATM switch design by high-level modeling, formal verification and high-level synthesi

ABSTRACT

Asynchronous Transfer Mode (ATM) has emerged as a backbone for high-speed broadband telecommunication networks. In this paper, we present ATM switch design, starting from a parametric high-level model and debugging the model using a combination of formal verification and simulation. The model has been used to synthesize ATM switches according to customers' choices, by choosing concrete values for each of the generic parameters. We provide a pragmatic combination of simulation, model checking, and theorem proving to gain confidence in the ATM switch design correctness.

REFERENCES

• 1: CHANEY, T., FINGERHUT, J. A., FLUCKE, M., AND TURNER, J. 1996. Design of a gigabit ATM switching system. Tech. Rep. WUCS-96-07 (Feb.). Computer Science Dept. Washington Univ. St. Louis.
• 2: CHEN, B., YAMAZAKI, M., AND FUJITA, M. 1994. Bug identification of a real chip design by symbolic model checking. In Proceedings of the European Conference on Design Automation, the European Test Conference (Paris, France, Feb.). IEEE Computer Society Press, Los Alamitos, CA, pp. 132-136.
• 3: CURZON, P. 1994. The formal verification of the fairisle ATM switching element. Tech. Rep. 328 and 329 (March). Computer Laboratory, Univ. Cambridge, Cambridge, U.K.
• 4: Mike Tien-Chien Lee , Yu-Chin Hsu , Ben Chen , Masahiro Fujita, Domain-specific high-level modeling and synthesis for ATM switch design using VHDL, Proceedings of the 33rd annual conference on Design automation, p.585-590, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240629]
• 5: Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
• 6: S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995
• 7: S. Tahar , Z. Zhou , X. Song , E. Cerny , Michel Langevin, Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs, Proceedings of the 6th Great Lakes Symposium on VLSI, p.106, March 22-23, 1996

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Design, Verification

Keywords:
ATM switch, high-level design, synthesis, verification