1 .\" $Id: nanotrav.1,v 1.23 2009/02/21 06:00:31 fabio Exp fabio $
3 .TH NANOTRAV 1 "18 June 2002" "Release 0.11"
5 nanotrav \- a simple state graph traversal program
11 nanotrav builds the BDDs of a circuit and applies various reordering
12 methods to the BDDs. It then traverses the state transition graph of
13 the circuit if the circuit is sequential, and if the user so requires.
14 nanotrav is based on the CUDD package. The ordering of the variables
15 is affected by three sets of options: the options that specify the
16 initial order (-order -ordering); the options that specify the
17 reordering while the BDDs are being built (-autodyn -automethod); and
18 the options to specify the final reordering (-reordering
19 -genetic). Notice that both -autodyn and -automethod must be specified
20 to get dynamic reordering. The first enables reordering, while the
21 second says what method to use.
25 read input in blif format from \fIfile\fR.
28 read options from \fIfile\fR.
31 traverse the state transition graph after building the BDDs. This
32 option has effect only if the circuit is sequential. The initial
33 states for traversal are taken from the blif file.
36 perform dependent variable analysis after traversal.
38 .B \-from \fImethod\fB
39 use \fImethod\fR to choose the frontier states for image computation
40 during traversal. Allowed methods are: \fInew\fR (default), \fIreached\fR,
41 \fIrestrict\fR, \fIcompact\fR, \fIsqueeze\fR, \fIsubset\fR, \fIsuperset\fR.
43 .B \-groupnsps \fImethod\fB
44 use \fImethod\fR to group the corresponding current and next state
45 variables. Allowed methods are: \fInone\fR (default), \fIdefault\fR,
48 .B \-image \fImethod\fB
49 use \fImethod\fR for image computation during traversal. Allowed
50 methods are: \fImono\fR (default), \fIpart\fR, \fIdepend\fR, and
54 use \fIn\fR to derive the clipping depth for image
55 computation. It should be a number between 0 and 1. The default value
58 .B \-verify \fIfile\fB
59 perform combinational verification checking for equivalence to
60 the network in \fIfile\fR. The two networks being compared must use
61 the same names for inputs, outputs, and present and next state
62 variables. The method used for verification is extremely
63 simplistic. BDDs are built for all outputs of both networks, and are
67 perform reachability analysis using the transitive closure of the
71 use \fIn\fR to derive the clipping depth for transitive closure
72 computation. It should be a number between 0 and 1. The default value
76 compute the greatest fixed point of the state transition
77 relation. (This greatest fixed point is also called the outer envelope
81 compute the strongly connected components of the state transition
82 graph. The algorithm enumerates the SCCs; therefore it stops after a
83 small number of them has been computed.
86 compute the maximum flow in the network defined by the state graph.
89 read the sink for maximum flow computation from \fIfile\fR. The source
90 is given by the initial states.
92 .B \-shortpaths \fImethod\fB
93 compute the distances between states. Allowed methods are: \fInone\fR
94 (default), \fIbellman\fR, \fIfloyd\fR, and \fIsquare\fR.
97 use selective tracing variant of the \fIsquare\fR method for shortest
101 compute the conjunctive decomposition of the transition relation. The
102 network must be sequential for the test to take place.
105 compute signatures. For each output of the circuit, all inputs are
106 assigned a signature. The signature is the fraction of minterms in the
107 ON\-set of the positive cofactor of the output with respect to the
108 input. Signatures are useful in identifying the equivalence of circuits
109 with unknown input or output correspondence.
112 perform a simple test of ZDD functions. This test is not executed if
113 -delta is also specified, because it uses the BDDs of the primary
114 outputs of the circuit. These are converted to ZDDs and the ZDDs are
115 then converted back to BDDs and checked against the original ones. A
116 few more functions are exercised and reordering is applied if it is
117 enabled. Then irredundant sums of products are produced for the
121 print irredundant sums of products for the primary outputs. This
122 option implies \fB\-zdd\fR.
124 .B \-second \fIfile\fB
125 read a second network from \fIfile\fR. Currently, if this option is
126 specified, a test of BDD minimization algorithms is performed using
127 the largest output of the second network as constraint. Inputs of the
128 two networks with the same names are merged.
131 test BDD approximation functions.
133 .B \-approx \fImethod\fB
134 if \fImethod\fR is \fIunder\fR (default) perform underapproximation
135 when BDDs are approximated. If \fImethod\fR is \fIover\fR perform
136 overapproximation when BDDs are approximated.
138 .B \-threshold \fIn\fB
139 Use \fIn\fR as threshold when approximating BDDs.
142 Use \fIn\fR (a floating point number) as quality factor when
143 approximating BDDs. Default value is 1.
146 test BDD decomposition functions.
149 test cofactor estimation functions.
151 .B \-clip \fIn file\fB
152 test clipping functions using \fIn\fR to determine the clipping depth
153 and taking one operand from the network in \fIfile\fR.
155 .B \-dctest \fIfile\fB
156 test functions for equality and containment under don't care
157 conditions taking the don't care conditions from \fIfile\fR.
160 test function that finds a cube in a BDD at minimum Hamming distance
164 test function that extracts two-literal clauses from a DD.
167 perform a simple test of the conversion from characteristic function
168 to functional vector. If the network is sequential, the test is
169 applied to the monolithic transition relation; otherwise to the primary
173 build local BDDs for each gate of the circuit. This option is not in
174 effect if traversal, outer envelope computation, or maximum flow
175 computation are requested. The local BDD of a gate is in terms of its
179 set the initial size of the computed table to \fIn\fR.
182 set the initial size of each unique subtable to \fIn\fR.
185 set the target maximum memory occupation to \fIn\fR MB. If this
186 parameter is not specified or if \fIn\fR is 0, then a suitable value
187 is computed automatically.
190 set the hard limit to memory occupation to \fIn\fR MB. If this
191 parameter is not specified or if \fIn\fR is 0, no hard limit is
192 enforced by the program.
195 set the hard limit to the number of live BDD nodes to \fIn\fR. If
196 this parameter is not specified, the limit is four billion nodes.
198 .B \-dumpfile \fIfile\fB
199 dump BDDs to \fIfile\fR. The BDDs are dumped just before program
200 termination. (Hence, after reordering, if reordering is specified.)
203 use blif format for dump of BDDs (default is dot format). If blif is
204 used, the BDDs are dumped as a network of multiplexers. The dot format
205 is suitable for input to the dot program, which produces a
209 use blif-MV format for dump of BDDs. The BDDs are dumped as a network
213 use daVinci format for dump of BDDs.
216 use DDcal format for dump of BDDs. This option may produce an invalid
217 output if the variable and output names of the BDDs being dumped do
218 not comply with the restrictions imposed by the DDcal format.
221 use factored form format for dump of BDDs. This option must be used
222 with caution because the size of the output is proportional to the
223 number of paths in the BDD.
225 .B \-storefile \fIfile\fB
226 Save the BDD of the reachable states to \fIfile\fR. The BDD is stored at
227 the iteration specified by \fB\-store\fR. This option uses the format of
228 the \fIdddmp\fR library. Together with \fB\-loadfile\fR, it implements a
229 primitive checkpointing capability. It is primitive because the transition
230 relation is not saved; because the frontier states are not saved; and
231 because only one check point can be specified.
234 Save the BDD of the reached states at iteration \fIn\fR. This option
235 requires \fB\-storefile\fR.
237 .B \-loadfile \fIfile\fB
238 Load the BDD of the initial states from \fIfile\fR. This option uses the
239 format of the \fIdddmp\fR library. Together with \fB\-storefile\fR, it
240 implements a primitive checkpointing capability.
243 do not build the BDDs. Quit after determining the initial variable
247 drop BDDs for intermediate nodes as soon as possible. If this option is
248 not specified, the BDDs for the intermediate nodes of the circuit are
249 dropped just before the final reordering.
252 build BDDs only for the next state functions of a sequential circuit.
255 build BDD only for \fInode\fR.
257 .B \-order \fIfile\fB
258 read the variable order from \fIfile\fR. This file must contain the
259 names of the inputs (and present state variables) in the desired order.
260 Names must be separated by white space or newlines.
262 .B \-ordering \fImethod\fB
263 use \fImethod\fR to derive an initial variable order. \fImethod\fR can
264 be one of \fIhw\fR, \fIdfs\fR. Method \fIhw\fR uses the order in which the
265 inputs are listed in the circuit description.
268 enable dynamic reordering. By default, dynamic reordering is disabled.
269 If enabled, the default method is sifting.
272 do first dynamic reordering when the BDDs reach \fIn\fR nodes.
273 The default value is 4004. (Don't ask why.)
276 include dead nodes in node count when deciding whether to reorder
277 dynamically. By default, only live nodes are counted.
280 maximum percentage by which the BDDs may grow while sifting one
281 variable. The default value is 20.
283 .B \-automethod \fImethod\fB
284 use \fImethod\fR for dynamic reordering of the BDDs. \fImethod\fR can
285 be one of none, random, pivot, sifting, converge, symm, cosymm, group,
286 cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing,
287 genetic, exact. The default method is sifting.
289 .B \-reordering \fImethod\fB
290 use \fImethod\fR for the final reordering of the BDDs. \fImethod\fR can
291 be one of none, random, pivot, sifting, converge, symm, cosymm, group,
292 cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing,
293 genetic, exact. The default method is none.
296 run the genetic algorithm after the final reordering (which in this case
297 is no longer final). This allows the genetic algorithm to have one good
298 solution generated by, say, sifting, in the initial population.
300 .B \-groupcheck \fImethod\fB
301 use \fImethod\fR for the the creation of groups in group sifting.
302 \fImethod\fR can be one of nocheck, check5, check7. Method check5 uses
303 extended symmetry as aggregation criterion; group7, in addition, also
304 uses the second difference criterion. The default value is check7.
306 .B \-arcviolation \fIn\fB
307 percentage of arcs that violate the symmetry condition in the aggregation
308 check of group sifting. Should be between 0 and 100. The default value is
309 10. A larger value causes more aggregation.
311 .B \-symmviolation \fIn\fB
312 percentage of nodes that violate the symmetry condition in the aggregation
313 check of group sifting. Should be between 0 and 100. The default value is
314 10. A larger value causes more aggregation.
317 threshold used in the second difference criterion for aggregation. (Used
318 by check7.) The default value is 0. A larger value causes more
319 aggregation. It can be either positive or negative.
322 read the variable group tree from \fIfile\fR. The format of this file is
323 a sequence of triplets: \fIlb ub flag\fR. Each triplet describes a
324 group: \fIlb\fR is the lowest index of the group; \fIub\fR is the
325 highest index of the group; \fIflag\fR can be either D (default) or F
326 (fixed). Fixed groups are not reordered.
329 size of the population for genetic algorithm. By default, the size of
330 the population is 3 times the number of variables, with a maximum of 120.
332 .B \-genexover \fIn\fB
333 number of crossovers at each generation for the genetic algorithm. By
334 default, the number of crossovers is 3 times the number of variables,
335 with a maximum of 50.
338 random number generator seed for the genetic algorithm and the random
339 and pivot reordering methods.
342 report progress when building the BDDs for a network. This option
343 causes the name of each primary output or next state function to be
344 printed after its BDD is built. It does not take effect if local BDDs
348 verbosity level. If negative, the program is very quiet. Larger values cause
349 more information to be printed.
351 The documentation for the CUDD package explains the various
354 The documentation for the MTR package provides details on the variable
360 "Efficient Manipulation of Decision Diagrams,"
361 Software Tools for Technology Transfer,
362 vol. 3, no. 2, pp. 171-181, 2001.
364 S. Panda, F. Somenzi, and B. F. Plessier,
365 "Symmetry Detection and Dynamic Variable Ordering of Decision Diagrams,"
366 IEEE International Conference on Computer-Aided Design,
367 pp. 628-631, November 1994.
369 S. Panda and F. Somenzi,
370 "Who Are the Variables in Your Neighborhood,"
371 IEEE International Conference on Computer-Aided Design,
372 pp. 74-77, November 1995.
374 G. D. Hachtel and F. Somenzi,
375 "A Symbolic Algorithm for Maximum Flow in 0-1 Networks,"
376 IEEE International Conference on Computer-Aided Design,
377 pp. 403-406, November 1993.
379 Fabio Somenzi, University of Colorado at Boulder.