Sequential optimisation without state space exploration.
We propose an algorithm for area optimization of sequential circuits through redundancy removal. The algorithm finds compatible redundancies by implying values over nets in the circuit. The potentially exponential cost of state space traversal is avoided and the redundancies found can all be removed at once. The optimized circuit is a safe delayed replacement of the original circuit. The algorithm computes a set of compatible sequential redundancies and simplifies the circuit by propagating them through the circuit. We demonstrate the efficacy of the algorithm even for large circuits through experimental results on benchmark circuits.
Introduction
Sequential optimisation seeks to replace a given sequential circuit
with another one optimised with respect to some criterion
area, performance or power, in a way such that the environment
of the circuit cannot detect the replacement. In this work,
we deal with the problem of optimising sequential circuits for
area. We present an algorithm which computes sequential redundancies
in the circuit by propagating implications over its
nets. The redundancies we compute are compatible in the
sense that they form a set that can be removed simultaneously.
Our algorithm works for large circuits and scales better than
those algorithms that depend on state space exploration.
The starting point of our work is [1], in which a method was
described to identify sequential redundancies without exploring
the state space. The basic algorithm is that for any net, two
cases are considered: the net value is 0 and the net value is 1.
For each case, constants as well as unobservability conditions
are learnt on other nets. If some other net is either set to the
same constant for both cases, or to a constant in one case and
is unobservable in the other, it is identified as redundant. For
example, consider the trivial circuit shown in Figure 1. For
the value the net n2 is unobservable and for the value
the net n2 is 1. Thus net n2 is stuck-at-1 redundant.
However, the redundancies found by the method in [1] are not
compatible in the sense that they remain redundant even in the
University of California at Berkeley, Berkeley, CA 94720
Cadence Berkeley Labs, Berkeley, CA 94704
# University of Texas at Austin, Austin,

Figure

