Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering

Document Type

Conference Proceeding


2019 Formal Methods in Computer Aided Design (FMCAD)

Publication Version

Accepted Manuscript

Link to Published Version

Publication Date


Journal or Book Title

2019 Formal Methods in Computer Aided Design (FMCAD)



Conference Title

2019 Formal Methods in Computer Aided Design (FMCAD)

Conference Date

October 22-25, 2019


San Jose, CA


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.


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.



File Format


Published Version


Article Location