Login | Register

Formal verification of a SONET data stream processor

Title:

Formal verification of a SONET data stream processor

Tahar, Sofiène, Zobair, M.H. and Song, X. (2004) Formal verification of a SONET data stream processor. IEE Proceedings - Computers and Digital Techniques, 151 (1). p. 71. ISSN 13502387

[img]
Preview
Text (application/pdf)
IEECDT-2004.pdf - Accepted Version
299kB

Official URL: http://dx.doi.org/10.1049/ip-cdt:20040034

Abstract

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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Tahar, Sofiène and Zobair, M.H. and Song, X.
Journal or Publication:IEE Proceedings - Computers and Digital Techniques
Date:2004
Digital Object Identifier (DOI):10.1049/ip-cdt:20040034
Keywords:SONET decision diagrams formal verification hardware description languages
ID Code:977382
Deposited By: DANIELLE DENNIE
Deposited On:14 Jun 2013 16:07
Last Modified:18 Jan 2018 17:44
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Back to top Back to top