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

exists in the resultant automaton of Procedure 2, then subset state fs 1 ;:::;s k g must
exist in the resultant automaton of Procedure 1. Observe that

• DC state is non-accepting. A subset state is accepting if and only if one of

its states is accepting. Thus, state fs 1 ;:::;s k g is accepting if and only if state

fs 1 ;:::;s k ;DCg is accepting.

• Under any transition condition, the successor states of fs 1 ;:::;s k g are the same

as those of fs 1 ;:::;s k ;DCg except that the latter contains the DC state.

Applying induction on the state space with the above two facts, it follows that subset
states s 1 ;:::;s k and s 1 ;:::;s k ;DC are equivalent. On the other hand, if a subset
state s 1 ;:::;s k or s 1 ;:::;s k ;DC can transition to the singleton subset state fDC g
under some transition condition, then all of the member states s 1 ;:::;s k must be
incomplete under this transition condition. Therefore, it is immaterial whether the
completion is done before or after the determinization. t

Other trivial propositions state that completion commutes with both the comple-
mentation and product operations. Corollary 7.3 follows from these observations
and Theorem 7.2 .

Corollary 7.3. Let X be the solution obtained when F and S are not completed

and let Y be the solution when F and S are made complete first. Then the languages

of X and Y are identical.

7.4 Experimental Results

In this section, an implementation using the partitioned representations is com-
pared with the implementation using the monolithic representations. In effect, the
partitioned implementation performs only the determinization procedure, which
subsumes all other steps, as described above. In the case of the monolithic
representations, the completion of S is done first, then the intermediate product
is derived, followed by hiding and determinization, performed in a traditional way.
The examples for this experiment were derived from FSM benchmarks by the
operation called latch splitting . It is explained in Chaps. 11 and 13. It is a syntactic
transformation of a sequential circuit into two circuits, one containing a subset of
the latches of the original circuit and the other containing the rest. One of these
becomes the fixed component, F , in the language solving problem while the other
represents a particular solution, X P , for the “unknown” component. The sequential
behavior of the original circuit is used as the specification. We compute the largest
FSM solution called CSF (complete sequential flexibility). Since X P , is a particular
solution, it is contained in the CSF.
After the computation of CSF, it was formally verified by checking:

1. X P CSF ,and

2. F CSF S D F X P .