From: Chao Wang (Wangc_at_colorado.edu)
Date: Fri Mar 12 2004 - 00:25:03 MST
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_at_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 - 00:26:29 MST