VIS Error in doing BMC of LTL Formula... Help !!

From: Aritra Hazra (aritrah_at_cse.iitkgp.ernet.in)
Date: Thu Jul 03 2008 - 02:59:17 MDT

• Next message: hmf_at_inescporto.pt: "CuDD: subsets and equivalence + compile error"
• Previous message: Aritra Hazra: "Fw: Help !! VIS Error !! The hierarchy manager is empty. Read in design."
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

Hello !!

I am encountering an error while attempting to use VIS for
bounded model checking of some LTL formulas.

The LTL formula "G(F(CKT.G17=0))" is correctly verified
using bmc whereas "G(CKT.G17=0)" gives the following
error:
"Formula: G(CKT.G17=0)
 bmc error: Could not find node corresponding to the
 name CKT.G17"

In my attachment, the verilog design file is "s27.v". The
file containing correct LTL formula is "s27_correct.ltl" and
the file containing wrong LTL formula is "s27_wrong.ltl".

The steps in VIS that I have followed are as follows:
> read_verilog s27.v
> init_verify
> build_partition_maigs
> bmc -k 100 s27_correct.ltl / s27_wrong.ltl

Kindly help me regarding this and suggest how I can get rid
of this error.

Thanking you for your time,
-----
Aritra Hazra.
MS Student & Research Consultant,
Department of Computer Science & Engineering,
Indian Institute of Technology, Kharagpur.
INDIA - 721302

• application/octet-stream attachment: s27_wrong.ltl

• application/octet-stream attachment: s27.v

• application/octet-stream attachment: s27_correct.ltl

• Next message: hmf_at_inescporto.pt: "CuDD: subsets and equivalence + compile error"
• Previous message: Aritra Hazra: "Fw: Help !! VIS Error !! The hierarchy manager is empty. Read in design."
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2.1.7 : Thu Jul 03 2008 - 03:02:04 MDT