Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties Dureja, Rohit Baumgartner, Jason Ivrii, Alexander Kanzelman, Robert Rozier, Kristin Yvonne Rozier, Kristin
dc.contributor.department Aerospace Engineering
dc.contributor.department Computer Science
dc.contributor.department Electrical and Computer Engineering 2020-02-14T21:56:13.000 2020-06-29T22:45:06Z 2020-06-29T22:45:06Z Tue Jan 01 00:00:00 UTC 2019 2018-01-01 2019-11-11
dc.description.abstract <p>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.</p>
dc.description.comments <p>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 <em>2019 Formal Methods in Computer Aided Design (FMCAD)</em>, 2019. DOI: <a href="" target="_blank">10.23919/FMCAD.2019.8894265</a>. Posted with permission.</p>
dc.format.mimetype application/pdf
dc.identifier archive/
dc.identifier.articleid 1048
dc.identifier.contextkey 16540504
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath aere_conf/49
dc.language.iso en
dc.source.bitstream archive/|||Sat Jan 15 00:29:49 UTC 2022
dc.source.uri 10.23919/FMCAD.2019.8894265
dc.subject.disciplines Aerospace Engineering
dc.subject.disciplines Computer Sciences
dc.subject.disciplines Electrical and Computer Engineering
dc.subject.keywords Logic gates
dc.subject.keywords Hamming distance
dc.subject.keywords Registers
dc.subject.keywords Partitioning algorithms
dc.subject.keywords Runtime
dc.subject.keywords Scalability
dc.subject.keywords Task analysis
dc.title Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
dc.type article
dc.type.genre conference
dspace.entity.type Publication
relation.isAuthorOfPublication 3c555e5b-8fd1-4c38-98c6-6a2449fab7cf
relation.isOrgUnitOfPublication 047b23ca-7bd7-4194-b084-c4181d33d95d
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
relation.isOrgUnitOfPublication a75a044c-d11e-44cd-af4f-dab1d83339ff
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
322.36 KB
Adobe Portable Document Format