1 | .\" $Id: nanotrav.1,v 1.23 2009/02/21 06:00:31 fabio Exp fabio $ |
---|
2 | .\" |
---|
3 | .TH NANOTRAV 1 "18 June 2002" "Release 0.11" |
---|
4 | .SH NAME |
---|
5 | nanotrav \- a simple state graph traversal program |
---|
6 | .SH SYNOPSIS |
---|
7 | .B nanotrav |
---|
8 | [option ...] |
---|
9 | .SH DESCRIPTION |
---|
10 | |
---|
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. |
---|
22 | .SH OPTIONS |
---|
23 | .TP 10 |
---|
24 | .B \fIfile\fB |
---|
25 | read input in blif format from \fIfile\fR. |
---|
26 | .TP 10 |
---|
27 | .B \-f \fIfile\fB |
---|
28 | read options from \fIfile\fR. |
---|
29 | .TP 10 |
---|
30 | .B \-trav |
---|
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. |
---|
34 | .TP 10 |
---|
35 | .B \-depend |
---|
36 | perform dependent variable analysis after traversal. |
---|
37 | .TP 10 |
---|
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. |
---|
42 | .TP 10 |
---|
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, |
---|
46 | \fIfixed\fR. |
---|
47 | .TP 10 |
---|
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 |
---|
51 | \fIclip\fR. |
---|
52 | .TP 10 |
---|
53 | .B \-depth \fIn\fB |
---|
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 |
---|
56 | is 1 (no clipping). |
---|
57 | .TP 10 |
---|
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 |
---|
64 | then compared. |
---|
65 | .TP 10 |
---|
66 | .B \-closure |
---|
67 | perform reachability analysis using the transitive closure of the |
---|
68 | transition relation. |
---|
69 | .TP 10 |
---|
70 | .B \-cdepth \fIn\fB |
---|
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 |
---|
73 | is 1 (no clipping). |
---|
74 | .TP 10 |
---|
75 | .B \-envelope |
---|
76 | compute the greatest fixed point of the state transition |
---|
77 | relation. (This greatest fixed point is also called the outer envelope |
---|
78 | of the graph.) |
---|
79 | .TP 10 |
---|
80 | .B \-scc |
---|
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. |
---|
84 | .TP 10 |
---|
85 | .B \-maxflow |
---|
86 | compute the maximum flow in the network defined by the state graph. |
---|
87 | .TP 10 |
---|
88 | .B \-sink \fIfile\fB |
---|
89 | read the sink for maximum flow computation from \fIfile\fR. The source |
---|
90 | is given by the initial states. |
---|
91 | .TP 10 |
---|
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. |
---|
95 | .TP 10 |
---|
96 | .B \-selective |
---|
97 | use selective tracing variant of the \fIsquare\fR method for shortest |
---|
98 | paths. |
---|
99 | .TP 10 |
---|
100 | .B \-part |
---|
101 | compute the conjunctive decomposition of the transition relation. The |
---|
102 | network must be sequential for the test to take place. |
---|
103 | .TP 10 |
---|
104 | .B \-sign |
---|
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. |
---|
110 | .TP 10 |
---|
111 | .B \-zdd |
---|
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 |
---|
118 | primary outputs. |
---|
119 | .TP 10 |
---|
120 | .B \-cover |
---|
121 | print irredundant sums of products for the primary outputs. This |
---|
122 | option implies \fB\-zdd\fR. |
---|
123 | .TP 10 |
---|
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. |
---|
129 | .TP 10 |
---|
130 | .B \-density |
---|
131 | test BDD approximation functions. |
---|
132 | .TP 10 |
---|
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. |
---|
137 | .TP 10 |
---|
138 | .B \-threshold \fIn\fB |
---|
139 | Use \fIn\fR as threshold when approximating BDDs. |
---|
140 | .TP 10 |
---|
141 | .B \-quality \fIn\fB |
---|
142 | Use \fIn\fR (a floating point number) as quality factor when |
---|
143 | approximating BDDs. Default value is 1. |
---|
144 | .TP 10 |
---|
145 | .B \-decomp |
---|
146 | test BDD decomposition functions. |
---|
147 | .TP 10 |
---|
148 | .B \-cofest |
---|
149 | test cofactor estimation functions. |
---|
150 | .TP 10 |
---|
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. |
---|
154 | .TP 10 |
---|
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. |
---|
158 | .TP 10 |
---|
159 | .B \-closest |
---|
160 | test function that finds a cube in a BDD at minimum Hamming distance |
---|
161 | from another BDD. |
---|
162 | .TP 10 |
---|
163 | .B \-clauses |
---|
164 | test function that extracts two-literal clauses from a DD. |
---|
165 | .TP 10 |
---|
166 | .B \-char2vect |
---|
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 |
---|
170 | outputs. |
---|
171 | .TP 10 |
---|
172 | .B \-local |
---|
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 |
---|
176 | local inputs. |
---|
177 | .TP 10 |
---|
178 | .B \-cache \fIn\fB |
---|
179 | set the initial size of the computed table to \fIn\fR. |
---|
180 | .TP 10 |
---|
181 | .B \-slots \fIn\fB |
---|
182 | set the initial size of each unique subtable to \fIn\fR. |
---|
183 | .TP 10 |
---|
184 | .B \-maxmem \fIn\fB |
---|
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. |
---|
188 | .TP 10 |
---|
189 | .B \-memhard \fIn\fB |
---|
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. |
---|
193 | .TP 10 |
---|
194 | .B \-maxlive \fIn\fB |
---|
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. |
---|
197 | .TP 10 |
---|
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.) |
---|
201 | .TP 10 |
---|
202 | .B \-dumpblif |
---|
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 |
---|
206 | drawing of the BDDs. |
---|
207 | .TP 10 |
---|
208 | .B \-dumpmv |
---|
209 | use blif-MV format for dump of BDDs. The BDDs are dumped as a network |
---|
210 | of multiplexers. |
---|
211 | .TP 10 |
---|
212 | .B \-dumpdaVinci |
---|
213 | use daVinci format for dump of BDDs. |
---|
214 | .TP 10 |
---|
215 | .B \-dumpddcal |
---|
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. |
---|
219 | .TP 10 |
---|
220 | .B \-dumpfact |
---|
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. |
---|
224 | .TP 10 |
---|
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. |
---|
232 | .TP 10 |
---|
233 | .B \-store \fIn\fB |
---|
234 | Save the BDD of the reached states at iteration \fIn\fR. This option |
---|
235 | requires \fB\-storefile\fR. |
---|
236 | .TP 10 |
---|
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. |
---|
241 | .TP 10 |
---|
242 | .B \-nobuild |
---|
243 | do not build the BDDs. Quit after determining the initial variable |
---|
244 | order. |
---|
245 | .TP 10 |
---|
246 | .B \-drop |
---|
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. |
---|
250 | .TP 10 |
---|
251 | .B \-delta |
---|
252 | build BDDs only for the next state functions of a sequential circuit. |
---|
253 | .TP 10 |
---|
254 | .B \-node |
---|
255 | build BDD only for \fInode\fR. |
---|
256 | .TP 10 |
---|
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. |
---|
261 | .TP 10 |
---|
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. |
---|
266 | .TP 10 |
---|
267 | .B \-autodyn |
---|
268 | enable dynamic reordering. By default, dynamic reordering is disabled. |
---|
269 | If enabled, the default method is sifting. |
---|
270 | .TP 10 |
---|
271 | .B \-first \fIn\fB |
---|
272 | do first dynamic reordering when the BDDs reach \fIn\fR nodes. |
---|
273 | The default value is 4004. (Don't ask why.) |
---|
274 | .TP 10 |
---|
275 | .B \-countdead |
---|
276 | include dead nodes in node count when deciding whether to reorder |
---|
277 | dynamically. By default, only live nodes are counted. |
---|
278 | .TP 10 |
---|
279 | .B \-growth \fIn\fB |
---|
280 | maximum percentage by which the BDDs may grow while sifting one |
---|
281 | variable. The default value is 20. |
---|
282 | .TP 10 |
---|
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. |
---|
288 | .TP 10 |
---|
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. |
---|
294 | .TP 10 |
---|
295 | .B \-genetic |
---|
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. |
---|
299 | .TP 10 |
---|
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. |
---|
305 | .TP 10 |
---|
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. |
---|
310 | .TP 10 |
---|
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. |
---|
315 | .TP 10 |
---|
316 | .B \-recomb \fIn\fB |
---|
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. |
---|
320 | .TP 10 |
---|
321 | .B \-tree \fIfile\fB |
---|
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. |
---|
327 | .TP 10 |
---|
328 | .B \-genepop \fIn\fB |
---|
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. |
---|
331 | .TP 10 |
---|
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. |
---|
336 | .TP 10 |
---|
337 | .B \-seed \fIn\fB |
---|
338 | random number generator seed for the genetic algorithm and the random |
---|
339 | and pivot reordering methods. |
---|
340 | .TP 10 |
---|
341 | .B \-progress |
---|
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 |
---|
345 | are requested. |
---|
346 | .TP 10 |
---|
347 | .B -p \fIn\fB |
---|
348 | verbosity level. If negative, the program is very quiet. Larger values cause |
---|
349 | more information to be printed. |
---|
350 | .SH SEE ALSO |
---|
351 | The documentation for the CUDD package explains the various |
---|
352 | reordering methods. |
---|
353 | |
---|
354 | The documentation for the MTR package provides details on the variable |
---|
355 | groups. |
---|
356 | |
---|
357 | dot(1) |
---|
358 | .SH REFERENCES |
---|
359 | F. Somenzi, |
---|
360 | "Efficient Manipulation of Decision Diagrams," |
---|
361 | Software Tools for Technology Transfer, |
---|
362 | vol. 3, no. 2, pp. 171-181, 2001. |
---|
363 | |
---|
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. |
---|
368 | |
---|
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. |
---|
373 | |
---|
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. |
---|
378 | .SH AUTHOR |
---|
379 | Fabio Somenzi, University of Colorado at Boulder. |
---|