Browse Prior Art Database

Massively Parallel Approach to Finite State Machines Verification

IP.com Disclosure Number: IPCOM000105626D
Original Publication Date: 1993-Aug-01
Included in the Prior Art Database: 2005-Mar-20
Document File: 2 page(s) / 43K

Publishing Venue

IBM

Related People

Gonsalves, G: AUTHOR

Abstract

This bulletin describes a software product for the verification of Finite State Machines (FSMs) called MP-LEVER (Massively Parallel sequential Logic Equivalence VERification) which utilizes the computing power of the Connection Machine [*] to verify designs which could not be handled by previous methods.

This text was extracted from an ASCII text file.
This is the abbreviated version, containing approximately 73% of the total text.

Massively Parallel Approach to Finite State Machines Verification

      This bulletin describes a software product for the verification
of Finite State Machines (FSMs) called MP-LEVER (Massively Parallel
sequential Logic Equivalence VERification) which utilizes the
computing power of the Connection Machine [*]  to verify designs
which could not be handled by previous methods.

      MP-LEVER performs FSM verification by simultaneously processing
different primary input/present state pairs on the Connection
Machine's processing elements (PEs) until all reachable state pairs
have been examined.  MP-LEVER maintains local input stacks and
balances the tasks among the PEs to enable each PE to continue to
enumerate different portions of the state transition graph despite
differences in the convergence rates.  Further, MP-LEVER accomplishes
convergence at primary outputs with large input cubes by using
partial symbolic simulation and avoids the expensive backtracking,
validity check for states by enumerating from restricted symbolic
state vectors.  Instead of conventional backtracking methods,
MP-LEVER uses tagged simulation to propagate influence information
for subsequent refinement of the input space to enable memory folding
for increased capacity and performance.  Another technique uses
refined tag propagation to create abbreviated influence tables for an
additional increase in capacity with minimal impact to convergence
rates.

      MP-LEVER's contributions...