Browse Prior Art Database

Structured Sequential Machine Comparison

IP.com Disclosure Number: IPCOM000089635D
Original Publication Date: 1977-Nov-01
Included in the Prior Art Database: 2005-Mar-05
Document File: 8 page(s) / 84K

Publishing Venue

IBM

Related People

Evangelisti, CJ: AUTHOR [+4]

Abstract

STATEMENT OF THE PROBLEM The subject matter of this publication is the comparison of two sequential machine models in order to find out whether they are "functionally equivalent". This term is used in a way that is similar to E. F. Moore's use of the term "indistinguishable machines" [1]. Moore defines two machines to be indistinguishable if they are alike in their behavior even though they may differ in their structure. That is, if for every state of one machine there exists a corresponding state of the other machine such that the output of every experiment (input sequence) starting in these respective states is the same, then the two machines are indistinguishable. Such machines can be thought of as being interchangeable.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 21% of the total text.

Page 1 of 8

Structured Sequential Machine Comparison

STATEMENT OF THE PROBLEM The subject matter of this publication is the comparison of two sequential machine models in order to find out whether they are "functionally equivalent". This term is used in a way that is similar to E.
F. Moore's use of the term "indistinguishable machines" [1]. Moore defines two machines to be indistinguishable if they are alike in their behavior even though they may differ in their structure. That is, if for every state of one machine there exists a corresponding state of the other machine such that the output of every experiment (input sequence) starting in these respective states is the same, then the two machines are indistinguishable. Such machines can be thought of as being interchangeable.

The term "functionally equivalent machines" is used to denote a weaker definition of the term "indistinguishable machines", for rather than comparing every input sequence for every state in both machine models for identical external behavior, only transitions which are exercised in performing prescribed functions are compared. To do this for each function, two subsets of the states of each machine model are defined, one for starting states (S1 and S2), the other for final states (F1 and F2). The two machine models are said to be functionally equivalent if for each state in S1 there is a corresponding state in S2 such that the results of any experiment starting in these respective states are the same
(i.e., the final states in F1 and F2 correspond to each other). In particular, the functional equivalency of two models is proven which have been formally described in a language such as LCD (Language for Computer Design) [2].

The principle of verifying the correctness of one sequential machine model by comparing it with another model implicitly assumes that one of the models is known to be correct. Therefore, one model per machine must be verified for correctness independent of any other model. To accomplish this, functional simulation is required. Naturally, such simulation would be most economical and reliable if it is applied to the highest level model of the machine.

The type of verification of present interest is sometimes called vertical validation [3] because it involves proving the correctness of a design as it moves from one level to another in a hierarchical description system.

BACKGROUND.

In recent years, interest has grown in finding verification methods which can be input data independent. Such methods for the general case of comparing two arbitrary sequential machines are not known. However, attempts have been made to solve the problem for some pairs of sequential machines which have a simple relationship. One case which involves such a relationship is that of two isomorphic machines. Two machines are said to be isomorphic if there exists a one-to-one correspondence between their state variables and, also, between their state transition tables. A solution for t...