>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> Sir
vg> (1)For the FSM code below,taking "ald" as MSB, and bits
vg> for moorestate as LSB's
vg> [0,1,2,3,4,5,6,7] are the 8 states.
vg> please tell me what are the
vg> "reachable states set" and "unreachable states set".
They are all reachable. If you run "rch," it will tell you that there
are 8 reachable states. In general, however, vis does not report
which states are reachable; only how many. For large designs, listing
all reachable states is usually infeasible. For individual states,
one can use EF properties to determine whether they are reachable.
vg> (2)Please tell me the same for the counter code.
Again, all states are reachable.
vg> How does,skip of reachability analysis for proving the property
vg> "AG(clatched=1->AX(q[20:0]=0))" saves time?
For the counter, it doesn't.
vg> Also how does this case differs from the case which
vg> includes reachability analysis?
For the general explanation, refer to
http://vlsi.colorado.edu/~vis/vis-users/0139.html
In this case, reachability takes a long time, but in the end all
states are reachable. Hence, the effort put into reachability
analysis is wasted.
Fabio
This archive was generated by hypermail 2b30 : Wed Jun 06 2001 - 12:11:52 MDT