Re: vis automata-based approach to model checking

From: Chao Wang (wangc@synopsys.com)
Date: Thu May 31 2001 - 10:20:08 MDT

  • Next message: Roderick Bloem: "Re: vis automata-based approach to model checking"

    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:07:00 MDT