source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/nanotrav.1

Last change on this file was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 13.9 KB
Line 
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
5nanotrav \- a simple state graph traversal program
6.SH SYNOPSIS
7.B nanotrav
8[option ...]
9.SH DESCRIPTION
10
11nanotrav builds the BDDs of a circuit and applies various reordering
12methods to the BDDs. It then traverses the state transition graph of
13the circuit if the circuit is sequential, and if the user so requires.
14nanotrav is based on the CUDD package. The ordering of the variables
15is affected by three sets of options: the options that specify the
16initial order (-order -ordering); the options that specify the
17reordering while the BDDs are being built (-autodyn -automethod); and
18the options to specify the final reordering (-reordering
19-genetic). Notice that both -autodyn and -automethod must be specified
20to get dynamic reordering. The first enables reordering, while the
21second says what method to use.
22.SH OPTIONS
23.TP 10
24.B \fIfile\fB
25read input in blif format from \fIfile\fR.
26.TP 10
27.B \-f \fIfile\fB
28read options from \fIfile\fR.
29.TP 10
30.B \-trav
31traverse the state transition graph after building the BDDs. This
32option has effect only if the circuit is sequential. The initial
33states for traversal are taken from the blif file.
34.TP 10
35.B \-depend
36perform dependent variable analysis after traversal.
37.TP 10
38.B \-from \fImethod\fB
39use \fImethod\fR to choose the frontier states for image computation
40during 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
44use \fImethod\fR to group the corresponding current and next state
45variables. Allowed methods are: \fInone\fR (default), \fIdefault\fR,
46\fIfixed\fR.
47.TP 10
48.B \-image \fImethod\fB
49use \fImethod\fR for image computation during traversal. Allowed
50methods are: \fImono\fR (default), \fIpart\fR, \fIdepend\fR, and
51\fIclip\fR.
52.TP 10
53.B \-depth \fIn\fB
54use \fIn\fR to derive the clipping depth for image
55computation. It should be a number between 0 and 1. The default value
56is 1 (no clipping).
57.TP 10
58.B \-verify \fIfile\fB
59perform combinational verification checking for equivalence to
60the network in \fIfile\fR. The two networks being compared must use
61the same names for inputs, outputs, and present and next state
62variables.  The method used for verification is extremely
63simplistic. BDDs are built for all outputs of both networks, and are
64then compared.
65.TP 10
66.B \-closure
67perform reachability analysis using the transitive closure of the
68transition relation.
69.TP 10
70.B \-cdepth \fIn\fB
71use \fIn\fR to derive the clipping depth for transitive closure
72computation. It should be a number between 0 and 1. The default value
73is 1 (no clipping).
74.TP 10
75.B \-envelope
76compute the greatest fixed point of the state transition
77relation. (This greatest fixed point is also called the outer envelope
78of the graph.)
79.TP 10
80.B \-scc
81compute the strongly connected components of the state transition
82graph. The algorithm enumerates the SCCs; therefore it stops after a
83small number of them has been computed.
84.TP 10
85.B \-maxflow
86compute the maximum flow in the network defined by the state graph.
87.TP 10
88.B \-sink \fIfile\fB
89read the sink for maximum flow computation from \fIfile\fR. The source
90is given by the initial states.
91.TP 10
92.B \-shortpaths \fImethod\fB
93compute the distances between states.  Allowed methods are: \fInone\fR
94(default), \fIbellman\fR, \fIfloyd\fR, and \fIsquare\fR.
95.TP 10
96.B \-selective
97use selective tracing variant of the \fIsquare\fR method for shortest
98paths.
99.TP 10
100.B \-part
101compute the conjunctive decomposition of the transition relation.  The
102network must be sequential for the test to take place.
103.TP 10
104.B \-sign
105compute signatures. For each output of the circuit, all inputs are
106assigned a signature. The signature is the fraction of minterms in the
107ON\-set of the positive cofactor of the output with respect to the
108input. Signatures are useful in identifying the equivalence of circuits
109with unknown input or output correspondence.
110.TP 10
111.B \-zdd
112perform 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
114outputs of the circuit. These are converted to ZDDs and the ZDDs are
115then converted back to BDDs and checked against the original ones.  A
116few more functions are exercised and reordering is applied if it is
117enabled. Then irredundant sums of products are produced for the
118primary outputs.
119.TP 10
120.B \-cover
121print irredundant sums of products for the primary outputs.  This
122option implies \fB\-zdd\fR.
123.TP 10
124.B \-second \fIfile\fB
125read a second network from \fIfile\fR. Currently, if this option is
126specified, a test of BDD minimization algorithms is performed using
127the largest output of the second network as constraint.  Inputs of the
128two networks with the same names are merged.
129.TP 10
130.B \-density
131test BDD approximation functions.
132.TP 10
133.B \-approx \fImethod\fB
134if \fImethod\fR is \fIunder\fR (default) perform underapproximation
135when BDDs are approximated. If \fImethod\fR is \fIover\fR perform
136overapproximation when BDDs are approximated.
137.TP 10
138.B \-threshold \fIn\fB
139Use \fIn\fR as threshold when approximating BDDs.
140.TP 10
141.B \-quality \fIn\fB
142Use \fIn\fR (a floating point number) as quality factor when
143approximating BDDs. Default value is 1.
144.TP 10
145.B \-decomp
146test BDD decomposition functions.
147.TP 10
148.B \-cofest
149test cofactor estimation functions.
150.TP 10
151.B \-clip \fIn file\fB
152test clipping functions using \fIn\fR to determine the clipping depth
153and taking one operand from the network in \fIfile\fR.
154.TP 10
155.B \-dctest \fIfile\fB
156test functions for equality and containment under don't care
157conditions taking the don't care conditions from \fIfile\fR.
158.TP 10
159.B \-closest
160test function that finds a cube in a BDD at minimum Hamming distance
161from another BDD.
162.TP 10
163.B \-clauses
164test function that extracts two-literal clauses from a DD.
165.TP 10
166.B \-char2vect
167perform a simple test of the conversion from characteristic function
168to functional vector.  If the network is sequential, the test is
169applied to the monolithic transition relation; otherwise to the primary
170outputs.
171.TP 10
172.B \-local
173build local BDDs for each gate of the circuit.  This option is not in
174effect if traversal, outer envelope computation, or maximum flow
175computation are requested.  The local BDD of a gate is in terms of its
176local inputs.
177.TP 10
178.B \-cache \fIn\fB
179set the initial size of the computed table to \fIn\fR.
180.TP 10
181.B \-slots \fIn\fB
182set the initial size of each unique subtable to \fIn\fR.
183.TP 10
184.B \-maxmem \fIn\fB
185set the target maximum memory occupation to \fIn\fR MB.  If this
186parameter is not specified or if \fIn\fR is 0, then a suitable value
187is computed automatically.
188.TP 10
189.B \-memhard \fIn\fB
190set the hard limit to memory occupation to \fIn\fR MB.  If this
191parameter is not specified or if \fIn\fR is 0, no hard limit is
192enforced by the program.
193.TP 10
194.B \-maxlive \fIn\fB
195set the hard limit to the number of live BDD nodes to \fIn\fR.  If
196this parameter is not specified, the limit is four billion nodes.
197.TP 10
198.B \-dumpfile \fIfile\fB
199dump BDDs to \fIfile\fR. The BDDs are dumped just before program
200termination. (Hence, after reordering, if reordering is specified.)
201.TP 10
202.B \-dumpblif
203use blif format for dump of BDDs (default is dot format). If blif is
204used, the BDDs are dumped as a network of multiplexers. The dot format
205is suitable for input to the dot program, which produces a
206drawing of the BDDs.
207.TP 10
208.B \-dumpmv
209use blif-MV format for dump of BDDs.  The BDDs are dumped as a network
210of multiplexers.
211.TP 10
212.B \-dumpdaVinci
213use daVinci format for dump of BDDs.
214.TP 10
215.B \-dumpddcal
216use DDcal format for dump of BDDs.  This option may produce an invalid
217output if the variable and output names of the BDDs being dumped do
218not comply with the restrictions imposed by the DDcal format.
219.TP 10
220.B \-dumpfact
221use factored form format for dump of BDDs. This option must be used
222with caution because the size of the output is proportional to the
223number of paths in the BDD.
224.TP 10
225.B \-storefile \fIfile\fB
226Save the BDD of the reachable states to \fIfile\fR. The BDD is stored at
227the iteration specified by \fB\-store\fR. This option uses the format of
228the \fIdddmp\fR library. Together with \fB\-loadfile\fR, it implements a
229primitive checkpointing capability. It is primitive because the transition
230relation is not saved; because the frontier states are not saved; and
231because only one check point can be specified.
232.TP 10
233.B \-store \fIn\fB
234Save the BDD of the reached states at iteration \fIn\fR. This option
235requires \fB\-storefile\fR.
236.TP 10
237.B \-loadfile \fIfile\fB
238Load the BDD of the initial states from \fIfile\fR.  This option uses the
239format of the \fIdddmp\fR library. Together with \fB\-storefile\fR, it
240implements a primitive checkpointing capability.
241.TP 10
242.B \-nobuild
243do not build the BDDs. Quit after determining the initial variable
244order.
245.TP 10
246.B \-drop
247drop BDDs for intermediate nodes as soon as possible. If this option is
248not specified, the BDDs for the intermediate nodes of the circuit are
249dropped just before the final reordering.
250.TP 10
251.B \-delta
252build BDDs only for the next state functions of a sequential circuit.
253.TP 10
254.B \-node
255build BDD only for \fInode\fR.
256.TP 10
257.B \-order \fIfile\fB
258read the variable order from \fIfile\fR. This file must contain the
259names of the inputs (and present state variables) in the desired order.
260Names must be separated by white space or newlines.
261.TP 10
262.B \-ordering \fImethod\fB
263use \fImethod\fR to derive an initial variable order. \fImethod\fR can
264be one of \fIhw\fR, \fIdfs\fR. Method \fIhw\fR uses the order in which the
265inputs are listed in the circuit description.
266.TP 10
267.B \-autodyn
268enable dynamic reordering. By default, dynamic reordering is disabled.
269If enabled, the default method is sifting.
270.TP 10
271.B \-first \fIn\fB
272do first dynamic reordering when the BDDs reach \fIn\fR nodes.
273The default value is 4004. (Don't ask why.)
274.TP 10
275.B \-countdead
276include dead nodes in node count when deciding whether to reorder
277dynamically. By default, only live nodes are counted.
278.TP 10
279.B \-growth \fIn\fB
280maximum percentage by which the BDDs may grow while sifting one
281variable. The default value is 20.
282.TP 10
283.B \-automethod \fImethod\fB
284use \fImethod\fR for dynamic reordering of the BDDs. \fImethod\fR can
285be one of none, random, pivot, sifting, converge, symm, cosymm, group,
286cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing,
287genetic, exact. The default method is sifting.
288.TP 10
289.B \-reordering \fImethod\fB
290use \fImethod\fR for the final reordering of the BDDs. \fImethod\fR can
291be one of none, random, pivot, sifting, converge, symm, cosymm, group,
292cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing,
293genetic, exact. The default method is none.
294.TP 10
295.B \-genetic
296run the genetic algorithm after the final reordering (which in this case
297is no longer final). This allows the genetic algorithm to have one good
298solution generated by, say, sifting, in the initial population.
299.TP 10
300.B \-groupcheck \fImethod\fB
301use \fImethod\fR for the the creation of groups in group sifting.
302\fImethod\fR can be one of nocheck, check5, check7. Method check5 uses
303extended symmetry as aggregation criterion; group7, in addition, also
304uses the second difference criterion. The default value is check7.
305.TP 10
306.B \-arcviolation \fIn\fB
307percentage of arcs that violate the symmetry condition in the aggregation
308check of group sifting. Should be between 0 and 100. The default value is
30910. A larger value causes more aggregation.
310.TP 10
311.B \-symmviolation \fIn\fB
312percentage of nodes that violate the symmetry condition in the aggregation
313check of group sifting. Should be between 0 and 100. The default value is
31410. A larger value causes more aggregation.
315.TP 10
316.B \-recomb \fIn\fB
317threshold used in the second difference criterion for aggregation. (Used
318by check7.) The default value is 0. A larger value causes more
319aggregation. It can be either positive or negative.
320.TP 10
321.B \-tree \fIfile\fB
322read the variable group tree from \fIfile\fR. The format of this file is
323a sequence of triplets: \fIlb ub flag\fR. Each triplet describes a
324group: \fIlb\fR is the lowest index of the group; \fIub\fR is the
325highest 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
329size of the population for genetic algorithm. By default, the size of
330the population is 3 times the number of variables, with a maximum of 120.
331.TP 10
332.B \-genexover \fIn\fB
333number of crossovers at each generation for the genetic algorithm. By
334default, the number of crossovers is 3 times the number of variables,
335with a maximum of 50.
336.TP 10
337.B \-seed \fIn\fB
338random number generator seed for the genetic algorithm and the random
339and pivot reordering methods.
340.TP 10
341.B \-progress
342report progress when building the BDDs for a network. This option
343causes the name of each primary output or next state function to be
344printed after its BDD is built. It does not take effect if local BDDs
345are requested.
346.TP 10
347.B -p \fIn\fB
348verbosity level. If negative, the program is very quiet. Larger values cause
349more information to be printed.
350.SH SEE ALSO
351The documentation for the CUDD package explains the various
352reordering methods.
353
354The documentation for the MTR package provides details on the variable
355groups.
356
357dot(1)
358.SH REFERENCES
359F. Somenzi,
360"Efficient Manipulation of Decision Diagrams,"
361Software Tools for Technology Transfer,
362vol. 3, no. 2, pp. 171-181, 2001.
363
364S. Panda, F. Somenzi, and B. F. Plessier,
365"Symmetry Detection and Dynamic Variable Ordering of Decision Diagrams,"
366IEEE International Conference on Computer-Aided Design,
367pp. 628-631, November 1994.
368
369S. Panda and F. Somenzi,
370"Who Are the Variables in Your Neighborhood,"
371IEEE International Conference on Computer-Aided Design,
372pp. 74-77, November 1995.
373
374G. D. Hachtel and F. Somenzi,
375"A Symbolic Algorithm for Maximum Flow in 0-1 Networks,"
376IEEE International Conference on Computer-Aided Design,
377pp. 403-406, November 1993.
378.SH AUTHOR
379Fabio Somenzi, University of Colorado at Boulder.
Note: See TracBrowser for help on using the repository browser.