Practical approaches to the verification of a telecom megacell using FormalCheck
Leila Barakatain, Sofiène Tahar, Jean Lamarche, Jean-Marc Gendreau · 2001
In this paper we present practical approaches to formally verify the RTL implementation of a Telecom megacell using model checking techniques based on the FormalCheck tool. We adopted a hierarchical verification method, which relies on the built-in hierarchy of the design as the mechanism to conquer its verification complexity. We then applied a number of tool guided abstraction and reduction techniques within FormalCheck to avoid state space explosion. The case study we considered is the Transmit Master/ Receive Slave (TMRS) Telecom megacell from PMC-Sierra, Inc., implementing a SCI-PHY (Saturn Compatible Interface for ATMPHY devices) protocol. Using our approaches, we succeeded the model checking of the TMRS design and were able to uncover a number of flaws in the RTL design as well as in the documentation specification.