Browse Prior Art Database

Verification of Finite State Machines using Partial Symbolic Simulation

IP.com Disclosure Number: IPCOM000105593D
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 called LEVER (sequential Logic Equivalence VERification) which performs a functional comparison of two finite state machines [*].

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

Verification of Finite State Machines using Partial Symbolic Simulation

      This bulletin describes a software product called LEVER
(sequential Logic Equivalence VERification) which performs a
functional comparison of two finite state machines [*].

      LEVER performs equivalence verification from an initial state
symbolic vector by comparing the primary outputs which result from
all members of the input alphabet and by recursively performing
equivalence verification on all corresponding successor states.
LEVER's contributions include the use of partial symbolic simulation
to converge at primary outputs with large input cubes.  LEVER makes
more informed decisions for search space refinement by performing
simultaneously enumeration on the two machines for more efficient
coverage of the product machine's state transition graph.  Further,
the input selection heuristic avoids futile simulation and thus,
accelerates the enumeration phase of the algorithm.  Since LEVER
enumerates from restricted symbolic state vectors, it avoids the
expensive validity check for state whenever it sets a present state
bit.  LEVER achieves the greatest lower bound on the worst case
computational complexity of the recursive constraint propagation
algorithm for translating a restricted symbolic state vector to its
corresponding set characteristic function.  It also provides an
additional improvement of the translation process by using
information associated with binary decision graphs...