From: Aritra Hazra (aritrah_at_cse.iitkgp.ernet.in)
Date: Thu Jul 03 2008 - 02:59:17 MDT
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
bmc error: Could not find node corresponding to the
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
> 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,
MS Student & Research Consultant,
Department of Computer Science & Engineering,
Indian Institute of Technology, Kharagpur.
INDIA - 721302
This archive was generated by hypermail 2.1.7 : Thu Jul 03 2008 - 03:02:04 MDT