Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration

dc.contributor.author Dureja, Rohit
dc.contributor.author Baumgartner, Jason
dc.contributor.author Kanzelman, Robert
dc.contributor.author Williams, Mark
dc.contributor.author Rozier, Kristin
dc.contributor.author Rozier, Kristin Yvonne
dc.contributor.department Aerospace Engineering
dc.contributor.department Computer Science
dc.contributor.department Virtual Reality Applications Center
dc.contributor.department Electrical and Computer Engineering
dc.contributor.department Mathematics
dc.date 2020-12-29T05:44:08.000
dc.date.accessioned 2021-02-24T18:25:07Z
dc.date.available 2021-02-24T18:25:07Z
dc.date.copyright Wed Jan 01 00:00:00 UTC 2020
dc.date.embargo 2019-01-01
dc.date.issued 2020-12-22
dc.description.abstract <p>Industrial hardware verification tasks often require checking a large number of properties within a testbench. Verification tools often utilize parallelism in their solving orchestration to improve scalability, either in portfolio mode where different solver strategies run concurrently, or in partitioning mode where disjoint property subsets are verified independently. While most tools focus solely upon reducing end-to-end walltime, reducing overall CPU-time is a comparably-important goal influencing power consumption, competition for available machines, and IT costs. Portfolio approaches often degrade into highly-redundant work across processes, where similar strategies address properties in nearly-identical order. Partitioning should take property affinity into account, atomically verifying high-affinity properties to minimize redundant work of applying identical strategies on individual properties with nearly-identical logic cones. In this paper, we improve multi-property parallel verification with respect to both wall- and CPU-time. We extend affinity-based partitioning to guarantee complete utilization of available processes, with provable partition quality. We propose methods to minimize redundant computation, and dynamically optimize work distribution. We deploy our techniques in a sequential redundancy removal framework, using localization to solve non-inductive properties. Our techniques offer a median 2.4× speedup yielding 18.1% more property solves, as demonstrated by extensive experiments.</p>
dc.description.comments <p>This proceeding is published as Dureja, Rohit, Jason Baumgartner, Robert Kanzelman, Mark Williams, and Kristin Y. Rozier. "Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration." In <em>Proceedings of the 20th International Conference on Formal Methods in Computer Aided Design (</em>Strichman, O. and A. Ivrii, eds.) (2020): 16-25. DOI: <a href="https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_8" target="_blank">10.34727/2020/isbn.978-3-85448-042-6_8</a>. Posted with permission.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/aere_conf/84/
dc.identifier.articleid 1085
dc.identifier.contextkey 20852286
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath aere_conf/84
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/93020
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/aere_conf/84/2020_RozierKristin_AcceleratingParallel.pdf|||Sat Jan 15 02:11:17 UTC 2022
dc.source.uri 10.34727/2020/isbn.978-3-85448-042-6_8
dc.subject.disciplines Computer Sciences
dc.subject.disciplines Systems Engineering and Multidisciplinary Design Optimization
dc.subject.keywords Power demand
dc.subject.keywords Scalability
dc.subject.keywords Redundancy
dc.subject.keywords Tools
dc.subject.keywords Parallel processing
dc.subject.keywords Task analysis
dc.subject.keywords Portfolios
dc.title Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
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 dad3cd36-0f8b-49c3-b43f-1df139ae2068
relation.isOrgUnitOfPublication a75a044c-d11e-44cd-af4f-dab1d83339ff
relation.isOrgUnitOfPublication 82295b2b-0f85-4929-9659-075c93e82c48
File
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
2020_RozierKristin_AcceleratingParallel.pdf
Size:
551.8 KB
Format:
Adobe Portable Document Format
Description: