NANOTRAV

NAME

SYNOPSIS

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.  

OPTIONS

file

read input in blif format from file.

-f file

read options from file.

-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.

-depend

perform dependent variable analysis after traversal.

-from method

use method to choose the frontier states for image computation during traversal. Allowed methods are: new (default), reached, restrict, compact, squeeze, subset, superset.

-groupnsps method

use method to group the corresponding current and next state variables. Allowed methods are: none (default), default, fixed.

-image method

use method for image computation during traversal. Allowed methods are: mono (default), part, depend, and clip.

-depth n

use n to derive the clipping depth for image computation. It should be a number between 0 and 1. The default value is 1 (no clipping).

-verify file

perform combinational verification checking for equivalence to the network in file. 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.

-closure

perform reachability analysis using the transitive closure of the transition relation.

-cdepth n

use n 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).

-envelope

compute the greatest fixed point of the state transition relation. (This greatest fixed point is also called the outer envelope of the graph.)

-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.

-maxflow

compute the maximum flow in the network defined by the state graph.

-sink file

read the sink for maximum flow computation from file. The source is given by the initial states.

-shortpaths method

compute the distances between states. Allowed methods are: none (default), bellman, floyd, and square.

-selective

use selective tracing variant of the square method for shortest paths.

-part

compute the conjunctive decomposition of the transition relation. The network must be sequential for the test to take place.

-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.

-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.

-cover

print irredundant sums of products for the primary outputs. This option implies -zdd.

-second file

read a second network from file. 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.

-density

test BDD approximation functions.

-approx method

if method is under (default) perform underapproximation when BDDs are approximated. If method is over perform overapproximation when BDDs are approximated.

-threshold n

Use n as threshold when approximating BDDs.

-quality n

Use n (a floating point number) as quality factor when approximating BDDs. Default value is 1.

-decomp

test BDD decomposition functions.

-cofest

test cofactor estimation functions.

-clip n file

test clipping functions using n to determine the clipping depth and taking one operand from the network in file.

-dctest file

test functions for equality and containment under don't care conditions taking the don't care conditions from file.

-closest

test function that finds a cube in a BDD at minimum Hamming distance from another BDD.

-clauses

test function that extracts two-literal clauses from a DD.

-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.

-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.

-cache n

set the initial size of the computed table to n.

-slots n

set the initial size of each unique subtable to n.

-maxmem n

set the target maximum memory occupation to n MB. If this parameter is not specified or if n is 0, then a suitable value is computed automatically.

-memhard n

set the hard limit to memory occupation to n MB. If this parameter is not specified or if n is 0, no hard limit is enforced by the program.

-maxlive n

set the hard limit to the number of live BDD nodes to n. If this parameter is not specified, the limit is four billion nodes.

-dumpfile file

dump BDDs to file. The BDDs are dumped just before program termination. (Hence, after reordering, if reordering is specified.)

-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.

-dumpmv

use blif-MV format for dump of BDDs. The BDDs are dumped as a network of multiplexers.

-dumpdaVinci

use daVinci format for dump of BDDs.

-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.

-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.

-storefile file

Save the BDD of the reachable states to file. The BDD is stored at the iteration specified by -store. This option uses the format of the dddmp library. Together with -loadfile, 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.

-store n

Save the BDD of the reached states at iteration n. This option requires -storefile.

-loadfile file

Load the BDD of the initial states from file. This option uses the format of the dddmp library. Together with -storefile, it implements a primitive checkpointing capability.

-nobuild

do not build the BDDs. Quit after determining the initial variable order.

-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.

-delta

build BDDs only for the next state functions of a sequential circuit.

-node

build BDD only for node.

-order file

read the variable order from file. 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.

-ordering method

use method to derive an initial variable order. method can be one of hw, dfs. Method hw uses the order in which the inputs are listed in the circuit description.

-autodyn

enable dynamic reordering. By default, dynamic reordering is disabled. If enabled, the default method is sifting.

-first n

do first dynamic reordering when the BDDs reach n nodes. The default value is 4004. (Don't ask why.)

-countdead

include dead nodes in node count when deciding whether to reorder dynamically. By default, only live nodes are counted.

-growth n

maximum percentage by which the BDDs may grow while sifting one variable. The default value is 20.

-automethod method

use method for dynamic reordering of the BDDs. method can be one of none, random, pivot, sifting, converge, symm, cosymm, group, cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing, genetic, exact. The default method is sifting.

-reordering method

use method for the final reordering of the BDDs. method can be one of none, random, pivot, sifting, converge, symm, cosymm, group, cogroup, win2, win3, win4, win2conv, win3conv, win4conv, annealing, genetic, exact. The default method is none.

-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.

-groupcheck method

use method for the the creation of groups in group sifting. method 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.

-arcviolation n

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.

-symmviolation n

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.

-recomb n

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.

-tree file

read the variable group tree from file. The format of this file is a sequence of triplets: lb ub flag. Each triplet describes a group: lb is the lowest index of the group; ub is the highest index of the group; flag can be either D (default) or F (fixed). Fixed groups are not reordered.

-genepop n

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.

-genexover n

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.

-seed n

random number generator seed for the genetic algorithm and the random and pivot reordering methods.

-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.

-p n

verbosity level. If negative, the program is very quiet. Larger values cause more information to be printed.

SEE ALSO

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

dot(1)  

REFERENCES

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.  

AUTHOR