Is there another way to walk around problem "Node ** is not driven only by latches and constants?"

From: Li, Lun (lli_at_mail.smu.edu)
Date: Mon Jun 21 2004 - 13:55:51 MDT

Dear Sir/Madam,

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

Node ** found in the support of node ld_B.
 
Node ** is not driven only by latches and constants.

But, when I play with gcd.v given in the example, it seems that this formula works while start is input without latch.

(start=1 -> AX(AF(busy=0)));

The gcd code is from Fabio Somenzi in examples distributed with VIS. Is it a ransom case or something? I just want to find a way to walk around above latch input problem. I don't want to add latch in the code because It will add porblem for reachability analysis.

Thanks,

Leon

This archive was generated by hypermail 2.1.7 : Mon Jun 21 2004 - 14:40:01 MDT