ATM switch design by high-level modeling, formal verification and high-level synthesi
- 1 October 1998
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Design Automation of Electronic Systems
- Vol. 3 (4) , 554-562
- https://doi.org/10.1145/296333.296342
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.Keywords
This publication has 3 references indexed in Scilit:
- Formal verification of an ATM switch fabric using multiway decision graphsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Bug identification of a real chip design by symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- An integration of model checking with automated proof checkingPublished by Springer Nature ,1995