Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration

Thumbnail Image
Dureja, Rohit
Baumgartner, Jason
Kanzelman, Robert
Williams, Mark
Rozier, Kristin
Major Professor
Committee Member
Journal Title
Journal ISSN
Volume Title
Rozier, Kristin Yvonne
Associate Professor
Research Projects
Organizational Units
Organizational Unit
Organizational Unit
Organizational Unit
Organizational Unit
Organizational Unit
Welcome to the exciting world of mathematics at Iowa State University. From cracking codes to modeling the spread of diseases, our program offers something for everyone. With a wide range of courses and research opportunities, you will have the chance to delve deep into the world of mathematics and discover your own unique talents and interests. Whether you dream of working for a top tech company, teaching at a prestigious university, or pursuing cutting-edge research, join us and discover the limitless potential of mathematics at Iowa State University!
Journal Issue
Is Version Of
Aerospace EngineeringComputer ScienceVirtual Reality Applications CenterElectrical and Computer EngineeringMathematics

Industrial hardware verification tasks often require checking a large number of properties within a testbench. Verification tools often utilize parallelism in their solving orchestration 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 walltime, 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. In this paper, 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 a median 2.4× speedup yielding 18.1% more property solves, as demonstrated by extensive experiments.


This proceeding is published as Dureja, Rohit, Jason Baumgartner, Robert Kanzelman, Mark Williams, and Kristin Y. Rozier. "Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration." In Proceedings of the 20th International Conference on Formal Methods in Computer Aided Design (Strichman, O. and A. Ivrii, eds.) (2020): 16-25. DOI: 10.34727/2020/isbn.978-3-85448-042-6_8. Posted with permission.

Wed Jan 01 00:00:00 UTC 2020