From: Fabio Somenzi (Fabio_at_colorado.edu)
Date: Mon Jun 21 2004 - 17:17:33 MDT
Leon,
"start" is a register of testGcd. Hence, it is not a primary input to
the model. BMC does not enforce the restriction that variables
appearing in properties should depend ultimately on registers, but the
BDD-based model checking algorithms do.
Fabio
>>>>> "LL" == Li, Lun <lli_at_mail.smu.edu> writes:
LL> Dear Sir/Madam,
LL> I read the vis FAQ and It is said that in the CTL formula, and input can not be put in the formular without latch, otherwise, it will cause problem like
LL> Node ** found in the support of node ld_B.
LL> Node ** is not driven only by latches and constants.
LL> But, when I play with gcd.v given in the example, it seems that
LL> this formula works while start is input without latch.
LL> (start=1 -> AX(AF(busy=0)));
LL> The gcd code is from Fabio Somenzi in examples distributed with
LL> VIS. Is it a ransom case or something? I just want to find a way
LL> to walk around above latch input problem. I don't want to add
LL> latch in the code because It will add porblem for reachability
LL> analysis.
LL> Thanks,
LL> Leon
This archive was generated by hypermail 2.1.7 : Mon Jun 21 2004 - 17:19:42 MDT