Announcing an extension of VIS model checking to CTL with past + timing

From: Paritosh Pandya (pandya@tcs.tifr.res.in)
Date: Thu Dec 07 2000 - 22:57:49 MST

  • Next message: ¾öÅÂÈ: "ever9@hanmail.net"

    Hi,

    We have recently built on top of VIS a model checker called CTLDC.
    An experimental preliminary implementation (linux binaries) is available
    for download.
    I would be happy to have comments/feedback.

    CTLDC checks Verilog designs against an extended logic CTL[DC].
    CTL[DC] extends CTL with
      -- past time properties
      -- timing properties.
    For example the formula
      AG #[] ([[req]] && slen >= 20 => scount ack >=3) #
    states that in any fragment of execution of length 20 or more if req is
    continuously high, then there must be at least 3 ack.

    Examples from VIS technology transfer course
    which are stated to be hard to formulate in CTL can now be handled.
    http://www.tcs.tifr.res.in/~pandya/dccheck/demo/sample.html

    Overview:
    http://www.tcs.tifr.res.in/~pandya/dccheck/demo/overview.html

    A motivating example: http://www.tcs.tifr.res.in/~pandya/dccheck/arbiter/arbquest.html

    CTLDC works by reducing model checking problem M |= R to M' |= R'
    where R is CTLDC formula but R' is pure CTL formula. Note that model
    M is transformed to M' in a way that preserves counter-examples and fairness.
    The actual model checking M'|=R' is still done by VIS.

    Thus CTLDC is not a new model checker. It extends the functionality of
    VIS to a richer (and we believe useful) logic CTLDC.

    Paritosh Pandya

    This archive was generated by hypermail 2b29 : Thu Dec 07 2000 - 22:53:40 MST