Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams and Kristin Yvonne Rozier
This webpage contains supplementary experimental data for "Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration" by R. Dureja, J. Baumgartner, R. Kanzelman, M. Williams, and K. Y. Rozier.
Industrial hardware verification tasks often require checking a large number of properties within a testbench. Verification tools often utilize parallelism to improve scalability, either in portfolio mode where different solver strategies run concurrently, or in partitioning mode where disjoint property subsets are verified independently. While most tools focus solely upon reducing end-to-end wall-time, reducing overall CPU-time is a comparably-important goal influencing power consumption, competition for available machines, and IT costs. Portfolio approaches often degrade into highly-redundant work across processes, where similar strategies address properties in nearly-identical order. Partitioning should take property affinity into account, atomically verifying high-affinity properties to minimize redundant work of applying identical strategies on individual properties with nearly-identical logic cones. We improve multi-property parallel verification with respect to both wall- and CPU-time. We extend affinity-based partitioning to guarantee complete utilization of available processes, with provable partition quality. We propose methods to minimize redundant computation, and dynamically optimize work distribution. We deploy our techniques in a sequential redundancy removal framework, using localization to solve non-inductive properties. Our techniques offer up to 3× speedup as demonstrated by extensive experiments.