1: Example of incompatible redundancies
presence of each other. For instance, the redundancy identification
algorithm will declare both the inputs n 1 and n 2 as
stuck-at-1 redundant. However, for logic optimisation, it is incorrect
to replace both the nets by a constant 1.
The straightforward application of Iyer's method to redundancy
removal is to identify one redundancy by their implication
procedure, remove the redundancy and iterate until con-
vergence. Our goal to learn all compatible implications in the
circuit in one step and use the compatibility of these implications
to remove all the redundancies simultaneously (in this
sense our method for finding compatible unobservabilities is
related to the work in [2, 3] for computing compatible ODC's
(observability don't cares). This is our first contribution. Sec-
ondly, we generalise the implication procedure by combining
it with recursive learning [4] to enhance the capability of the
redundancy identification procedure. Recursive learning lets
us perform case split on unjustified gates so that it is possible
to learn more implications at the expense of computation time.
Consider the circuit in Figure 2. Setting net a to 0 implies that
net f is 0. If we set a to 1, a1 becomes 1, but the AND-gate
connected to remains unjustified. If we perform recursive
learning for the two justifications:
the former case, net f becomes 0, and for the latter case, f becomes
unobservable because e is 1. Thus, for all the possible
cases, either f is 0 or it is unobservable. Hence f is declared
stuck-at-0 redundant. Recursive learning helps identify these
kinds of new redundancies. We present data which shows that
we are able to gain significant optimisations on large benchmark
circuits using these two new improvements. In fact, for
some circuits, we find that recursive learning not only gives us
more optimisation, it is even faster since a previous recursive
learning step makes the circuit simpler for a later stage.
We do not assume designated initial states for circuits. For
sequential optimisation, we use the notion of c-delay replacement
[1, 5]. This notion guarantees that every possible input-output
behaviour that can be observed in the new circuit after
it has been clocked for c cycles after power-up, must have been
present in the old circuit. In contrast to the work in [5, 6], the
synthesis method presented here does not require state space
a
e
d
c
f

Figure

2: Example of recursive learning
a
d
c o1
a
d
c

Figure

3: A circuit and its graph
traversal, and can therefore be applied to large sequential cir-
cuits. Recursive learning has been used earlier for optimi-
sation, as described in [7], but their method is applied only
to combinational circuits and they do not use unobservability
conditions. Another procedure to do redundancy removal is
described in [8], but as [9] shows, their notion of replacement
is not compositional and may also identify redundancies which
destroy the initialisability of the circuit. We have therefore
chosen to use the notion of safe delayed replacement which
preserves responses to all initializing sequences. We are interested
in compositionality because we would like a notion
of replacement that is valid without making any assumptions
about the environment of the circuit. This is why our replacement
notion is safer than that used in [10] which identifies sequential
redundancies by preserving weak synchronizing se-
quences. Their work implicitly assumes that the environment
of the circuit has total control so that it can supply the arbitrary
sequence that the redundancy identification tool has in mind.
Our approach does not pose any such restrictions.
The rest of the paper is organised as follows. In Section 2,
we present our algorithm to compute compatible redundancies
on combinational and sequential circuits. In Section 3, we
present experimental results on some large circuits from the
ISCAS benchmark set. In Section 4, we conclude with some
directions for future work.
Redundancy Removal
We present an algorithm for sequential circuits that have been
mapped using edge-triggered latches, inverters and 2-input
gates; note that any combinational implementation can be
mapped to a circuit containing only inverters and 2-input gates.
We use the notion of circuit graph for explaining our algorithm.
A circuit graph is a labelled directed graph whose vertices correspond
to primary inputs, primary outputs, logic gates and
latches, and edges correspond to wires between the elements
of the circuit. The label of a vertex identifies the type of ele-

Figure

4: Rules for implying constants
ment it represents (e.g. two-input gates, inverters or latches).
We refer to an edge in the circuit graph as a net. Figure 3 shows
an example of a circuit graph.
2.1 Combinational redundancies
We explain our algorithm and prove its correctness for combinational
circuits and later extend it to sequential circuits. Consider
a circuit graph of a circuit, where V is the
set of vertices and E is the set of nets. An assumption A on
the subset P ' E is a labelling of the nets in P by values from
the set f0;1g. Let n 2 P be a net. We
labels the net n with the value v. An assumption is denoted by
an ordered tuple. The set of all possible assumptions on the
set P of nets is denoted by A P . Consider the set
The assumption labeling m with 0 and n with 1 is denoted
by hm 7! 0;n 7! 1i and A
1i;hm 7! 1;n 7! 0i;hm 7! 1;n 7! 1ig. An assumption A 2 A P
is inconsistent if it is not satisfiable for any assignments to the
primary inputs of the circuits. For instance, an assumption of 0
at the input and 1 at the output of an AND gate is inconsistent.
In the algorithm, values are implied at nets in E nP from an
assumption on P. We imply either constants or unobservability
indicators at nets. We indicate unobservability at a net by
implying a symbolic
value\Omega at it. Let be the set
of all possible value that can be implied at any net. An implication
is a label (n is a net and r 2 R. Figure 4
illustrates the rules for implying constants. Rules C1, C2, C3
and C5 are self-explanatory. Rule C4 states that for an AND
gate, 0 at the output and 1 at an input implies 0 at the other
input. Rule C6 states that a constant at some fanout net of a
gate implies the same constant at all other fanout nets. Figure
5 illustrates the rules for
implying\Omega 's. Rule O1 states that
0 at an input of an AND gate implies
a\Omega at the other input.
Rule O2 states that
a\Omega at every fanout net of a gate implies
a\Omega at every fanin net of that gate. Note that constants can
be implied in both directions across a gate
while\Omega propagates
only backwards. We have shown rules only for inverters and
AND gates but similar rules can be easily formulated for other
gates as well. We use these rules to label the edges of the
circuit graph. A constant (0 or 1) label on a net indicates that
\Omega \Omega \Omega \Omega \Omega \Omega

Figure

5: Rules for implying unobservability0a e1
c
b d
\Omega \Omega \Omega

Figure

Overwriting constants with unobservability indicator

the net assumes the respective constant value under the current
assumption.
A\Omega label indicates that the net is not observable
at any primary output. Hence, it can be freely assigned to either
or 1 under the current assumption. Suppose for every
assumption in A P , some net n is labelled either with constant v
or
with\Omega , then we can safely replace n with constant v. This
is because we have shown that under every possible assump-
tion, either the net takes the value v or its value does not affect
the output. We can therefore conclude that net n is stuck-at-v
redundant.
We are concerned about the compatibility of all labellings
because otherwise we run the danger of marking nets with labels
so that all labels are not consistent. For example, consider
the circuit in Figure 1. For the purpose of identifying
redundancies, [1] would infer the implications
from the assumption hn 7! 1i. Additionally, the assumption
hn 7! 0i implies that
hn 7! 0i implies that (notice that we use
the
symbol\Omega to denote compatible observability as opposed to
which simply denotes observability). So, [1] would rightly
claim that both n1 and are stuck-at-1 redundant in isola-
tion; however, for redundancy removal it is easy to see that we
cannot This is why we want to make all labelings compatible.
A sufficient condition for the redundancies to be compatible
is to ensure that the procedure for computing implications from
an assumption returns compatible implications, i.e., every implication
is valid in the presence of all other implications. It is
easy to see that if the labelling of edges in the circuit graph is
done by invoking the rules described above and no label is ever
overwritten, then the set of learnt implications will be compat-
ible. For instance, in the circuit of Figure 1, once n1 is labelled
a\Omega cannot be inferred at because (n1
be overwritten with 0). But this approach is conservative
and will miss some redundancies. In Figure 6, we show
an example where overwriting a constant with
a\Omega yields a
redundancy which could not have been found otherwise. We
propagate implications from assumptions on the net a. The
redundancy remove
/* find and remove redundancies from the circuit graph */
while (there is an unvisited net n in the circuit graph) f
S := learn implications (G , hn 7! 1i)
S := learn implications (G , hn 7! 0i)
R := T -T
for every implication set net n to constant v
propagate constants and simplify
learn implications
propagate implications on the circuit graph given an assignment */
f
forall n such that A : n 7! v f
label n / v
while (some rule can be invoked) f
b) be the new implication
if (b
label n / b
conflicts with a current label)
return
else
label n / b
return set of all current labels

Figure

7: Combinational redundancy removal algorithm
implications from ha 7! 0i are written below and those from
ha 7! 1i are written above the wires. Note that while propagating
implications from ha 7! 1i, a2 and d are initially labeled
with 1 but after labelling c with 0, the labels at d and
a2 are successively overwritten
's. Hence, a2 is found
to be stuck-at-0 redundant. As a result, the OR gate can be re-
moved. We prove later in this section that this overwriting does
not make previously learnt implications invalid, i.e., compatibility
of implications is maintained, if the only overwriting that
is allowed is that of constants with unobservability indicators.
Our algorithm for removing combinational redundancies is
given in Figure 7. The function learn implications takes as input
an assumption A on an arbitrary subset of nets and labels
nets with values from f0;1; learnt through implications.
Initially all nets n such that A : n 7! v is an assumption, are la-
belled. Then we derive new labels by invoking the rules C1-C6
and O1-O2 and similar rules for other kinds of two input gates.
Note that at all times each net has a unique label and constants
can be overwritten
with\Omega 's but not vice-versa. It returns the
set of all final labels. The function redundancy remove takes
as input a circuit graph G and calls learn implications successively
with assumptions hn i 7! 0i and hn i 7! 1i on the singleton
subset fn i g. The two sets of labels are used to compute
all pairs n and v such that n is stuck-at-v redundant. We
later show that our labelling procedure for learning implications
guarantees that all such redundancies can be removed
f
d
c
d
e
f
a
c e
a

Figure

8: An implication graph
simultaneously. These redundancies are used to simplify the
network. The process is repeated until all nets have been con-
sidered. Note that the function redundancy remove considers
assumptions on only a single net but in general any number of
nets could be used to generate assumptions. We later show results
for the case when we considered assumptions on two nets,
the second one corresponding to the unjustified node closest to
This is an instance of recursive learning.
We now formalise the notion of a valid label as one for
which an implication graph exists. We will use the notion
of implication graph for proving the compatibility of the set
of labels generated by the algorithm. Let A be an assumption
on a set P of nets. An implication graph for the label
from assumption A is a directed acyclic graph G I = (V I
where L I is a set of labels of the form (m = a) for some net m
and some a 2 f0;1; labelling every vertex v 2V I , such that
ffl Every root 1 vertex is labelled with
m 7! a
ffl There is exactly one leaf 2 vertex v 2V I which is labelled
ffl For any vertex v 2 V I , if v is not a root node the implication
labelling it can be obtained from the implications
labelling its parents by invoking an inference rule.
An example of an implication graph for the label
from the assumption hn8 7! 1i is shown in Figure 8. A set of labels
C derived from an assumption A is compatible if for every
label C2C there exists an implication graph
of C from A such that LC ' C .
We now prove the compatibility of implications returned by
our labelling procedure. At each step, the labelling procedure
either labels a node for the first time or overwrites a constant
with
a\Omega . We prove the invariant that at any time, the current
set of implications C is compatible. We must prove that if a
label is overwritten with a new label, every other label must
have an implication graph which does not depend on the over-written
label. This claim is proved in the following lemma
and is needed for all current labels to be simultaneously valid.
1 A vertex with no incoming edges
A vertex with no outgoing edges
Note that overwriting a 0 with a 1 (or vice-versa) implies an
inconsistent assumption and the procedure exits.
Lemma 2.1 Let A be a consistent assumption. If a label
a) is overwritten by the label (m
=\Omega ) in the current set of
labels, then for all labels (n there is an implication
graph such that a) is not a label of any vertex in the
graph.
Proof: We call net m a parent of net n if there is a node v of the
circuit graph such that m is an incoming arc and n an outgoing
arc of v. We also say that n is a child of m. We say m is a sibling
of n if there is a node v such that both m and n are outgoing
edges of v.
We prove the claim by contradiction. Suppose it is false.
Let the replacement of a) by (m
=\Omega ) be the first instance
that makes it false. Therefore, there was an implication
graph for each current implication before this happened. Let
be an implication that does not have a valid implication
graph now. Consider any path in the old implication graph
for a net n j , (n
is the ith implication on the path. We consider the case where
b j is a constant. Hence, all b k 's in the path are constants since
a\Omega at a net can only imply
a\Omega at another. The case in which
=\Omega is considered later. We show that if the assumption A is
consistent then it is possible to replace n in the implication
graph for n j . There are three cases on the relation between
Case 1: The circuit edge n i\Gamma1 is a child of n i
.\Omega can be
inferred at n i only if either n
=\Omega is a current implication
or current implication and n i 0
and n i are inputs to
an AND gate. In the first case, the fact that an implication
graph existed in which n i\Gamma1 was labelled with a constant is
contradicted. In the second case, n i\Gamma1 is the output of an AND
gate, whose two inputs are n i and n i 0 . Since (n
and In either
case
Case 2: n i\Gamma1 and n i are siblings and (n
is an application of Rule C6. If n i+1 is either the parent or a
sibling of n i then can be removed from the implication
graph for
implication. If n i+1 is a child of n i ,
then\Omega can be inferred at
=\Omega is a current implication or n i
is a current implication and n i and n i are inputs to an AND
gate. In the first case, the fact that an implication graph existed
in which n i+1 was labelled with a constant is contradicted. In
the second case, clearly n i+1 is labelled with 0, i.e., b
otherwise the assumption A is inconsistent, and the path (n
can be replaced by the path (n
Note that to get a new implication graph for
we need the implication graph for n but that exists
and is not affected by the overwriting of the previous label of
with\Omega .
e
a g
x
c
d
f
y

Figure

9: Sequential circuit C
Case 3: n i\Gamma1 is a parent of n i . The reasoning is same as in
Case 2.
Thus we have shown that if the assumption was consistent,
each vertex labelled with (n in the implication graph of a
current implication (n can be replaced with some other
current implication. This shows that the replacement of n
by
=\Omega does not falsify the claim which is a contradiction.
Now we consider the case in which b j
=\Omega . Then, there
is a greatest k such that b k is a constant, b l is constant for all
=\Omega for all k ! l - j. From the proof before,
we know there exists an implication graph for n k in which
not used. This yields an implication graph for
in which n used.
Lemma 2.2 Let A be a consistent assumption. Then the set of
labels returned by the algorithm is compatible.
Proof: At each step in the algorithm, either a value is implied
at a net for the first time or a constant is overwritten by
a\Omega .
The proof of this lemma follows by induction on the number
of steps of the algorithm and by using Lemma 2.1 to prove the
induction step.
Theorem 2.1 Let n i stuck-at-v i redundant, for all 1
be the set of redundant faults reported by the algorithm. Then
the circuit obtained by setting combinationally
equivalent to the original.
2.2 Sequential redundancies
Now we extend the algorithm for combinational circuits described
in the previous section to find sequential redundancies
by propagating implications across latches. The implications
may not be valid on the first clock cycle since the latches
power-up nondeterministically and have a random boolean
value initially. Nevertheless, we can use the notion of k-
delayed replacement which requires that the modified circuit
produce the same behaviour as the original only after k clock
cycles have elapsed. Thus, for example, if implying constant
v at a latch output from constant v at its input yields a redun-
dancy, a 1-delay replacement 3 is guaranteed on the removal of
that redundancy.
3 If we have latches where a reset value is guaranteed on the first cycle of
operation, it is sufficient to ensure that the constant v is equal to the reset value;
in this case the replacement is a 0-delay replacement.

Figure

10: A sequential implication graph from assumption
a for the circuit C

Figure

11: An incorrect sequential implication graph from assumption
a for the circuit C
The notion of a label in the implication graph is modified
so that it also contains an integer time offset with respect to
a global symbolic time step t. The rules for learning implications
are exactly the same as before with the addition of a new
rule which allows us to propagate implications across latches:
when we go across a latch we modify the time offset accord-
ingly, e.g. if the output of a latch is labelled with 1 and offset
-2, the input of the latch can be labelled with 1 and offset -3.
An example of an implication graph for the circuit C in Figure
9 is shown in Figure 10.
This example also shows a potential problem with learning
sequential implications. Consider the circuit C in Figure 9.
For the two assumptions ha t 7! 0i (a is 0 at t and t denotes
the global symbolic time) and ha t 7! 1i we get two implication
graphs (in Figures 10 and 11) which both imply (c
This might lead us to believe that the
dundancy. However, the new circuit obtained by replacing c
with 0, if it powers up in state 11 (each latch at 1), remains forever
in 11 with the circuit output x = 1. However, the original
circuit produces no matter which state
it powers up in. Thus we do not have a k-delay replacement
for any k. The reason for this incorrect redundancy identification
is that in order to infer (c from the assumption
needed (c
with 0 (i.e., for all times), c could not have been 1 at t + 1.
One way of solving the above problem is to ensure that no
net is labelled with different labels for different times. We will
label a net with at most one label, and if a net is labelled we
will associate a list of integers with this label which denotes
the time offset when this label is valid. Thus, for the above
example, during the implication propagation phase for the assumption
never infer (a and we will
not get the second implication graph in Figure 10. Labeling
one net with at most one label also obviates the need for the
validation step described in [1].
The algorithm replaces a net n with the constant v if for some
time offset t 0 , it is either labelled with v or is unobservable for
all assumptions. With each such replacement, we associate a
time k as follows [1]. To validate a redundancy n stuck-at-v
at time t 0 , we have a set of implication graphs, one for each
assumption, that imply either n t 0
=\Omega . Let t 00 be
the least time offset on any label in these implication graphs
such that for some net m, m t 00
is labelled with a constant. Then
We say that n is k-cycle
stuck-at-v redundant. We use the following theorem to claim
that the circuit obtained by replacing net n with constant v is a
k-delayed safe replacement.
Lemma 2.3 ([1]) Let a net n be k-cycle stuck-at-v redundant.
Then the circuit obtained by setting net results in a k-
delayed safe replacement of the original circuit.
As in the combinational case, we allow overwriting of constants
with unobservability indicators. We make sure that the
label at net n at time t +a is overwritten only if the new label
is\Omega and net n is not labelled at any other time offset (this is to
prevent the problem shown in Figure 11). This may make our
algorithm dependent on the order of application of rules, but
we have not explored the various options. The proof of the following
two lemmas follows by easy extensions of Lemmas 2.1
and 2.2.
Lemma 2.4 Let A be a consistent assumption. If a label m
a is replaced with m t
=\Omega in the current set of labels, then
for all labels m t
there is an implication graph such that
a is not a label in the graph.
Lemma 2.5 Let A be a consistent assumption. Then the set of
labels returned by the algorithm is compatible.
Hence, the redundancies reported by the algorithm are compatible
with each other and all redundancies can be removed
simultaneously to get a delayed safe replacement.
Theorem 2.2 Let n i k i -cycle stuck-at-v i redundant, for all 1 -
be the set of redundant faults reported by the algorithm.
Then, the circuit obtained by setting net
K-delay safe replacement of the
original.
Proof: From Lemma 2.5, we know from that for all 1
redundant in the circuit obtained by
setting It has been shown in [5] that
for any circuits C, D and E, if C is an a-delay replacement
for D and D is a b-delay replacement for E then C is (a
delay replacement for E. The desired result follows easily by
induction on n from this property of delay replacements.
3 Experimental Results
We present some experimental results for this algorithm. We
demonstrate that our approach of identifying sequential redundancies
yields significant reduction in area and is better than
Circuit Redundancy Removal With Recursive Learning
Name red LR A1 % red LR A2 %
cordic
For legend see Table 2.

Table

1: Experimental results for combinational redundancies
the approach which removes only combinational redundancies.
We also show that for most examples, recursive learning gives
better results then the simple implication propagation scheme.
In fact for many circuits, recursive learning could identify redundancies
where the simple implication propagation scheme
is unable to find any.
This algorithm was implemented in SIS [11]. The circuit
was first optimised using script.rugged which performs
combinational optimisation on the network. The optimised circuit
was mapped with a library consisting of 2-input gates and
inverters. The sequential redundancy removal algorithm was
run on the mapped circuit. The propagation of implications
was allowed to propagate 15 time steps forward and 15 time-steps
backward from the global symbolic time. Table 2 shows
the mapped (to MCNC91 library) area of the circuits obtained
by running script.ruggedand that obtained by starting from
that result and applying redundancy removal algorithm. For
very large circuits (s15850 and larger), BDD operations during
the full simplify step in script.ruggedwere not per-
formed. We report results for those circuits on which our algorithm
was able to find redundancies.
As mentioned earlier, our algorithm starts with an assumption
on the nets and implies values on other nets of the circuit.
We implemented two flavors of selection of assumptions. In
the first case a conflicting assignment was assumed on one net
and values were implied on other nets. The second case was
similar to the first except that once the implications could not
propagate for an assumption on a net, we performed a na-ve
Circuit Attributes Redundancy Removal With Recursive Learning
Name PI PO L A red C LR A1 % time red C LR A2 % time
s953
43 26 183 3775
28 7035 8.4 66.9 92 733 70 6317 17.8 32.1
43 9380 10.0 493.7
s38417* 28 106 1464 33055 591 887 42 31943 3.4 1139.4 1129 9245 97 29718 10.1 1763.7
* full simplify not run.
All times reported on an Alpha 21164 300MHz dual processor with 2G of memory.
PI number of primary inputs PO number of primary outputs L number of latches
A Mapped area after script.rugged A1 Mapped area after redundancy removal A2 Mapped area after redundancy removal with recursive learning
red number of redundancies removed LR Number of latches removed C Upper bound on c, where the new circuit is a c-delay replacement
time CPU time % Percentage area reduction

Table

2: Experimental results for sequential redundancies
version of case splitting only on the net which was closest to
the original net from which the implications were propagated
and implications common in the two cases were also added in
the set of implications learnt for the original net. 4 This enabled
us to propagate implications over a larger set of nets in
the network and hence to discover more redundancies at the
expense of CPU time. Table 2 indicates the area reduction
obtained both by simple propagation and by performing this
recursive learning. We find that even for this na-ve recursive
learning we get reduction in area in most of the circuits over
that obtained without case split. For instance, for S5378 we
were able to obtain 37.5% area reduction with recursive learning
as against 19.6% without it. For most of the medium sized
circuits we were not able to obtain any reduction in area without
recursive learning. For large circuits also we were able to
obtain approximately 5-10% area reduction. S35952 was an
exception where we did not obtain any more reduction in area.
Except for this circuit the CPU time for recursive learning was
less than twice the CPU time for redundancy removal without
it. This suggests that more sophisticated recursive learning
4 If a node is unjustified during forward propagation of implications then
case-split is performed by setting the output net to 0 and 1. If the node is
unjustified during backward propagation case split is achieved by setting one
of the two inputs to the input controlling value (0 for (N)AND gate and 1 for
(N)OR gate) at a time and propagating the implications backward.
based techniques could yield larger area reduction without prohibitive
overhead in terms of CPU time.
Since our algorithm also identified combinational redundan-
cies, we wanted to quantify how many of the redundancies
were purely combinational. To verify this we ran our algorithm
on the circuits for combinational redundancy removal
only.

Table

1 shows the area reduction due to combinational redundancies
only with and without recursive learning. In most
cases, the number of redundancies identified in Table 2 is significantly
larger than the set of combinational redundancies
identified by our algorithm. Only for S35952 and S953 did the
combinational redundancy removal result in approximately the
same area reduction as the sequential redundancy case.
For the example circuits presented here we were able to
achieve 0-37% area reduction. In a number of cases the algorithm
was able to remove a significant number of latches. In
all cases, the new circuit is a C-delay safe replacement of the
original circuit. The C reported in Table 2 is actually an upper
bound. For most of the delay replaced circuits C ! 10000.
However most practical circuits operate at speeds exceeding
100 MHz in present technology. C ! 10000 for a circuit would
require the user to wait for at most 100 -s before useful operation
can begin. This is not a severe restriction.
We are unable to compare sequential redundancy removal
results with the previous work of Entrena and Cheng [8] because
as we noted earlier, their notion of sequential replace-
ment, which is based on the conservative 0,1,X-valued simula-
tion, is not compositional (unlike the notion of delay replacement
that we use).
4 Future Work
Our redundancy removal algorithm does not find the complete
set of redundancies. We can extend this scheme in several
ways to identify larger sets. For instance, instead of analyzing
two assumptions due to a case split on a single net we could
case split on multiple nets and intersect the implications learnt
on this larger set of assumptions. One such method is to incrementally
select those which are at the frontier where the
first phase of implications died out. Additionally, if we split
on multiple nets it is possible to detect pairs of nets such that
if one is replaced with another the circuit functionality does
not change. With our current approach, because we split on
a single net, one of the nets in this pair is always a 1 or a 0,
which means that we are only identifying stuck-at-constant redundancies

For this algorithm we map a given circuit using a library of
two input gates and inverters. A different approach would be
to use the original circuit and propagate the implications forward
and backward by building the BDD's for the node function
in terms of it's immediate fanins. We intend to compare
the running times and area reduction numbers of our approach
with such a BDD based approach. In addition, BDD based
approaches may allow us to do redundancy removal for multi-valued
logic circuits as well in a relatively inexpensive way.
We can extend the notion of redundancy for multi-valued circuits
to identify cases where a net can take only a subset of its
allowed values. Then latches of this kind can be encoded using
fewer bits.

Acknowledgements

We had very useful discussions with Mahesh Iyer and Miron
Abramovici during the course of this work. The comments by
the referees also helped to improved the paper.



--R

"Identifying Sequential Redundancies Without Search,"
"The Transduction Method - Design of Logic Networks Based on Permissible Functions,"
Don't Cares in Multi-Level Network Optimiza- tion
"Recursive Learning: A New Implication Technique for Efficient Solution to CAD Problems - Test, Verification and Optimization,"
"Ex- ploiting Power-up Delay for Sequential Optimization,"
"Latch Redundancy Removal without Global Reset,"
"LOT: Logic Optimization with Testability - New Transformations using Recursive Learning,"
"Sequential Logic Optimization by Redundancy Addition and Removal,"
On Redundancy and Untestability in Sequential Circuits.
"On Removing Redundancies from Synchronous Sequential Circuits with Synchronizing Sequences,"
"SIS: A System for Sequential Circuit Synthesis,"
--TR
The Transduction Method-Design of Logic Networks Based on Permissible Functions
Don''t cares in multi-level network optimization
Exploiting power-up delay for sequential optimization
On Removing Redundancies from Synchronous Sequential Circuits with Synchronizing Sequences
On redundancy and untestability in sequential circuits
sequential redundancies without search
Sequential logic optimization by redundancy addition and removal
Latch Redundancy Removal Without Global Reset

--CTR
Vigyan Singhal , Carl Pixley , Adnan Aziz , Shaz Qadeer , Robert Brayton, Sequential optimization in the absence of global reset, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.8 n.2, p.222-251, April
sequential optimization;recursive learning;sequential circuits;safe delay replacement;compatible unobservability