VIS-HELP (fwd)

From: K T Oommen Tharakan(99407703) (tharakan@ee.iitb.ernet.in)
Date: Mon Nov 13 2000 - 08:23:09 MST

  • Next message: Roderick Bloem: "Re: VIS-HELP (fwd)"

    ---------- Forwarded message ----------
    Date: Mon, 13 Nov 2000 16:49:00 +0530 (IST)
    From: "K T Oommen Tharakan(99407703)" <tharakan@bhairav.ee.iitb.ernet.in>
    To: vis@ic.eecs.berkeley.edu
    Subject: VIS-HELP

    ---------- Forwarded message ----------
    Date: Mon, 13 Nov 2000 16:42:45 +0530 (IST)
    From: "K T Oommen Tharakan(99407703)" <tharakan@bhairav.ee.iitb.ernet.in>
    To: vis@ic.eecs.berkeley.edu
    Subject: VIS

    Dear Sirs:

    My name is K T Oommen Tharakan. I am a research scholar in the Dept. of
    Electrical Engg. at Indian Institute of Technology, Bombay,INDIA. I would
    like to verify one of my circuits. I am trying VIS for the same.

    For verification, we have to write the properties of the circuit to be
    checked in CTL. My doubt is how we will be knowing the name of the
    variables whose proerties are to be checked, from the BLIF-MV description
    of the circuit.

    When compiled in vis, after comput_reach -v 1, the Reachability Analysis
    showed the following.

    ==========================================================================
    Reachibility Analysis Results.

    FSSM depth = 5
    Reachable States = 48
    BDD Size = 24
    Analysis time = 0.07
    reachability analysis =complete
    ==========================================================================

    KIndly let me know how to proceed with property writing. I have good
    background of temporal logics and CTL.

    Looking forward for help from you,

    With best regards,

    K T Oommen Tharakan

     



    This archive was generated by hypermail 2b29 : Mon Nov 13 2000 - 08:41:00 MST