Hardware Reference
In-Depth Information
We call
T.i;cs;ns/
the
monolithic
representation of the transition relation and
contrast it with the representation in terms of the partition,
fT
k
.i; cs; ns
k
/g
.Many
problems can be solved using a partitioned representation without ever resorting
to the monolithic one, which may be impossible for larger problems. For example,
the image computation can be performed using the partitioned representation by
scheduling those
cs
variables, which do not appear in some parts, to be quantified
earlier . In practice, this approach to image computation leads to significantly
smaller intermediate BDDs, and has been responsible for dramatic increases, both
in efficiency and in the sizes of problems that formal verification can solve.
In this chapter, we discuss how to use the partitioned representation for solving
language equations of the type
F X D S
, for the case when the automata for
F
and
S
are prefix-closed and represented by multi-level sequential networks. We
show how the partitioned representation can be used to perform the basic operations
of language equation solving: completing, complementing, determinizing, hiding,
and computing the product of finite automata. An important aspect is that we show
how most of these operations can be reformulated in terms of image computations,
and hence can take advantage of the efficient developments in this area.
7.1
Problem Statement
The interaction of
F
and
X
within the specification
S
isshowninFig.
7.1
.
3
The
external input and output variables are represented by symbols
i
and
o
, respectively.
The internal variables that are the inputs and outputs of
X
are represented by
symbols
u
and
v
, respectively.
We assume that the behaviors of the components
F
and
S
are represented by
multi-level sequential networks, similar to the one in Fig.
7.2
. The external variables
i
o
F
v
u
X
Fig. 7.1
Topology with
known component
F
,
unknown component
X
and specification
S
S
3
The results of this chapter are not limited to the particular topology of Fig.
7.1
, but we confine the
discussion to that of Fig.
7.1
for ease of presentation.
Search WWH ::
Custom Search