Formal verification of the RCMP egress routing logic [ATM]

In this paper, we present our results on the formal verification of an egress traffic module using CTL model checking. The design considered is a commercial product obtained from PMC-Sierra, Inc. and is used by the RCMP (routing, cell counting, monitoring, policing) process in a network port interface for an ATM switch fabric. The available behavioral level VHDL design was translated to a synthesizable Verilog set and verification was carried out using the VIS (verification interacting with synthesis) tool. One design error which could lead the system into a hang-up state was detected through the verification of a set of liveness and safety properties. The design error was also confirmed through Synopsys-VSS and Verilog-XL simulations.