Full text available in:
Adobe Acrobat .pdf format
Word .doc format

Formal Verification: A New Partial Order Approach

Lubomir Ivanov
Department of Computer Science
Iona College
715 North Avenue
New Rochelle, NY 10801
livanov@iona.edu
Ramakrishna Nunna
Department of Electrical and Computer Engineering
California State University Fresno, MS 94
Fresno, CA 93740
rnunna@csufresno.edu
Abstract
Verification methodologies are trying to catch up with the increasing  functionality and complexity of ASICs and Systems on Chips. Traditional simulation based procedures, though vital in certain segments of the overall design, are not efficient for large scale structures.  In this paper, we explore the suitability of partial orders for formal verification of hardware. We present a new partial order verification approach based on the inductively defined notion of a series-parallel poset. Series-parallel posets can be used to model the behavior of combinational and finite state machine systems. We also show how to define temporal verification properties and how to check for the satisfaction of these properties within the behavior of the system.