cudd/nanotrav/nanotrav.1

.\" $Id: nanotrav.1,v 1.23 2009/02/21 06:00:31 fabio Exp fabio $
.\"
.TH NANOTRAV 1 "18 June 2002" "Release 0.11"
.SH NAME
nanotrav \- a simple state graph traversal program
.SH SYNOPSIS
.B nanotrav
[option ...]
.SH DESCRIPTION

nanotrav builds the BDDs of a circuit and applies various reordering
methods to the BDDs. It then traverses the state transition graph of
the circuit if the circuit is sequential, and if the user so requires.
nanotrav is based on the CUDD package. The ordering of the variables
is affected by three sets of options: the options that specify the
initial order (-order -ordering); the options that specify the
reordering while the BDDs are being built (-autodyn -automethod); and
the options to specify the final reordering (-reordering
-genetic). Notice that both -autodyn and -automethod must be specified
to get dynamic reordering. The first enables reordering, while the
second says what method to use.
.SH OPTIONS
.TP 10
.B \fIfile\fB
read input in blif format from \fIfile\fR.
.TP 10
.B \-f \fIfile\fB
read options from \fIfile\fR.
.TP 10
.B \-trav
traverse the state transition graph after building the BDDs. This
option has effect only if the circuit is sequential. The initial
states for traversal are taken from the blif file.
.TP 10
.B \-depend
perform dependent variable analysis after traversal.
.TP 10
.B \-from \fImethod\fB
use \fImethod\fR to choose the frontier states for image computation
during traversal. Allowed methods are: \fInew\fR (default), \fIreached\fR,
\fIrestrict\fR, \fIcompact\fR, \fIsqueeze\fR, \fIsubset\fR, \fIsuperset\fR.
.TP 10
.B \-groupnsps \fImethod\fB
use \fImethod\fR to group the corresponding current and next state
variables. Allowed methods are: \fInone\fR (default), \fIdefault\fR,
\fIfixed\fR.
.TP 10
.B \-image \fImethod\fB
use \fImethod\fR for image computation during traversal. Allowed
methods are: \fImono\fR (default), \fIpart\fR, \fIdepend\fR, and
\fIclip\fR.
.TP 10
.B \-depth \fIn\fB
use \fIn\fR to derive the clipping depth for image
computation. It should be a number between 0 and 1. The default value
is 1 (no clipping).
.TP 10
.B \-verify \fIfile\fB
perform combinational verification checking for equivalence to
the network in \fIfile\fR. The two networks being compared must use
the same names for inputs, outputs, and present and next state
variables.  The method used for verification is extremely
simplistic. BDDs are built for all outputs of both networks, and are
then compared.
.TP 10
.B \-closure
perform reachability analysis using the transitive closure of the
transition relation.
.TP 10
.B \-cdepth \fIn\fB
use \fIn\fR to derive the clipping depth for transitive closure
computation. It should be a number between 0 and 1. The default value
is 1 (no clipping).
.TP 10
.B \-envelope
compute the greatest fixed point of the state transition
relation. (This greatest fixed point is also called the outer envelope
of the graph.)
.TP 10
.B \-scc
compute the strongly connected components of the state transition
graph. The algorithm enumerates the SCCs; therefore it stops after a
small number of them has been computed.
.TP 10
.B \-maxflow
compute the maximum flow in the network defined by the state graph.
.TP 10
.B \-sink \fIfile\fB
read the sink for maximum flow computation from \fIfile\fR. The source
is given by the initial states.
.TP 10
.B \-shortpaths \fImethod\fB
compute the distances between states.  Allowed methods are: \fInone\fR
(default), \fIbellman\fR, \fIfloyd\fR, and \fIsquare\fR.
.TP 10
.B \-selective
use selective tracing variant of the \fIsquare\fR method for shortest
paths.
.TP 10
.B \-part
compute the conjunctive decomposition of the transition relation.  The
network must be sequential for the test to take place.
.TP 10
.B \-sign
compute signatures. For each output of the circuit, all inputs are
assigned a signature. The signature is the fraction of minterms in the
ON\-set of the positive cofactor of the output with respect to the
input. Signatures are useful in identifying the equivalence of circuits
with unknown input or output correspondence.
.TP 10
.B \-zdd
perform a simple test of ZDD functions. This test is not executed if
-delta is also specified, because it uses the BDDs of the primary
outputs of the circuit. These are converted to ZDDs and the ZDDs are
then converted back to BDDs and checked against the original ones.  A
few more functions are exercised and reordering is applied if it is
enabled. Then irredundant sums of products are produced for the
primary outputs.
.TP 10
.B \-cover
print irredundant sums of products for the primary outputs.  This
option implies \fB\-zdd\fR.
.TP 10
.B \-second \fIfile\fB
read a second network from \fIfile\fR. Currently, if this option is
specified, a test of BDD minimization algorithms is performed using
the largest output of the second network as constraint.  Inputs of the
two networks with the same names are merged.
.TP 10
.B \-density
test BDD approximation functions.
.TP 10
.B \-approx \fImethod\fB
if \fImethod\fR is \fIunder\fR (default) perform underapproximation
when BDDs are approximated. If \fImethod\fR is \fIover\fR perform
overapproximation when BDDs are approximated.
.TP 10
.B \-threshold \fIn\fB
Use \fIn\fR as threshold when approximating BDDs.
.TP 10
.B \-quality \fIn\fB
Use \fIn\fR (a floating point number) as quality factor when
approximating BDDs. Default value is 1.
.TP 10
.B \-decomp
test BDD decomposition functions.
.TP 10
.B \-cofest
test cofactor estimation functions.
.TP 10
.B \-clip \fIn file\fB
test clipping functions using \fIn\fR to determine the clipping depth
and taking one operand from the network in \fIfile\fR.
.TP 10
.B \-dctest \fIfile\fB
test functions for equality and containment under don't care
conditions taking the don't care conditions from \fIfile\fR.
.TP 10
.B \-closest
test function that finds a cube in a BDD at minimum Hamming distance
from another BDD.
.TP 10
.B \-clauses
test function that extracts two-literal clauses from a DD.
.TP 10
.B \-char2vect
perform a simple test of the conversion from characteristic function
to functional vector.  If the network is sequential, the test is
applied to the monolithic transition relation; otherwise to the primary
outputs.
.TP 10
.B \-local
build local BDDs for each gate of the circuit.  This option is not in
effect if traversal, outer envelope computation, or maximum flow
computation are requested.  The local BDD of a gate is in terms of its
local inputs.
.TP 10
.B \-cache \fIn\fB
set the initial size of the computed table to \fIn\fR.
.TP 10
.B \-slots \fIn\fB
set the initial size of each unique subtable to \fIn\fR.
.TP 10
.B \-maxmem \fIn\fB
set the target maximum memory occupation to \fIn\fR MB.  If this
parameter is not specified or if \fIn\fR is 0, then a suitable value
is computed automatically.
.TP 10
.B \-memhard \fIn\fB
set the hard limit to memory occupation to \fIn\fR MB.  If this
parameter is not specified or if \fIn\fR is 0, no hard limit is
enforced by the program.
.TP 10
.B \-maxlive \fIn\fB
set the hard limit to the number of live BDD nodes to \fIn\fR.  If
this parameter is not specified, the limit is four billion nodes.
.TP 10
.B \-dumpfile \fIfile\fB
dump BDDs to \fIfile\fR. The BDDs are dumped just before program
termination. (Hence, after reordering, if reordering is specified.)
.TP 10
.B \-dumpblif
use blif format for dump of BDDs (default is dot format). If blif is
used, the BDDs are dumped as a network of multiplexers. The dot format
is suitable for input to the dot program, which produces a
drawing of the BDDs.
.TP 10
.B \-dumpmv
use blif-MV format for dump of BDDs.  The BDDs are dumped as a network
of multiplexers.
.TP 10
.B \-dumpdaVinci
use daVinci format for dump of BDDs.
.TP 10
.B \-dumpddcal
use DDcal format for dump of BDDs.  This option may produce an invalid
output if the variable and output names of the BDDs being dumped do
not comply with the restrictions imposed by the DDcal format.
.TP 10
.B \-dumpfact
use factored form format for dump of BDDs. This option must be used
with caution because the size of the output is proportional to the
number of paths in the BDD.
.TP 10
.B \-storefile \fIfile\fB
Save the BDD of the reachable states to \fIfile\fR. The BDD is stored at
the iteration specified by \fB\-store\fR. This option uses the format of
the \fIdddmp\fR library. Together with \fB\-loadfile\fR, it implements a
primitive checkpointing capability. It is primitive because the transition
relation is not saved; because the frontier states are not saved; and
because only one check point can be specified.
.TP 10
.B \-store \fIn\fB
Save the BDD of the reached states at iteration \fIn\fR. This option
requires \fB\-storefile\fR.
.TP 10
.B \-loadfile \fIfile\fB
Load the BDD of the initial states from \fIfile\fR.  This option uses the
format of the \fIdddmp\fR library. Together with \fB\-storefile\fR, it
implements a primitive checkpointing capability.
.TP 10
.B \-nobuild
do not build the BDDs. Quit after determining the initial variable
order.
.TP 10
.B \-drop
drop BDDs for intermediate nodes as soon as possible. If this option is
not specified, the BDDs for the intermediate nodes of the circuit are
dropped just before the final reordering.
.TP 10
.B \-delta
build BDDs only for the next state functions of a sequential circuit.
.TP 10
.B \-node
build BDD only for \fInode\fR.
.TP 10
.B \-order \fIfile\fB
read the variable order from \fIfile\fR. This file must contain the
names of the inputs (and present state variables) in the desired order.
Names must be separated by white space or newlines.
.TP 10
.B \-ordering \fImethod\fB
use \fImethod\fR to derive an initial variable order. \fImethod\fR can
be one of \fIhw\fR, \fIdfs\fR. Method \fIhw\fR uses the order in which the
inputs are listed in the circuit description.
.TP 10
.B \-autodyn
enable dynamic reordering. By default, dynamic reordering is disabled.
If enabled, the default method is sifting.
.TP 10
.B \-first \fIn\fB
do first dynamic reordering when the BDDs reach \fIn\fR nodes.
The default value is 4004. (Don't ask why.)
.TP 10
.B \-countdead
include dead nodes in node count when deciding whether to reorder
dynamically. By default, only live nodes are counted.
.TP 10
.B \-growth \fIn\fB
maximum percentage by which the BDDs may grow while sifting one
variable. The default value is 20.
.TP 10
.B \-automethod \fImethod\fB
use \fImethod\fR for dynamic reordering of the BDDs. \fImethod\fR can
be one of none, random, pivot, sifting, converge, symm, cosymm, group,
cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing,
genetic, linear, linconv, exact. The default method is sifting.
.TP 10
.B \-reordering \fImethod\fB
use \fImethod\fR for the final reordering of the BDDs. \fImethod\fR can
be one of none, random, pivot, sifting, converge, symm, cosymm, group,
cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing,
genetic, linear, linconv, exact. The default method is none.
.TP 10
.B \-genetic
run the genetic algorithm after the final reordering (which in this case
is no longer final). This allows the genetic algorithm to have one good
solution generated by, say, sifting, in the initial population.
.TP 10
.B \-groupcheck \fImethod\fB
use \fImethod\fR for the the creation of groups in group sifting.
\fImethod\fR can be one of nocheck, check5, check7. Method check5 uses
extended symmetry as aggregation criterion; group7, in addition, also
uses the second difference criterion. The default value is check7.
.TP 10
.B \-arcviolation \fIn\fB
percentage of arcs that violate the symmetry condition in the aggregation
check of group sifting. Should be between 0 and 100. The default value is
10. A larger value causes more aggregation.
.TP 10
.B \-symmviolation \fIn\fB
percentage of nodes that violate the symmetry condition in the aggregation
check of group sifting. Should be between 0 and 100. The default value is
10. A larger value causes more aggregation.
.TP 10
.B \-recomb \fIn\fB
threshold used in the second difference criterion for aggregation. (Used
by check7.) The default value is 0. A larger value causes more
aggregation. It can be either positive or negative.
.TP 10
.B \-tree \fIfile\fB
read the variable group tree from \fIfile\fR. The format of this file is
a sequence of triplets: \fIlb ub flag\fR. Each triplet describes a
group: \fIlb\fR is the lowest index of the group; \fIub\fR is the
highest index of the group; \fIflag\fR can be either D (default) or F
(fixed). Fixed groups are not reordered.
.TP 10
.B \-genepop \fIn\fB
size of the population for genetic algorithm. By default, the size of
the population is 3 times the number of variables, with a maximum of 120.
.TP 10
.B \-genexover \fIn\fB
number of crossovers at each generation for the genetic algorithm. By
default, the number of crossovers is 3 times the number of variables,
with a maximum of 50.
.TP 10
.B \-seed \fIn\fB
random number generator seed for the genetic algorithm and the random
and pivot reordering methods.
.TP 10
.B \-progress
report progress when building the BDDs for a network. This option
causes the name of each primary output or next state function to be
printed after its BDD is built. It does not take effect if local BDDs
are requested.
.TP 10
.B -p \fIn\fB
verbosity level. If negative, the program is very quiet. Larger values cause
more information to be printed.
.SH SEE ALSO
The documentation for the CUDD package explains the various
reordering methods.

The documentation for the MTR package provides details on the variable
groups.

dot(1)
.SH REFERENCES
F. Somenzi,
"Efficient Manipulation of Decision Diagrams,"
Software Tools for Technology Transfer,
vol. 3, no. 2, pp. 171-181, 2001.

S. Panda, F. Somenzi, and B. F. Plessier,
"Symmetry Detection and Dynamic Variable Ordering of Decision Diagrams,"
IEEE International Conference on Computer-Aided Design,
pp. 628-631, November 1994.

S. Panda and F. Somenzi,
"Who Are the Variables in Your Neighborhood,"
IEEE International Conference on Computer-Aided Design,
pp. 74-77, November 1995.

G. D. Hachtel and F. Somenzi,
"A Symbolic Algorithm for Maximum Flow in 0-1 Networks,"
IEEE International Conference on Computer-Aided Design,
pp. 403-406, November 1993.
.SH AUTHOR
Fabio Somenzi, University of Colorado at Boulder.