distr/nanotrav/README

   1 $Id: README,v 1.8 1997/01/23 07:33:22 fabio Exp fabio $
   2
   3 WHAT IS NANOTRAV
   4 ================
   5
   6 This directory contains nanotrav, a simple reachability analysis program
   7 based on the CUDD package. Nanotrav uses a very naive approach and is
   8 only included to provide a sanity check for the installation of the
   9 CUDD package.
  10
  11 Nanotrav reads a circuit written in a small subset of blif. This
  12 format is described in the comments in bnet.c. Nanotrav then creates
  13 BDDs for the primary outputs and the next state functions (if any) of
  14 the circuit.
  15
  16 If, passed the -trav option, nanotrav builds a BDD for the
  17 characteristic function of the transition relation of the graph. It then
  18 builds a BDD for the initial state(s), and performs reachability
  19 analysis.  Reachability analysys is performed with either the method
  20 known as "monolithic transition relation method," whose main virtue is
  21 simplicity, or with a unsophisticated partitioned transition relation
  22 method.
  23
  24 Once it has completed reachability analysis, nanotrav prints results and
  25 exits. The amount of information printed, as well as several other
  26 features are controlled by the options. For a complete list of the
  27 options, consult the man page. Here, we only mention that the options allow
  28 the user of nanotrav to select among different reordering options.
  29
  30 TEST CIRCUITS
  31 =============
  32
  33 Five test circuits are contained in this directory: C17.blif,
  34 C880.blif, s27.blif, mult32a.blif, and rcn25.blif. The first two are
  35 combinational, while the last three are sequential.  The results or
  36 running
  37
  38     nanotrav -p 1 -cover C17.blif > C17.out
  39     nanotrav -p 1 -ordering dfs -autodyn -automethod sifting -reordering sifting -drop C880.blif > C880.out
  40     nanotrav -p 1 -trav s27.blif > s27.out
  41     nanotrav -p 1 -autodyn -reordering sifting -trav mult32a.blif > mult32a.out
  42     nanotrav -p 1 -envelope rcn25.blif > rcn25.out
  43
  44 are also included.  They have been obtained on a 200 MHz P6-based
  45 machine with 128MB of memory. These tests can be run with the shell
  46 script tst.sh. Notice that rcn25 requires approximately 500 sec. All
  47 other tests run in a few seconds.