|
Space vs Time Trade-off : Partitioned Transition Relation
Space vs Time Trade-off : Partitioned Transition Relation
- Behavior of the system described by a vector of next state functions (# of latches), and functions for intermediate variables : T1 , T2 , ... , Tn , I1 , I2 ..., Ik
- Some next state functions can be grouped together into components : (T1 , T2 ), (T3 ,T4 ,T5 ) ... (Tn , I1 , I2) .....
- Number of BDD nodes roughly increases with decrease in number of components
- Time taken to perform reachability analysis is a convex function of number of components
- Number of components can be controlled by the parameter “image_cluster_size”. Usage:
vis> set image_cluster_size 1000
- “print_img_info” command creates the clusters
|
