Skip to main content
Presentation
Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
2019 Formal Methods in Computer Aided Design (FMCAD)
  • Rohit Dureja, Iowa State University
  • Jason Baumgartner, IBM Corporation
  • Alexander Ivrii, IBM Corporation
  • Robert Kanzelman, IBM Corporation
  • Kristin Y. Rozier, Iowa State University
Document Type
Conference Proceeding
Conference
2019 Formal Methods in Computer Aided Design (FMCAD)
Publication Version
Accepted Manuscript
Link to Published Version
https://doi.org/10.23919/FMCAD.2019.8894265
Publication Date
11-11-2019
DOI
10.23919/FMCAD.2019.8894265
Conference Title
2019 Formal Methods in Computer Aided Design (FMCAD)
Conference Date
October 22-25, 2019
Geolocation
(37.3382082, -121.88632860000001)
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.

Copyright Owner
The Authors and FMCAD, Inc.
Language
en
File Format
application/pdf
Citation Information
Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, et al.. "Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties" San Jose, CA2019 Formal Methods in Computer Aided Design (FMCAD) (2019)
Available at: http://works.bepress.com/kristin-yvonne-rozier/38/