[ Results |  Tables |  Logs |  Benchmarks |  Setup |  Submission |  Organization |  Previous Editions ]

HWMCC'17

Affiliated to FMCAD'17

Vienna, Austria, October 2 - 6, 2017

This was the 9th competitive event for hardware model checkers.

The slides for presenting the competition results at FMCAD'17:

[ Biere-HWMCC17-talk.pdf ]

There is a page written before the competition describing setup and history:

Armin Biere, Tom van Dijk, Keijo Heljanko.
Hardware Model Checking Competition 2017.
In Proc. 17th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'17),
page 9, IEEE 2017.
[ paper | bibtex ]

Results

In the SINGLE track the top three places are:

1. ABC (abcdsuperprove)
   Robert K. Brayton, Baruch Sterin, Alan Mishchenko (Univ. Berkeley)
2. PDTRAV (pdtravthrd)
   Gianpiero Cabodi et.al. (Politecnico di Torino)
3. AVY
   Yakir Vizel (Univ. Princeton), Arie Gurfinkel (Univ. Waterloo)

1. ABC (abcdeep)
   Robert K. Brayton, Baruch Sterin, Alan Mishchenko (Univ. Berkeley)
2. SHIFTBMC
   Norbert Manthey (hobbyist, former Post-Doc @ TU Dresden)
3. TRUSS
Ryan Berryhill ¹, Alexander Ivrii ², Neil Veira ¹, Andreas Veneris ^1
1 Univ. Toronto    ² IBM Research Haifa

1. ABC (abclive)
   Robert K. Brayton, Baruch Sterin, Alan Mishchenko (Univ. Berkeley)

Tables

Generated with zummarize.c from the following logs.

Logs

[ hwmcc17-live-logs.tar.xz | hwmcc17-single-logs.tar.xz ]

Benchmarks

[ hwmcc17-live-benchmarks.tar.xz | hwmcc17-single-benchmarks.tar.xz ]

Setup

The competition consisted of a single safety property track (SINGLE), a (single) liveness property track (LIVE), and a deep bound track (DEEP), but no multiple property track. The winner of the deep bound track received an award of $500 sponsored by Oski Technology.

The tracks were runnnin in the same way as in the previous four incarnations of the competition, except that we used our new cluster running Ubuntu 16.04.2 64 bit. Each cluster node had two Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz CPUs and 128 GB of main memory.

Each solver had full access to both processors on one node, thus combined 16 cores (32 virtual cores) and 128 GB of main memory. Accordingly a memory limit of 120GB was enforced. As in the previous competition in 2015 we further used a time limit of 1 hour of wall clock-time.

Also as before the number of submissions was restricted to at most two model checkers per submitter and model checkers were required to produce witnesses in the SINGLE track. These witnesses were checked by the AIGSIM tool, which is part of the AIGER tools.

Except for the new hardware, competition rules, as well as input and output formats did not change. Please consult the pages of previous competitions (see for instance HWMCC'12 or below) for more details.

Again as in 2014 and 2015, in order to avoid glitches in interpreting the format, the SINGLE track only used AIGER pre 1.9 single property benchmarks, with the single bad state property encoded as an output (MILOA header with O = 1). All latches were implicitly initialized to zero as it was the default in the pre 1.9 AIGER format.

There was no change in the LIVE track nor in the DEEP track. Solvers intended to participate in the DEEP track were run in the SINGLE track and were expected to print reached bounds as in previous years (see for instance HWMCC'12).

Submission

Email submission to "Armin Biere" <biere@jku.at>.

Registration and first versions of model checkers were due on September 7.

It was possible to send updates of model checkers until September 14.

New benchmarks were accepted by September 13 as well.

All submission dates were anywhere on earth.

Organization

HWMCC'17 was organized by

Armin Biere, Johannes Keplers University, Linz, Austria
Tom van Dijk, Johannes Keplers University, Linz, Austria
Keijo Heljanko, Aalto University, Finland

Previous Editions

HWMCC'15 at FMCAD'15, Austin, USA
HWMCC'14 at CAV'14, FLoC'14 Olympic Games, Vienna, Austria
HWMCC'13 at FMCAD'13, Portland, USA
HWMCC'12 at FMCAD'12, Cambridge, UK
HWMCC'11 at FMCAD'11, Austin, USA
HWMCC'10 at CAV'10, FloC'10, Edinburgh, UK
HWMCC'08 at CAV'08, Princeton, USA
HWMCC'07 at CAV'07, Berlin, Germany