Manipulations of FSMs Represented as Sequential Circuits - The Unknown Component Problem: Theory and Applications - page 113

Chapter 7
Manipulations of FSMs Represented
as Sequential Circuits

In many cases, hard computational problems can be reformulated using decompo-
sition and partitioning, which can lead to computational advantages. An example
is image computation, which is a core computation in formal verification. In its
simplest form, the image of a set of states is computed using the formula:

Img.ns/ D9 i;cs ŒT .i; cs; ns/ : .cs/;

where T.i;cs;ns/ is the transition relation, .cs/ is the set of current states, i is
the set of input variables, and cs.ns/ is the set of current (next) state variables. The
image, Img.ns/ , is the set of states reachable in one transition under all possible
inputs from the current states, .cs/ , using the state transition structure given by

T.i;cs;ns/ . 1
When the state transition structure is given by a sequential network, the transition
relation can be represented, for example, in partitioned form using a set of next
state functions, fT k .i; cs/g , which update the state of each latch. 2 The partition,

fT k .i; cs; ns k /g , represents how the next state of each latch, ns k , depends on the

values of inputs, i , and the current state, cs , of all latches:

T k .i; cs; ns k / D Œns k T k .i; cs/:

The complete transition relations can be derived as the product of the next state
functions as follows:
T.i;cs;ns/ D Y
k

T k .i; cs; ns k / D Y
k

Œns k T k .i; cs/:

1 We do not distinguish between sets, relations, and their characteristic functions. Therefore, it is
possible to think of .cs/ , Img.ns/ ,and T.i;cs;ns/ as completely specified Boolean functions
represented using e.g. BDDs.
2 In this section, we will illustrate the concepts using next state functions, but the computations also
work for the case of non-deterministic relations.