1NANOTRAV(1) General Commands Manual NANOTRAV(1)
2
6 nanotrav - a simple state graph traversal program
7
9 nanotrav [option ...]
10
12 nanotrav builds the BDDs of a circuit and applies various reordering
13 methods to the BDDs. It then traverses the state transition graph of
14 the circuit if the circuit is sequential, and if the user so requires.
15 nanotrav is based on the CUDD package. The ordering of the variables is
16 affected by three sets of options: the options that specify the initial
17 order (-order -ordering); the options that specify the reordering while
18 the BDDs are being built (-autodyn -automethod); and the options to
19 specify the final reordering (-reordering -genetic). Notice that both
20 -autodyn and -automethod must be specified to get dynamic reordering.
21 The first enables reordering, while the second says what method to use.
22
24 file read input in blif format from file.
25 -f file read options from file.
27 -trav traverse the state transition graph after building the BDDs.
29 This option has effect only if the circuit is sequential. The
30 initial states for traversal are taken from the blif file.
31 -depend perform dependent variable analysis after traversal.
33 -from method
35 use method to choose the frontier states for image computa‐
36 tion during traversal. Allowed methods are: new (default),
37 reached, restrict, compact, squeeze, subset, superset.
38 -groupnsps method
40 use method to group the corresponding current and next state
41 variables. Allowed methods are: none (default), default,
42 fixed.
43 -image method
45 use method for image computation during traversal. Allowed
46 methods are: mono (default), part, depend, and clip.
47 -depth n use n to derive the clipping depth for image computation. It
49 should be a number between 0 and 1. The default value is 1
50 (no clipping).
51 -verify file
53 perform combinational verification checking for equivalence
54 to the network in file. The two networks being compared must
55 use the same names for inputs, outputs, and present and next
56 state variables. The method used for verification is
57 extremely simplistic. BDDs are built for all outputs of both
58 networks, and are then compared.
59 -closure perform reachability analysis using the transitive closure of
61 the transition relation.
62 -cdepth n use n to derive the clipping depth for transitive closure
64 computation. It should be a number between 0 and 1. The
65 default value is 1 (no clipping).
66 -envelope compute the greatest fixed point of the state transition
68 relation. (This greatest fixed point is also called the outer
69 envelope of the graph.)
70 -scc compute the strongly connected components of the state tran‐
72 sition graph. The algorithm enumerates the SCCs; therefore it
73 stops after a small number of them has been computed.
74 -maxflow compute the maximum flow in the network defined by the state
76 graph.
77 -sink file
79 read the sink for maximum flow computation from file. The
80 source is given by the initial states.
81 -shortpaths method
83 compute the distances between states. Allowed methods are:
84 none (default), bellman, floyd, and square.
85 -selective
87 use selective tracing variant of the square method for short‐
88 est paths.
89 -part compute the conjunctive decomposition of the transition rela‐
91 tion. The network must be sequential for the test to take
92 place.
93 -sign compute signatures. For each output of the circuit, all
95 inputs are assigned a signature. The signature is the frac‐
96 tion of minterms in the ON-set of the positive cofactor of
97 the output with respect to the input. Signatures are useful
98 in identifying the equivalence of circuits with unknown input
99 or output correspondence.
100 -zdd perform a simple test of ZDD functions. This test is not exe‐
102 cuted if -delta is also specified, because it uses the BDDs
103 of the primary outputs of the circuit. These are converted to
104 ZDDs and the ZDDs are then converted back to BDDs and checked
105 against the original ones. A few more functions are exer‐
106 cised and reordering is applied if it is enabled. Then irre‐
107 dundant sums of products are produced for the primary out‐
108 puts.
109 -cover print irredundant sums of products for the primary outputs.
111 This option implies -zdd.
112 -second file
114 read a second network from file. Currently, if this option is
115 specified, a test of BDD minimization algorithms is performed
116 using the largest output of the second network as constraint.
117 Inputs of the two networks with the same names are merged.
118 -density test BDD approximation functions.
120 -approx method
122 if method is under (default) perform underapproximation when
123 BDDs are approximated. If method is over perform overapproxi‐
124 mation when BDDs are approximated.
125 -threshold n
127 Use n as threshold when approximating BDDs.
128 -quality n
130 Use n (a floating point number) as quality factor when
131 approximating BDDs. Default value is 1.
132 -decomp test BDD decomposition functions.
134 -cofest test cofactor estimation functions.
136 -clip n file
138 test clipping functions using n to determine the clipping
139 depth and taking one operand from the network in file.
140 -dctest file
142 test functions for equality and containment under don't care
143 conditions taking the don't care conditions from file.
144 -closest test function that finds a cube in a BDD at minimum Hamming
146 distance from another BDD.
147 -clauses test function that extracts two-literal clauses from a DD.
149 -char2vect
151 perform a simple test of the conversion from characteristic
152 function to functional vector. If the network is sequential,
153 the test is applied to the monolithic transition relation;
154 otherwise to the primary outputs.
155 -local build local BDDs for each gate of the circuit. This option
157 is not in effect if traversal, outer envelope computation, or
158 maximum flow computation are requested. The local BDD of a
159 gate is in terms of its local inputs.
160 -cache n set the initial size of the computed table to n.
162 -slots n set the initial size of each unique subtable to n.
164 -maxmem n set the target maximum memory occupation to n MB. If this
166 parameter is not specified or if n is 0, then a suitable
167 value is computed automatically.
168 -memhard n
170 set the hard limit to memory occupation to n MB. If this
171 parameter is not specified or if n is 0, no hard limit is
172 enforced by the program.
173 -maxlive n
175 set the hard limit to the number of live BDD nodes to n. If
176 this parameter is not specified, the limit is four billion
177 nodes.
178 -dumpfile file
180 dump BDDs to file. The BDDs are dumped just before program
181 termination. (Hence, after reordering, if reordering is spec‐
182 ified.)
183 -dumpblif use blif format for dump of BDDs (default is dot format). If
185 blif is used, the BDDs are dumped as a network of multiplex‐
186 ers. The dot format is suitable for input to the dot program,
187 which produces a drawing of the BDDs.
188 -dumpmv use blif-MV format for dump of BDDs. The BDDs are dumped as
190 a network of multiplexers.
191 -dumpdaVinci
193 use daVinci format for dump of BDDs.
194 -dumpddcal
196 use DDcal format for dump of BDDs. This option may produce
197 an invalid output if the variable and output names of the
198 BDDs being dumped do not comply with the restrictions imposed
199 by the DDcal format.
200 -dumpfact use factored form format for dump of BDDs. This option must
202 be used with caution because the size of the output is pro‐
203 portional to the number of paths in the BDD.
204 -storefile file
206 Save the BDD of the reachable states to file. The BDD is
207 stored at the iteration specified by -store. This option uses
208 the format of the dddmp library. Together with -loadfile, it
209 implements a primitive checkpointing capability. It is primi‐
210 tive because the transition relation is not saved; because
211 the frontier states are not saved; and because only one check
212 point can be specified.
213 -store n Save the BDD of the reached states at iteration n. This
215 option requires -storefile.
216 -loadfile file
218 Load the BDD of the initial states from file. This option
219 uses the format of the dddmp library. Together with -store‐
220 file, it implements a primitive checkpointing capability.
221 -nobuild do not build the BDDs. Quit after determining the initial
223 variable order.
224 -drop drop BDDs for intermediate nodes as soon as possible. If this
226 option is not specified, the BDDs for the intermediate nodes
227 of the circuit are dropped just before the final reordering.
228 -delta build BDDs only for the next state functions of a sequential
230 circuit.
231 -node build BDD only for node.
233 -order file
235 read the variable order from file. This file must contain the
236 names of the inputs (and present state variables) in the
237 desired order. Names must be separated by white space or
238 newlines.
239 -ordering method
241 use method to derive an initial variable order. method can be
242 one of hw, dfs. Method hw uses the order in which the inputs
243 are listed in the circuit description.
244 -autodyn enable dynamic reordering. By default, dynamic reordering is
246 disabled. If enabled, the default method is sifting.
247 -first n do first dynamic reordering when the BDDs reach n nodes. The
249 default value is 4004. (Don't ask why.)
250 -countdead
252 include dead nodes in node count when deciding whether to
253 reorder dynamically. By default, only live nodes are counted.
254 -growth n maximum percentage by which the BDDs may grow while sifting
256 one variable. The default value is 20.
257 -automethod method
259 use method for dynamic reordering of the BDDs. method can be
260 one of none, random, pivot, sifting, converge, symm, cosymm,
261 group, cogroup, win2, win3, win4, win2conv, win3conv,
262 win4conv, annealing, genetic, exact. The default method is
263 sifting.
264 -reordering method
266 use method for the final reordering of the BDDs. method can
267 be one of none, random, pivot, sifting, converge, symm,
268 cosymm, group, cogroup, win2, win3, win4, win2conv, win3conv,
269 win4conv, annealing, genetic, exact. The default method is
270 none.
271 -genetic run the genetic algorithm after the final reordering (which
273 in this case is no longer final). This allows the genetic
274 algorithm to have one good solution generated by, say, sift‐
275 ing, in the initial population.
276 -groupcheck method
278 use method for the the creation of groups in group sifting.
279 method can be one of nocheck, check5, check7. Method check5
280 uses extended symmetry as aggregation criterion; group7, in
281 addition, also uses the second difference criterion. The
282 default value is check7.
283 -arcviolation n
285 percentage of arcs that violate the symmetry condition in the
286 aggregation check of group sifting. Should be between 0 and
287 100. The default value is 10. A larger value causes more
288 aggregation.
289 -symmviolation n
291 percentage of nodes that violate the symmetry condition in
292 the aggregation check of group sifting. Should be between 0
293 and 100. The default value is 10. A larger value causes more
294 aggregation.
295 -recomb n threshold used in the second difference criterion for aggre‐
297 gation. (Used by check7.) The default value is 0. A larger
298 value causes more aggregation. It can be either positive or
299 negative.
300 -tree file
302 read the variable group tree from file. The format of this
303 file is a sequence of triplets: lb ub flag. Each triplet
304 describes a group: lb is the lowest index of the group; ub is
305 the highest index of the group; flag can be either D
306 (default) or F (fixed). Fixed groups are not reordered.
307 -genepop n
309 size of the population for genetic algorithm. By default, the
310 size of the population is 3 times the number of variables,
311 with a maximum of 120.
312 -genexover n
314 number of crossovers at each generation for the genetic algo‐
315 rithm. By default, the number of crossovers is 3 times the
316 number of variables, with a maximum of 50.
317 -seed n random number generator seed for the genetic algorithm and
319 the random and pivot reordering methods.
320 -progress report progress when building the BDDs for a network. This
322 option causes the name of each primary output or next state
323 function to be printed after its BDD is built. It does not
324 take effect if local BDDs are requested.
325 -p n verbosity level. If negative, the program is very quiet.
327 Larger values cause more information to be printed.
328
330 The documentation for the CUDD package explains the various reordering
331 methods.
332 The documentation for the MTR package provides details on the variable
334 groups.
335 dot(1)
337
339 F. Somenzi, "Efficient Manipulation of Decision Diagrams," Software
340 Tools for Technology Transfer, vol. 3, no. 2, pp. 171-181, 2001.
341 S. Panda, F. Somenzi, and B. F. Plessier, "Symmetry Detection and
343 Dynamic Variable Ordering of Decision Diagrams," IEEE International
344 Conference on Computer-Aided Design, pp. 628-631, November 1994.
345 S. Panda and F. Somenzi, "Who Are the Variables in Your Neighborhood,"
347 IEEE International Conference on Computer-Aided Design, pp. 74-77, No‐
348 vember 1995.
349 G. D. Hachtel and F. Somenzi, "A Symbolic Algorithm for Maximum Flow in
351 0-1 Networks," IEEE International Conference on Computer-Aided Design,
352 pp. 403-406, November 1993.
353
355 Fabio Somenzi, University of Colorado at Boulder.
356Release 0.11 18 June 2002 NANOTRAV(1)