回复:Re: your mail

From: 022021074_at_fudan.edu.cn
Date: Fri Mar 12 2004 - 06:04:40 MST


>Great !

I will look into VIS to verify your words.

if it works ,that will bring great convenience to my study!

thanks

----- 原邮件 -----

: Chao Wang <Wangc@Colorado.EDU>

日期: 星期五, 三月 12日, 2004 下午3:25

主题: Re: your mail

> A week has passed before an easy method is proposed; so, I will
> just
> describe my way of doing this -- you can use the BMC package in
> VIS (BMC -
> Bounded Model Checking), but you need to add some source code.
>
> A normal sequence of commands for BMC is
> read_blif xxx.blif
> flattern_hierarchy
> build_partition_maigs
> <--
> bounded_model_checking ... ltl_property
> After the first 3 steps, the circuit (in xxx.blif) has been read
> into VIS
> and translated into a so-called AND-INVERTER graph -- a circuit
> with only
> AND gates and INVERTERs. (I assume that's what you nt.)
>
> This AND-INVERTER graph is an internal data structure (check
> vis/src/baig,
> vis/src/maig, vis/src/ntmaig); therefore, you need to add some
> source
> code if you want the output in a file.
>
> BTW: There might be some existing tools that can do this.
>
> Chao
>
>
> On Wed, 3 Mar 2004 022021074@fudan.edu.cn wrote:
>
> >
> > Hi,folks,
> >
> > ??? I have benn working on sequential circuit for several
> months. The
> > iscas89 benchmarks are very popular in verification area.I
> download them
> > from internet,while the format is BLIF.you know, the relation
> between> variables is truth table,and only gives the ON set. Now,
> what I want is
> > another kind of format,in which the relation between variables
> is basic
> > gate type such as (N)AND,(N)OR,(N)XOR,NOT.
> >
> > ????Woule?you mind telling me? how to get them on internet,or which
> > tool?can ?converse BLIF in that kind of format,or whether you
> have the
> > code writting in C/C++ that can do this job ??
> >
> > ? Thanks,
> >
> > ?Huang Wei???
> >
> >
> >
>
> --
>
>

This archive was generated by hypermail 2.1.7 : Fri Mar 12 2004 - 06:23:51 MST