Boosting Verification Scalability via Structural Grouping
and Semantic Partitioning of Properties
Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, and Kristin Yvonne Rozier
This webpage contains supplementary experimental data for "Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties" by R. Dureja, J. Baumgartner, A. Ivrii, R. Kanzelman, and K. Y. Rozier.
From equivalence checking to functional verification to design-space exploration, industrial verification tasks entail checking a large number of properties on the same design. State-of-the-art tools typically solve all properties concurrently, or one-at-a-time. They do not optimally exploit subproblem sharing between properties, leaving an opportunity to save considerable verification resource via concurrent verification of properties with nearly identical cone of influence (COI). These high-affinity properties can be concurrently solved; the verification effort expended for one can be directly reused to accelerate the verification of the others, without hurting per-property verification resources through bloating COI size. We present a near-linear runtime algorithm for partitioning properties into provably high- affinity groups for concurrent solution. We also present an effective method to partition high-structural-affinity groups using semantic feedback, to yield an optimal multi-property localization abstraction solution. Experiments demonstrate substantial end- to-end verification speedups through these techniques, leveraging parallel solution of individual groups.