|
Space vs Time Trade-off : Partitioning the Circuit
Space vs Time Trade-off : Partitioning the Circuit
- In some cases sizes of next state functions get too large
- BDD size can be controlled by partitioning the circuit and introducing intermediate variables to represent the partition.
- Number of BDD nodes decrease with increase in partition
- Reachability analysis time increases with increase in number of partitions
- Usage: vis> build_partition_mdds frontier
- Number of partitions is controlled by the parameter “partition_threshold” (size of the BDD at which new partition is created)
- Creates the BDDs for next state functions and intermediate variables : T1 , T2 , ... , Tn , I1 , I2 ..., Ik
|
