Scalable Verification of Designs with Multiple Properties

EasyChair Preprint 1411

Abstract

Many industrial verification tasks entail checking a large number of properties on the same design. Formal verification techniques, such as model checking, can verify multiple properties concurrently, or sequentially one-at-a-time. State-of-the-art verification tools do not optimally exploit subproblem sharing between properties, leaving an opportunity to save considerable verification resources. A significant need therefore exists to develop efficient and scalable techniques that intelligently check multiple properties by utilizing implicit inter-property logical dependencies and subproblem sharing, and improve tool orchestration. We report on our investigation of the multi-property model checking problem, and discuss research results, and highlight future research directions.

Keyphrases: Clustering, Multiple Properties, design space, formal verification, incremental verification, model checking

@booklet{EasyChair:1411,
  author    = {Rohit Dureja and Kristin Yvonne Rozier},
  title     = {Scalable Verification of Designs with Multiple Properties},
  howpublished = {EasyChair Preprint 1411},
  year      = {EasyChair, 2019}}