Hi,
assuming you are starting with verilog, I would suggest you look at the
examples that come with vis. some of them (e.g. abp) come with the
verilog file, and you can do some easy patern matching to find out the
system. Basically, you can use the verilog name of the variable. If
you have more than one level of modules, you should prefix variable name
with the path to it, as if it is a file name in a file system, but using
. instead of /. Bits in a register are written reg<0>, reg<1>, etc.
Arrays are written array<*0*> etc.
When in doubt, try "sim -n1". It will simulate the circuit and in the
process print all latch names.
Let us know if you have any more questions.
Roderick.
"K T Oommen Tharakan(99407703)" wrote:
> 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
>
>
_________________________________________________________
Do You Yahoo!?
Get your free @yahoo.com address at http://mail.yahoo.com
This archive was generated by hypermail 2b29 : Tue Nov 14 2000 - 20:19:19 MST