About backward reachable analysis

From: Zhao, Yang (zhaoyang_at_ict.ac.cn)
Date: Sun May 06 2007 - 04:26:05 MDT


Hello,

My question is about how to use VIS to compute all the states from which the circuit can final reach the given initial state. Or, it can be considered as a backward reachable analysis. I use the commands like these£º
init_verify
print_img_info -b
compute_reach

Does it gives the correct results?

Thank you very much!

Yang
                                 
--------------
Zhao, Yang
Key Laboratory of Computer System and Architecture,
Institution of Computing Technology,
Chinese Academy of Sciences.
2007-05-06



This archive was generated by hypermail 2.1.7 : Sun May 06 2007 - 04:30:50 MDT