遺伝学・遺伝統計学関連の姉妹ブログ『ryamadaの遺伝学・遺伝統計学メモ』
京都大学大学院医学研究科ゲノム医学センター統計遺伝学分野のWiki
講義・スライド
医学生物学と数学とプログラミングの三重学習を狙う学習ツール
駆け足で読む○○シリーズ
ぱらぱらめくるシリーズ
カシオの計算機
オンライン整数列大辞典

nanotrav

CUDD
  • 前の記事でCUDDの実行確認をしてみた。そこではnanotrav.exeを動かして、hoge.blif ファイルを読んでいる
  • nanotrav,blifってなに？
  • blifフォーマットはこちらにあるように"logic-level hierarchical circuit in textual form"なのだという
  • nanotravについてこちらからべたコピーしたのが以下

WHAT IS NANOTRAV
================

This directory contains nanotrav, a simple reachability analysis program
based on the CUDD package. Nanotrav uses a very naive approach and is
only included to provide a sanity check for the installation of the
CUDD package.

Nanotrav reads a circuit written in a small subset of blif. This
format is described in the comments in bnet.c. Nanotrav then creates
BDDs for the primary outputs and the next state functions (if any) of
the circuit.

If, passed the -trav option, nanotrav builds a BDD for the
characteristic function of the transition relation of the graph. It then
builds a BDD for the initial state(s), and performs reachability
analysis. Reachability analysys is performed with either the method
known as "monolithic transition relation method," whose main virtue is
simplicity, or with a unsophisticated partitioned transition relation
method.

Once it has completed reachability analysis, nanotrav prints results and
exits. The amount of information printed, as well as several other
features are controlled by the options. For a complete list of the
options, consult the man page. Here, we only mention that the options allow
the user of nanotrav to select among different reordering options.

TEST CIRCUITS
=============

Five test circuits are contained in this directory: C17.blif,
C880.blif, s27.blif, mult32a.blif, and rcn25.blif. The first two are
combinational, while the last three are sequential. The results or
running

nanotrav -p 1 -cover C17.blif > C17.out
nanotrav -p 1 -ordering dfs -autodyn -automethod sifting -reordering sifting -drop C880.blif > C880.out
nanotrav -p 1 -trav s27.blif > s27.out
nanotrav -p 1 -autodyn -reordering sifting -trav mult32a.blif > mult32a.out
nanotrav -p 1 -envelope rcn25.blif > rcn25.out

are also included. They have been obtained on a 200 MHz P6-based
machine with 128MB of memory. These tests can be run with the shell
script tst.sh. Notice that rcn25 requires approximately 500 sec. All
other tests run in a few seconds.
|