In this case, the solution is simple. Use:
mc -D 0 bc.ctl
Model checking will complete almost instantaneously.
The -D 0 option causes VIS to skip the reachability analysis step.
Reachability information is used to simplify the model checking
computation proper.
For a 20-bit counter, this analysis takes about a million
breadth-first search steps, and is quite inefficient. In many other
cases, reachability analysis is quite helpful; hence, it is performed
by default.
In general, if the "FSM depth" is very large, reachability may hinder
more than help. Counters typically have large depths. (Unless they
have a parallel load command, of course.) In general, however, it is
not easy to predict the FSM depth in advance, and furthermore
depth is not the only factor determining whether it's better to do
reachability analysis or not.
Using -D 3 provides a reasonable compromise, because reachability
analysis is performed in an approximate way, which is ususally much
less expensive than the exact one. In your example,
mc -D 3 bc.ctl
also completes almost instantaneously.
Fabio
>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> Sir
vg> For the following code,
vg> AG(clatched=1->AX(q[20:0]=255)); took 10 mins. for
vg> evaluation.
vg> i want to ask what are the ways(and how) VIS provides
vg> so that we can reduce time taken by a property for evaluation.How can we use readings shown by print commands or other commands for this purpose?
vg> thanking you
vg> vanessa
vg> *********************************************************
vg>module bc(ck,p,c,u,q);
vg> input ck,p,c,u;
vg> output[20:0]q;
vg> reg clatched,platched,ulatched;
vg> reg[20:0]counter;
vg> assign q = counter;
vg> initial
vg> begin
vg> counter = 0;
vg> clatched=0;platched=0;ulatched=0;
vg> end
vg> always @(posedge ck)
vg> begin
vg> clatched=c;platched=p;ulatched=u;
vg> end
vg> always @ (posedge ck)
vg> if(clatched) counter=0;
vg> else if(platched) counter=255;
vg> else if(ulatched)counter=counter+1;
vg> else counter= counter-1;
vg> endmodule
vg> _____________________________________________________
vg> Chat with your friends as soon as they come online. Get Rediff Bol at
vg> http://bol.rediff.com
This archive was generated by hypermail 2b30 : Mon May 28 2001 - 14:18:59 MDT