Formal verification of a SONET data stream processor

We describe the formal verification of an industrial hardware design from PMC-Sierra, Inc. The design under investigation is a telecom system block, which processes a portion of the synchronous optical network (SONET) line overhead of a received data stream. We adopted a hierarchical modelling and verification approach which follows the natural design hierarchy. The formal specification and verification have been carried out based on multiway decision graphs (MDG), a new decision diagram subsuming the traditional binary decision diagrams and allowing abstract data and functions. The verification has been performed using both equivalence and model checking. To measure the performance of the MDG-based model checking, we also conducted a comparative verification of the same design using Cadence FormalCheck.