I would just like to add that Fabio is planning to release a new version
of wring soon. It will be able to output verilog.
Roderick.
Chao Wang wrote:
>
> Hi, Fang:
>
> Currently VIS support CTL property (the model_check command) and partially
> support LTL property (the lang_empty). In order to do LTL model checking,
> the user need to translate the LTL formulae into Buechi automaton then to a
> Verilog monitor. The Verilog monitor is then composed with the design, and
> the language emptiness checking command can be used to check if there is a
> fair cycle.
>
> Fabio have a Perl script called "Wring", which can do the LTL->Buechi
> automaton translation. The Link is, http://vlsi.colorado.edu/~fabio/
>
> Hopefully, the entire LTL-based or CTL*-based approach could appear in the
> next release.
>
> Chao
>
> At 11:39 AM 5/31/01 -0400, you wrote:
> >Hi,
> >
> >I am very interesting in VIS. I have following three question. Thanks
> >for your reply.
> >
> >1)Are automata-based approach used in VIS.
> >2)Which logic formular are used to represent the property in this
> >automata-based approach.
> >
> >3)Need to build the product of the automata for the process and proeprty
> >to do the check.
> >
> >Thanks very much.
> >
> >Fang
> >
> >
This archive was generated by hypermail 2b30 : Thu May 31 2001 - 10:22:13 MDT