Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks

Research output: Contribution to journalArticleScientificpeer-review

Researchers

  • Gianpiero Cabodi
  • Carmelo Loiacono
  • Marco Palena
  • Paolo Pasini
  • Denis Patti
  • Stefano Quer
  • Danilo Vendraminetto
  • Armin Biere
  • Keijo Heljanko

Research units

  • Polytechnic University of Turin
  • Johannes Kepler University of Linz

Abstract

Model checkers and sequential equivalence checkers have become essential tools for the semiconductor industry in recent years. The Hardware Model Checking Competition (HWMCC) was founded in 2006 with the purpose of intensifying research interest in these technologies, and establishing more of a science behind them. For example, the competition provided a standardized benchmark format, a challenging and diverse set of industrially- relevant public benchmarks, and, as a consequence, a significant motivation for additional research to advance the state-of-the-art in model checkers for these verification problems. This paper provides a historical perspective, and an analysis of the tools and benchmarks submitted to the competition. It also presents a detailed analysis of the results collected in the 2014 edition of the contest, showing relations among tools, and among tools and benchmarks. It finally proposes a list of considerations, lessons learned, and hints for both future organizers and competitors.

Details

Original languageEnglish
Pages (from-to)135-172
JournalJournal of Satisfiability, Boolean Modeling and Computation
Volume9
Publication statusPublished - 28 Jan 2016
MoE publication typeA1 Journal article-refereed

    Research areas

  • model checking, equivalence checking, binary decisions diagrams, satisfiability solvers, interpolation, IC3, property directed reachability

ID: 10327672