---------- 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