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

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

Research output: Contribution to journalArticleScientificpeer-review


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.
Original languageEnglish
JournalJournal on Satisfiability, Boolean Modeling and Computation
Pages (from-to)135-172
Publication statusPublished - 2016
Externally publishedYes
MoE publication typeA1 Journal article-refereed

Fields of Science

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

Cite this