Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties

Thumbnail Image
Date
2019-11-11
Authors
Dureja, Rohit
Baumgartner, Jason
Ivrii, Alexander
Kanzelman, Robert
Rozier, Kristin
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Research Projects
Journal Issue
Series
Abstract

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.

Comments

This proceeding was published as Dureja, Rohit, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, and Kristin Y. Rozier. "Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties." In 2019 Formal Methods in Computer Aided Design (FMCAD), 2019. DOI: 10.23919/FMCAD.2019.8894265. Posted with permission.

Description
Keywords
Citation
DOI
Copyright
Tue Jan 01 00:00:00 UTC 2019