Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering

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

Journal or Book Title

2019 Formal Methods in Computer Aided Design (FMCAD)

DOI

10.23919/FMCAD.2019.8894265

Conference Title

2019 Formal Methods in Computer Aided Design (FMCAD)

Conference Date

October 22-25, 2019

City

San Jose, CA

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

Published Version

Share

Article Location

 
COinS