Latch optimization in circuits generated from high-level descriptions.
In a gate-level description of a finite state machine (\fsm), there is a tradeoff between the number of latches and the size of the logic implementing the next-state and output functions. Typically, an initial implementation is generated via explicit state assignment or translation from a high-level language, and the tradeoff is subsequently only lightly explored. We efficiently explore good latch/logic tradeoffs for large designs generated from high-level specifications. We reduce the number of latches while controlling the logic size. We demonstrate the efficacy of our techniques on some large industrial examples.
Introduction
In a gate-level description of a -nite state machine (fsm), there is a tradeooe between the number of
latches and the size of the logic implementing the next-state logic. This tradeooe can be exploited at
two levels: during generation of the initial implementation, and during subsequent logic optimization
steps.
1.1 Background
State assignment is the generation of a state encoding and an initial latch/logic implementation from
a higher level in the design process. To date, primarily two approaches have been used:
Explicit state assignment begins from an explicit state transition graph and chooses a minimum-
latch encoding while minimizing the size of the combinational logic [DBSV85, VSV90, Har61].
State assignment from high-level languages chooses an encoding according to the delay statements
in the speci-cation, relying on logic synthesis to later optimize the gate-level implementation
[BT93].
Explicit state assignment is impractical for large designs, and despite sophisticated techniques for determining
an optimal assignment, it can produce results far worse than hand-coded implementations.
Furthermore, explicit state assignment programs have not targeted greater-than-minimum-latch imple-
mentations. With current technology (e.g. FPGAs), it is no longer necessary to minimize the number
of latches and doing so often produces prohibitively large combinational logic. One-hot encoding can
also be applied to an explicit state graph, where one latch is used for each state. The resulting logic
will be small and fast since the states do not need to be encoded and decoded. However, the number
of latches is huge, and a one-hot implementation can be a diOEcult starting place for logic synthesis.
Automatic techniques for reducing the number of latches in a one-hot implementation to produce a
good tradeooe have not been resoundingly successful.
State assignment from high-level languages is typically done by a statement-by-statement transla-
tion, which results in a natural insertion of registers at the delay statements in the description. This
is a good starting point for logic synthesis, but results in far more latches than are required to implement
the design [BT93]. Even if the number of latches is not important for the -nal implementation,
too many can drastically reduce the eOEciency of many synthesis and optimization algorithms (e.g.,
symbolic state traversal).
After state assignment, the latch/logic tradeooe can be explored via logic optimization. Standard
techniques, e.g., extracting common factors, function simpli-cation, and retiming, may result in some
latch/logic rearrangement, but largely the state assignment is -xed and optimization only improves
the implementation for the given assignment. The goal of retiming and resynthesis [MSBSV91] was to
jointly optimize latch positions and combinational logic, but the optimization potential was too limited
by the initial state assignment.
RR n\Sigma2943
4 Ellen M. Sentovich, Horia Toma, G#rard Berry
Removal of redundant latches has been done ubiquitously. The term iredundant latchesj itself is
used ubiquitously with a variety of meanings: latches that do not fanout to a primary output, latches
that are constant in the entire state space, latches that are constant in the reachable state space, latches
that are equivalent to other latches, and other more sophisticated de-nitions. We do not consider simple
redundant latch removal here (latches that do not fanout, latches that are constant) as the results are
straightforward. Equivalent state variable identi-cation and removal has been done as part of several
works (e.g., [SSM current BDD and symbolic traversal techniques, this
also is a simple operation. A more robust algorithm for single latch removal was published in [LN91].
It is directly relevant to our single latch removal algorithm described in Section 3.1 and is treated more
thoroughly in that section. It is exact (precisely for replacing a single latch with logic), and far too
expensive when the number of latches exceeds the minimum (log 2 (reachable \Gamma states)) even for small
circuits. In [QCC + 95], a more general technique for re-encoding -nite state machines was given. While
some of the work there is relevant to ours (e.g., controlling the size of the encoding/decoding logic),
the target was quite dioeerent. The goal of that re-encoding was to try to match the encodings of two
dioeerent but similar machines in order to speed up symbolic traversal.
1.2 Our Approach
A complete exploration of the latch/logic tradeooe is certainly not feasible or necessary. Nonetheless, a
suOEciently rich choice of solutions should be available, especially with the variety of implementations
found in today's technology. For example:
ffl one may target an implementation in hardware or software
ffl a hardware implementation may be targeted to a -nal custom design or an FPGA board for
emulation
ffl the current speci-cation may be a preliminary one (not intended for implementation) and used
only for veri-cation of functional properties.
In the above three cases, the optimization criteria are quite dioeerent.
We focus on eOEcient exploration of the latch/logic tradeooe for a design generated from a high-level
speci-cation. In particular, we begin with designs generated from Esterel descriptions. The initial
encoding (generated by the Esterel compiler), while a natural one with respect to the behavior of the
design, contains many redundant registers. We develop algorithms for removing redundant registers.
We target the algorithms to work well on large designs, and to remove registers as cheaply as possible
(i.e., to easily discover redundant registers, to be able to easily replace them with a minimum amount of
additional logic). We generate optimal solutions considering -nal implementation cost and/or eOEcacy
of the intermediate representations.
Our key results include the following:
ffl Our algorithms are eOEcient enough to provide a signi-cant choice of implementations regarding
the latch/logic tradeooe for very large circuits. No other results in this direction have been
published thus far that we are aware of.
ffl By applying simple (easy to compute) heuristics for latch reduction, we get very close to the
minimum number of latches possible on a given reachable state set. In almost all our examples
we obtained a -nal number of latches less than or equal to log 2 jRj is the set of
reachable states.
ffl Because we work incrementally from an initial implementation taken from a high-level language,
and we strive to preserve the given structure, the size of the resulting logic remains tractable
even as we approach the minimum number of latches.
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 5
ffl Our results for maximum latch removal, in terms of area of the resulting logic, compare very
favorably to those obtained by the traditional irobustj technique of extracting the state transition
graph, running an explicit state encoding program, and performing logic optimization on the
result: we usually obtain a smaller implementation in much less time. Furthermore, we observed
a blow-up in the area of the initial implementation after state assignment (resulting in very long
logic optimization run-times) which we do not experience with our incremental techniques. We
could only make this comparison on relatively small examples, as the explicit state transition
graph is expensive to compute.
ffl Run-times for the latch removal algorithms are insigni-cant. The reachable state set is computed
initially, and all subsequent latch redundancies are determined in a comparatively trivial amount
of time from this set.
2 Overview of the Technique
We apply heuristic techniques to successively remove redundant latches while controlling the size of
the combinational logic. A complete latch removal technique could be implemented by extracting an
explicit state transition graph, performing exact state minimization, and running a state assignment
program to generate a minimum-latch encoding. This is far too expensive and yields no insight to
the latch/logic tradeooe. We instead successively remove latches using a subset of the information that
is used in the aforementioned complete scheme. (For example, we consider reachable states, but not
equivalent states.) In this realm, a general heuristic procedure might be:
1. Compute the BDDs for the latches, the outputs, and some auxiliary functions (e.g., equivalent
states, reachable states, controllability/observability information from the environment).
2. Apply algorithms for removing latches such that the sequential behavior is unchanged with
respect to the environment described by the auxiliary functions.
3. Iterate, removing as many latches as possible, or as many latches as desired given constraints on
the size of the combinational logic.
2.1 The General Algorithm
As we -nd this scheme still too expensive for industrial applications, and more robust than necessary
as we demonstrate experimentally, we choose the simpler scheme:
1. Compute the reachable states of the machine.
2. Determine a set of latches which may be easily removed while preserving the reachable state set.
3. Among these, choose a set of latches to remove based on a cost estimate; remove latches, add
logic, and optimize.
4. Iterate, removing as many latches as possible, or as many latches as desired given constraints on
the size of the combinational logic.
It is important to note that at each one-latch-removal step, for each of our proposed algorithms, we re-encode
states by considering state pairs which can be easily merged. This is not a general re-encoding:
we pair each reachable state with an unreachable state, and give each pair a single new encoding. The
pair/merge operation is done in such a way that
ffl it is computationally easy to determine the pairings
RR n\Sigma2943
6 Ellen M. Sentovich, Horia Toma, G#rard Berry
In In Out
M'
Out

Figure

1: General Circuit Transformation
ffl it is inexpensive in BDD size and logic size to perform the mergings and update the reachable
states
ffl the existing logic is preserved as much as possible as it contains valuable information on the
structure of the circuit.
In this way, the computations required remain tractable for our very large circuits, and the resulting
additional combinational logic (which is usually the most limiting factor in incremental re-encoding
algorithms) is controllable.
It is very important to note that the transformation is proven to preserve behavior on the reachable
state set and remains correct for every over-approximation of the reachable state set. Therefore it could
be used in conjunction with eOEcient techniques for approximate reachability analysis [CHM
2.2 Circuit Transformation
The transformation is illustrated in Figure 1. The original FSM is M and the transformed one is
M 0 . We call ng the set of latches of M . A transformation will remove latches
with indices in a set I. For convenience, we keep the same indices for the remaining latches in
Ig, and we assume that L 0 has m latches. The next state vector for L in M
is generated by C and called Y . In M 0 , the encoding function E has type and it is given by
a vector of functions I. The decoding function D has type
and is given by a vector
be the set of reachable states in M (resp M 0 ), and
denote the characteristic function of R (resp. R 0 ). Thus r 2 R implies
Let r 0 and r 0
0 denote the initial states of M and M 0 .
In this context we say that M is equivalent to M 0 if r
This is the property our transformations will satisfy.
Functions will be represented by polynomials or BDDs. The input variables will be consistently
called
k for D, l k for R, and l 0
k for R 0 . If F denotes a polynomial or BDD over a set of
variables X and if Y is another set of variables where we denote by F [Y=X] the result
of the substitution of the x k by the y k , and F [Y =X] the result of the substitution of the x k by the
complements y k . We respectively denote by F x and F -
x the positive and negative cofactor of F with
respect to x.
Algorithms
In this section, several algorithms for latch removal are described. In summary:
1. single-latch removal: determine which latches can be removed individually and replaced by a
combinational function of the other latches.
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 7
2. determine pairs of latches that can be removed and replaced by a single latch whose
input is a combinational function of the other latches.
3. one-hot-3-by-2: search for a one-hot encoding and replace every three latches by two latches
and a combinational function.
4. replacement of n latches by latches with a new combinational function for
each latch.
In the following sections, each is speci-ed precisely according to
ffl the condition under which latches are removed
ffl the logical transformation required in the circuit, i.e. the speci-cation of D and E in Figure 1
[Note: There are many choices in the functions to implement. We have chosen and described one
for each algorithm. The reasons for each choice and its subsequent eoeects on optimization are
further described in Section 4.]
ffl a proof that the transformation is valid [Note: The new initial state is trivially computed from
the encoding function E and hence not discussed further.]
ffl a brief description of the algorithm [Note: In every case, R is incrementally and eOEciently updated
for further computations and iterations.]
3.1 Transformation single-latch
Single latch removal -nd and replaces latches that can be substituted by a combinational function of
the other latches.
Condition: A single latch l i can be replaced by a combinational function of the others if
R l i
This condition was originally given in [BCM90]. Its satisfaction implies that l i does not distinguish
any reachable states; the re-encoding will couple each reachable state of the form l 1 l
with the unreachable state l 1 l to produce the state l 0
n and similarly
for 1=0.
In general, a subset of the latches will each satisfy this condition. Once a single latch is removed,
the remaining subset of removable latches may change. We apply heuristic techniques, as described in
the algorithms below, to determine which latches to remove.
In [LN91], an exact branch-and-bound algorithm is used to determine the maximum number of
single latches that can be removed. While the paper indicates that the bounding heuristics are powerful
and the exact result is obtained in a reasonable amount of time, the experiments were only performed
on small examples: the largest reduction in number of latches is 5 and the largest total number of
latches is 21. Our designs have 10's and 100's of latches, with many redundant latches. The exact
algorithm is far too expensive, and we have empirically observed results that nearly match it with
the single-latch algorithms. Furthermore, we reduce the number of latches even further with the
algorithms described in the sequel.
Transformation: The latch l i is removed and the logic for functions D and E are added, where E
is de-ned by E k (Y For D, we set D k (L 0
RR n\Sigma2943
8 Ellen M. Sentovich, Horia Toma, G#rard Berry
single-latch-1(M, R)
removed-list
/* Find and remove latches. */
while (1) -
best-latch-cost
foreach latch l i -
if (C l i
best-latch-cost
if (best-latch-cost j 1) break;
removed-list removed-list
if (removed-list j OE) return;
/* Compute D and modify M. */
foreach l i 2 removed-list -
foreach l
remove-latch(M, l
R-new / 9 l i
R / R-new;

Figure

2: Transformation
Let l
, and
this implies R l i
Two algorithms were implemented for single latch removal; the pseudo-code is given in Figures 2
and 3.
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 9
single-latch-2(M, R, bound)
while (1) -
removable-list
removed-list
foreach latch l i -
/* By transformation (2) */
removable-list removable-list [ (l
if (removable-list j OE) return;
foreach latch l i 2 removable-list -
if (still-can-be-removed(removed-list, l i
remove-latch(M, l
removed-list removed-list

Figure

3: Transformation
Algorithm 1: greedily selects and removes one latch at a time based on a cost function related to
the potential for removing other latches. We use the branching heuristic of [LN91], so compute-cost
sets C l i
j), where jRj is the onset size of the BDD R. The absolute value term is
highest for those latches with the most potential for distinguishing states. By selecting the latch with
the lowest C l i
, we leave the latches with the highest potential, and thus heuristically maximize the
chances of removing more latches. Furthermore, this heuristic implies a minimum number of minterms
that are changed in the encoding space, which we observe to help control the size of the overall logic.
After selecting the latch, R is updated as though the latch had already been removed, and the process
is iterated. After a set of latches that can be removed simultaneously have been computed, they
are removed and replaced by combinational logic that depends only on the remaining latches. This
algorithm computes a maximal removable set, and hence iteration is not necessary.
Note that upon removing the latch, the output variable implementing the input of the latch is set
to 0, which results in simpli-cation of the combinational logic C. In addition, each D i is computed
directly from the initial R by smoothing all the other variables that will be removed: if l 1
are simultaneously removable, D
thermore, the operations can be performed in any order since 9 is commutative and 9 and cofactor
commute. Alternately, R could be updated as each variable is removed, and the next D i computed
from the updated R. This latter technique requires less computation at each removal, but creates
functions that depend upon variables that will be eventually removed and hence increases the levels
of logic. As we strive to control size and depth of the logic and as computation time is not signi-cant,
we prefer the former method.
Algorithm 2: selects a set of latches according to a cost bound that is based on the BDD size.
compute-cost returns the number of support variables in the BDD for D i , and as such is an estimate
of both BDD size (for manipulation) and -nal implementation size (resulting logic for D). Of course,
the number of BDD support variables is not at all a tight measure of implementation size; nonetheless,
RR n\Sigma2943
Ellen M. Sentovich, Horia Toma, G#rard Berry
foreach latch l i -
foreach latch l j , j
if is-removable(R l i l j
transformations (4) (5) */
remove-latch(M, l i );
(R l i

Figure

4: Transformation 2-by-1: Algorithm
there is a correlation and at this level it is very diOEcult to estimate implementation size without further
synthesizing the design. Since a set of latches is selected according to their individual removable
condition in R, there is no guarantee that they can be removed simultaneously. This condition is
checked during latch removal in the second part of the algorithm. D i must be recomputed as well to
ensure that it depends only on remaining latches. The entire process is iterated with an increasing
cost bound.
3.2 Transformation 2-by-1
Condition: Two latches l i and l j can be replaced by a single latch l 0
The satisfaction of this condition implies that there is again a valid pairing of reachable states and
unreachable states. The re-encoding will couple each reachable state l 1 l
with the unreachable state l 1 l to produce l 0
n .
That is, l i l or 11 is replaced by l is replaced by l
Transformation: If l i and l j satisfy the above condition, one can remove l i and set
ae
(4)!
Proof: Let l 2 R. If k 6= i and k 6= j, then D k
Let l l. Then since
and
1. With the -rst term of condition (3), this implies R l i l j
l j . Similarly for l i l j 2 f01; 10; 11g. Thus, l for each reachable state l. 2
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 11
Algorithm: The pseudo-code for the algorithm is shown in Figure 4. Each latch pair is examined
and replaced by a single latch if possible. Note that in this case, the input y i of the removed latch l i
cannot be set to 0 because E j depends on it. Therefore, there is no subsequent logic reduction in C.
3.3 Transformation one-hot-3-by-2
This transformation is very speci-c to one-hot encoded designs. Note that if the single latch removal
algorithm is applied to a one-hot-encoded design, only one latch can be removed (even if the exact
algorithm is applied) even though the design has jLj latches and the minimum is log 2 jLj. This algorithm
-rst searches for part of the encoding space that is one-hot encoded. It then replaces every three latches
by two in this part of the encoding.
Condition: The condition for a latch y i to be one-hot-encoded is given by
R l i
Y
Transformation: Each group of three latches l i , l i+1 , l i+2 can be replaced as
\Deltal 0
l
Proof and Algorithm: We omit the proof for brevity, and we do not describe this algorithm in
detail as it is a specialized heuristic, and straight-forward to implement.
3.4 Transformation n-by-(n-1)
The n-by-(n-1) algorithm considers the entire encoding space when searching for a state-pair merging,
rather than restricting to merging across a plane or a small cube (as the case for single and 2-by-1).
The algorithm has two parts. First, the encoding is modi-ed (without removing latches) by clustering
the existing encodings toward the all-0 encoding. This is called migrate-states. Next, the resulting
encoding is checked to see if each reachable state can be paired with its mirror state (all variables
complemented).
3.4.1 Transformation migrate-states
Condition: The condition that some encodings can be shifted toward the origin is given by
No registers are removed at this step. The reachable states in l i \DeltaR l i
are re-encoded as - l i \DeltaR l i
6' R, this transformation safely maps a state in the reachable set to an unused encoding
(in the unreachable set).
Transformation: Given l i that satis-es (6), the machine is re-encoded as follows:
(R l i
RR n\Sigma2943
12 Ellen M. Sentovich, Horia Toma, G#rard Berry
Let l
, and
1. The Shannon cofactor and
(l). Finally, D i
(l) +R- l i
Algorithm: greedily moves the encodings towards the origin in the Boolean space. The algorithm is
implemented simply by iterating over the latches, checking the condition and performing the transformations
if possible. The motivation is that the subsequent fold-states operation can be performed
if all the reachable states are Hamming distance d ne \Gamma 1 of the origin 1 . We could choose any point in
the Boolean space around which to cluster the encodings, but the all-0 encoding is a good choice for
Esterel circuits (and, we believe, for others generated from high-level descriptions). The reason is that,
while the initial encodings are not one-hot, they are close to one-hot, and igroup-hotj; as such they
contain many 0's. migrate-states can add an exorbitant amount of logic, so rather than iterating to
completion, we check the fold-states condition at each iteration and stop when it is satis-ed. The
reachable states are updated after each latch is visited as follows:
3.4.2 Transformation fold-states
The re-encoding is done by choosing a latch l i , and for each state encoding l, if l l the encoding
is unchanged, while if l the other state variables are inverted. The latch l i is then removed. For
example, the condition is satis-ed. Choosing the -rst bit for the removed
latch l i , the new encoding is R
Condition: The condition under which the states can be merged is given by
Transformation: The transformation removes register l i and sets
ae
Proof: Let l 2 R. Let l l. The Shannon expansion of R(l) and the fact that
since condition
L=L]), so R l i
Finally, because l
for each j 6= i.
Similarly for l
Algorithm: is implemented directly from (10) and (11). The reachable states are updated as follows:
1 This is a suOEcient but not necessary condition.
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 13
3.5 Comments on the Algorithms
It must be emphasized that in selecting algorithms and heuristics, we do not focus primarily on
traditional logic optimization metrics. Our goals while exploring the latch/logic tradeooe are instead to
ffl maintain the initial existing logic structure to the extent possible, as it reAEects the structure
given by the high-level description,
ffl use metrics that relate to the perform of our algorithms and to the size of the D, E logic which
we have the most control over: we try not to overly pessimize logic synthesis,
ffl leave the logic optimization to existing tools that are specialized for this purpose.
Heuristics
The most important heuristic that we have not described is related to don't care conditions for
selecting D and E. In each case, there is actually a set of combinational functions that can be used,
not just a single one. The set arises from the use of the unreachable states as don't care conditions;
we have not indicated this choice in our description of the D and E functions. For example, in the
single-latch algorithm, any function that satis-es R l i
would be correct. We
experimented with dioeerent choices, and found that the functions were small enough that this degree
of AEexibility was not useful at this level. Furthermore, since it arises solely from the reachable state
set, the same information can be used instead in subsequent logic optimization.
There are many other heuristics that can be employed for selecting a latch, for minimizing the
BDDs, for minimizing the implementation, for optimizing algorithm performance, etc. We focus on
-nding good implementations and exploring a reasonable subset of the latch/logic tradeooe given the
available tools (state-of-the-art BDD technology, logic optimization, etc.) for the designs in our domain,
rather than attempting to implement any exact algorithms or thoroughly test a large set of heuristics
whose -nal value is diOEcult to measure. We tested a number of heuristics (especially for selecting D
and E) and our choices in function implementation reAEect the results of these experiments.
Other similar algorithms
Note that the 2-by-1 is a generalization of the single latch removal algorithm, which can be further
generalized to replace 3 registers by 2, etc. We found that such a successive generalization did
not improve the results suOEciently to justify its rapidly increasing cost. (Note that the n-by-(n-1)
algorithm described above is not a generalization of 2-by-1).
Completeness
The single-latch algorithms are complete in that when they are -nished, no single latches can be
removed while maintaining the same reachable state set on L. No claims are made about removing
several latches by this criteria. Transformation 2-by-1 is not complete in that it may be possible for
two latches to be replaced by one latch with additional combinational logic and not replaced by this
algorithm. Similarly, the n-by-(n-1) algorithm is not complete.
4 Implementation and Results
Experiments have shown that -nding a good latch encoding before performing optimization is a very
diOEcult problem, yet an important one as the encoding strongly eoeects subsequent optimization. We
know that a log 2 jRj encoding usually implies exorbitant combinational logic, but given a particular
encoding we cannot predict what the size of the combinational logic will be. The same intuition applies
to the tradeooe between the number of latches and the performance of veri-cation algorithms.
RR n\Sigma2943
14 Ellen M. Sentovich, Horia Toma, G#rard Berry
The aim of our implementation was to develop a tool which allows us to make estimates over the
starting points of combinational optimization for hardware and software designs and for veri-cation.
These two dioeerent metrics imply the need for dioeerent strategies combining latch removal and logic
optimization.
4.1 Implementation
We implemented our program rem-latch using the TiGeR library [CMT93] (which contains a BDD
package and the reachable states computation) to implement the latch removal algorithms, and the
Berkeley SIS environment [SSL + 92] to perform combinational logic optimization. We used mainly two
scripts for logic optimization in SIS: a fast but less robust one (COMBOPT), and a more expensive one
which includes, e.g., full-simplify (BLIFOPT). Where actual logic cost is estimated, literal count in SIS
is computed; the cost of a register in terms of literals varies depending on the target implementation.
We have found this to be a reasonable measure for both the hardware and software that we produce.
Implementation Optimization
The -rst strategy is oriented to hardware and software implementations. The basis of latch removal
in this case is single-latch-2, where the cost function bounds the size of the support of the BDDs
for the logic replacing the latches (D). The transition from BDDs to logic can be costly, and we found
that BDD support size was the best measure for controlling this blow-up (as opposed to a guess based
on literal count). Recall that the single-latch algorithms actually reduce the size of C, so the overall
logic cost (using the post-synthesis measure of literal count) varies very little (see Section 4.2).
During the experiments we observed that very attractive con-gurations can be discovered even for
circuits where large intermediate BDDs are generated. In these cases, subsequent logic optimization
successfully reduced the implementation sizes. For this reason, we iterate single-latch-2 while relaxing
the cost conditions, and then continue with 2-by-1. While the fold-states algorithm is no
more expensive in terms of additional logic than 2-by-1, the necessity of performing migrate-to-0,
which does add signi-cant logic, prohibits the use of n-by-(n-1) for hardware and software implementations

4.1.2 Strategy 2: Veri-cation Optimization
The second strategy is oriented to improving the time taken by veri-cation-based algorithms. Experiments
demonstrate that reducing the number of latches has a positive eoeect on the performance of
veri-cation techniques: the BDDs for the reachable states decrease in size and the size of the combinational
logic grows slowly. The reason for this is primarily that the number of latches has a strong
eoeect on the BDD sizes (there are two BDD variables per latch for FSM veri-cation). Thus strategy
uses single-latch-1 with its heuristics for maximizing the number of removed latches, followed
by iteration of 2-by-1 to completion. This latter is applied alternatively with logic optimization to
ensure that the successive -nite state machines have reasonable sizes. The results of this phase are
very encouraging, mainly because we can suOEciently control the additional logic using the BLIFOPT
script. For the largest circuits, of course this was not possible. We had to use the COMBOPT script,
the logic grew more quickly and consequently we were restricted in the number of latches that were
removed. Nonetheless, we were able to reduce latches and improve veri-cation times where we were
not able to perform any optimization previously. We explore the topic of handling very large circuits
in Section 5.
4.1.3 Strategy 3: Exploration
The goal of the third strategy was to minimize the number of latches to study the behavior of the
algorithms and properties of the -nal circuits. Interestingly, we were able in almost all cases to reduce
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 15
Circuit #states #reg exact single-1 minimum
s400 8865 21
s526 8868 21 19 19 14

Table

1: single-latch-1 vs exact single removal
the number of latches to log 2 (jRj) + 1, which gives an indication of the power of our algorithms. In
addition, we found that some large examples remain reasonably-sized even when the number of latches
decreases dramatically. We report more extensively on maximum latch removal compared to other
strategies in Section 4.2.
4.1.4 Controlling the Logic Size
We already tailor our algorithms to -nd state pairs that are easy to merge and re-encode, and thereby
minimally modify the reached state set. Once the functions are determined, it is necessary to compute
the implementing logic. We start with a BDD for the new logic and must transform it to a logic-gate
representation. There are two places where we control the size of the introduced logic. The -rst is in
keeping the BDD sizes small, a goal used by all of our algorithms. The TiGeR BDD package creates
logic from BDDs that is linear in the number of BDD nodes. The second is to use the formulas for
the D and E logic and directly implement some functions as logic gates, computing other functions as
BDDs and substituting the BDD results into the created logic gates. This technique can increase the
number of levels of the circuit, so it must be used with caution.
4.2 Results
The -rst set test is the ISCAS-89 sequential test benchmarks, which we used for comparison with the
exact single latch algorithm in [LN91]. The results are shown in Table 1. Only for s444 are the
results of the exact algorithm better. A run-time comparison would not be fair as we do not have the
implementation of the exact algorithm by the author. Our algorithm ran in a few seconds for all the
ISCAS benchmarks, which compares favorably to the results in [LN91]. Our implementation of the
exact algorithm ran more than an hour for all but the smallest of the Esterel examples.
The other benchmarks we used are all synthesized by the Esterel v5 compiler. Some of them
are simply test programs, but others are large industrial designs. tcint, renault, snecma, sequenceur,
and trappes are particularly large and interesting examples. We have two possible starting points. The
designs generated directly from the Esterel compiler have a manageable initial implementation in terms
of encoding and logic, but far too many redundant registers. The other case arises from examples that
initially have combinational cycles. If the design is causal, the causality analysis program [SBT96]
generates an initial acyclic implementation directly from the BDDs and is thus huge in terms of logic
(e.g., trappes).
In

Table

2, the initial circuit is compared with the minimum-latch rem-latch result optimized with
COMBOPT. We obtained close to the minimum number of latches on most examples. Where the logic
increases it remains reasonable, and in many cases it decreases due to the removal of many simply
redundant latches and gates. In fact, for sequenceur, tcintnocount, and trappes, we have not reported
the minimum number of latches as the logic increase was exorbitant (e.g., for tcintnocount we obtained
a 9-latch version with 11826 literals and for sequenceur a 59-latch version with some 600,000 literals).
CPU times are reported in Table 3. The experiments were run on a DEC Alpha 200/233 station,
RR n\Sigma2943
Ellen M. Sentovich, Horia Toma, G#rard Berry
initial rem-latch
Circuit #in #out states min #reg #lit #reg #lit
abc 4 12
renault
runner 6 5 5182 13
sequenceur
tcintnocount 19 20 310 9 90 1036 26 328
trappes 53 154 135718

Table

2: Initial version vs Minimum-latch version
Circuit reachable-states single 2-by-1 merge fold
abc 0.3 0.7 0.9 1.1 1.3
abcdef 1.2 3.3 3.5 3.7 3.9
controle 0.9 1.4 1.6 1.8 2.0
controlecount 4.5 5.8 6.4 6.8 7.1
renault 6.5 12.2 14.6 15.6 16.9
runner 54.6 62.0 68.3 75.5 76.1
sequenceur 1270.6 2678.9 3402.7 3630.7 -
snecma 45.3 67.2 69.7 70.5 71.2
tcint 133.6 238.1 250.0 250.5 252.8
tcintnocount 19.6 76.1 81.9 82.9 84.1
trappes 245.9 406.4 571.1 733.5 896.1

Table

3: CPU seconds on a DEC Alpha
rem-latch NOVA/SIS
Circuit reg literals reg literals states
abc 4 111 4 197
controle 5 626 5 172 23
controlecount
tcintnocount 26 313 8 7692 231
traOEc 5

Table

4: rem-latch minimum-latch vs NOVA/SIS
and the times are in CPU seconds. In this table, we show a series of cumulatives times for running the
algorithms in succession. We begin with the reachable states computation, and progressively add the
times for each algorithm. The run-times remain on the same order of magnitude as the initial reachable
states computation. Note that for tcint, the merge-states condition is satis-ed immediately, so it runs
very quickly.
In

Table

4 we report our minimum-latch+BLIFOPT results versus those obtained from a combination
of state-graph extraction, exact state minimization, state assignment with NOVA, and logic
optimization in SIS with both the SIS rugged script and BLIFOPT. With the tcint example, we
actually had to run some latch removal and optimization to obtain an implementation from which
we could extract the state transition graph. Still, with the exception of the controle circuits, the
NOVA/SIS combination performed much worse. In the case of abcdef, the initial NOVA circuit was
too large to run any optimization. Even though these circuits were generated from Esterel, in only
one case were equivalent states found, and this did not aoeect the minimum number of latches. This
gives some indication that we are not losing much by not explicitly considering equivalent states in our
strategy.
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 17
BLIFOPT best-remlatch
Circuit #in #out #reg #lit #reg #lit
renault 23 166 37 507 28 497
runner 6 5 29 198 15 198
tcint 19 20 50 241 38 237
tcintnocount 19 20 47 197 38 194
sequenceur
trappes 53 154 - 20 1193

Table

5: BLIFOPT vs best-remlatch2503504508
'single.dat'
'sis_single.dat'

Figure

5: Graph 1: Latches vs literals
In

Table

5, we compare the best logic optimization results obtained from applying BLIFOPT
to the initial circuit to the best rem-latch results obtained with a combination of latch removal
and optimization. For all small examples, we were able to reduce the number of latches to the
minimum so thorough exploration was possible. Here, we tried many combinations of latch removal and
optimization, and the algorithms and strategies discussed in Sections 3 and 4.1 reAEect this experience.
On larger -les we couldn't obtain the minimum (due to the size of the encoding logic and not theoretical
limits of the algorithms). Instead, we used strategies similar to those that were successful on small
examples. The number of literals is comparable, despite the fact that rem-latch must add encoding
and decoding logic. Furthermore, the number of latches is much lower. For sequenceur and trappes, no
signi-cant logic optimization can be done without -rst removing latches, so we present novel results
on these examples.
The graph in Figure 5 shows the evolution of the latch-literal tradeooe for one example during the
application of the standard strategies (all of our examples behaved similarly). We observe -rst that the
number of literals remains almost constant during single latch removal. Recall that here C is actually
RR n\Sigma2943
Ellen M. Sentovich, Horia Toma, G#rard Berry579111315

Figure

Graph 2: Veri-cation times vs number of latches
reduced. This is not the case for 2-by-1 algorithm, so the logic tends to increase quickly. Still, we
were successful in reducing this logic and continuing with 2-by-1 except for sequenceur. The logic
size must always be carefully monitored. A similar phenomenon is observed with the application of
migrate and fold.
The graph in Figure 6 shows the evolution of the CPU time for self-veri-cation of one of our
examples as the number of latches decreases. The best point, at 15 latches, was obtained after single
and 2-by-1, but without iterating 2-by-1 to completion. All examples behaved similarly.
5 Future Work
The -rst goal is to use the results of this work as a pre-processor to improve logic optimization. This
is a critical point since the circuits produced by causal analysis are very large and diOEcult to cope
with. Our experimental work indicates that partitioning (beyond D and E) will improve results at
this stage.
The next step is to exploit particular properties of Esterel programs (including Esterel relations, a
form of don't care conditions, and circuit structures particular to Esterel-generated implementations).
Cost functions based on the structural analysis could not only improve the veri-cation times, but
also allow good tradeooes in logic optimization. It is important with large designs to exploit the given
natural circuit structure.
For hardware implementations using FPGAs, we will explore increasing the number of latches
via retiming to improve the critical path. In fact, retiming-based techniques could be used in both
directions at this stage, i.e., to reduce the number of latches and to reduce the critical path by increasing
new latches.

Acknowledgements

This work was supported in part by the National Science Foundation under grant INT-9505943, and
the French GENIE MESR INRIA project.
INRIA
Latch Optimization in Circuits Generated from High-level Descriptions 19



--R

New Ideas on Symbolic Manipulations of Finite State Machines.
Optimized Controller Synthesis Using Esterel.
A Structural Approach to State Space Decomposition for Approximate Reachability Analysis.

Optimal State Assignment for Finite State Machines.
On the State Assignment Problem for Sequential Machines.
Exact Redundant State Registers Removal Based on Binary Decision Diagrams.
Retiming and Resyn- thesis: Optimizing Sequential Networks with Combinational Techniques
Incremental FSM Re-Encoding for Simplifying Veri-cation by Symbolic Traversal
Constructive Analysis of Cyclic Circuits.
SIS: A System for Sequential Circuit Synthesis.
Sequential Circuit Design Using Synthesis and Optimization.
Detection of Equivalent State Variables in Finite State Machine Veri-cation
NOVA: State Assignment of Finite State Machines for Optimal Two-Level Logic Implementations
--TR
Sequential Circuit Design Using Synthesis and Optimization
A Structural Approach to State Space Decomposition for Approximate Reachability Analysis
Constructive Analysis of Cyclic Circuits

--CTR
Ellen M. Sentovich , Horia Toma , Gard Berry, Efficient latch optimization using exclusive sets, Proceedings of the 34th annual conference on Design automation, p.8-11, June 09-13, 1997, Anaheim, California, United States
Andrew Seawright , Wolfgang Meyer, Partitioning and optimizing controllers synthesized from hierarchical high-level descriptions, Proceedings of the 35th annual conference on Design automation, p.770-775, June 15-19, 1998, San Francisco, California, United States
Yunjian Jiang , Robert K. Brayton, Software synthesis from synchronous specifications using logic simulation techniques, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Priyank Kalla , Maciej J. Ciesielski, Performance driven resynthesis by exploiting retiming-induced state register equivalence, Proceedings of the conference on Design, automation and test in Europe, p.125-es, January 1999, Munich, Germany
Hahnsang Kim , Thierry Turletti , Amar Bouali, EPspectra: a formal toolkit for developing DSP software applications, Theory and Practice of Logic Programming, v.6 n.4, p.451-481, July 2006
Stefano Quer , Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Ellen M. Sentovich , Robert K. Brayton, Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks, Formal Methods in System Design, v.17 n.2, p.107-134, Oct. 2000
Klaus Winkelmann, Formal Methods in Designing Embedded Systemsthe SACRES Experience, Formal Methods in System Design, v.19 n.1, p.81-110, July 2001
state assignment;high-level synthesis;sequential optimisation