Call for Model Checkers and Benchmarks HWMCC'14 CAV Edition

60 views
Skip to first unread message

Armin Biere

unread,
May 2, 2014, 9:17:17 AM5/2/14
to hw...@googlegroups.com
HWMCC'14 CAV Edition

http://fmv.jku.at/hwmcc14cav/

Affiliated to CAV'14 and
FLoC Olympic Games Vienna,
Austria, July 18-22, 2014


DATES

First version of model checkers due June 1.

Updates of model checkers possible until June 15.


PREVIOUS EDITIONS

HWMCC'13, HWMCC'12, HWMCC'11, HWMCC'10, HWMCC'08, and HWMCC'07.

This is the 7th competitive event for hardware model checkers.


SETUP

Model checkers are required to produce witnesses for single safety
properties. These traces will be checked by the AIGSIM tool, which is
part of the AIGER tools.

Otherwise, the competition is going to be run almost the same way as the
last two years, except that we also plan to use more powerful hardware
(more cores and memory). For now assume that you will have at least the
resources of last year (900 seconds time limit, four cores, 7 GB).

Beside the requirement to produces witnesses, rules, input and output
format did not change. Please consult the pages of HWMCC'12 for more
details.

There will be three real silver medals handed out for the winners at
the FLoC Olympic Games cerenomy in the second week.

Thus we decided to only have three tracks this year, the single safety,
the liveness and the deep bound track. We will not have a multiple
property track for the CAV edition. It is technically the most challenging
one and we only got three medals to hand out. 


SUBMISSION

As in previous years benchmarks and model checkers should be submitted
directly to the organizers (bi...@jku.at). First versions of model
checkers are due on June 1 and can be updated until June 15. Benchmarks
can be submitted anytime.


ORGANIZATION

HWMCC'13 is organized by Armin Biere, JKU Austria, and Keijo Heljanko,
Aalto University Finland.


SPONSORS

We are grateful to Oski Technology again sponsoring the deep bound
track award.

The winner of the deep bound track will get a medal and a check.

The organizers are also partially sponsored by RiSE.

Armin Biere

unread,
May 5, 2014, 4:40:31 AM5/5/14
to hw...@googlegroups.com

There is an update on the HW:

We plan to run the competition on a cluster at Aalto University. We will have exclusive access to 32 nodes of 2x Six-Core AMD Opteron 2435 2.6GHz with at least 16 GB of RAM. This would mean 12 cores for each solver per benchmark, memory limit around 15 GB and time limit of 900 seconds. As fall back we have the cluster at JKU with the same characteristics as in the last years.

Armin Biere

unread,
May 20, 2014, 4:36:32 PM5/20/14
to hw...@googlegroups.com
Another update related to an issue spotted by Zyad Hassan.

Thanks Zyad!

It turns out that the Oski benchmarks submitted and used last year contained uinitialized latches, which would not be supported by pre-AIGER 1.9 format as officially used in the single track. They did have the bad state constraint as output though, which makes them kind of mixed format benchmarks.

In order to only incrementally change what was said before and still being able to use these benchmarks in principle (again), we thus would want to make the following change to the expected input format for the single and deep bound track (liveness is not affected since it will  use the 1.9 format anyhow as already the last two years):

Beside the requirement to produces witnesses, rules, input and output format did not change. Please consult the pages of HWMCC'12 for more details. There is one exception though. We want to reuse the new Oski benchmarks submitted and used in 2013. But those have uninitialized latches. Thus you should assume pre AIGER 1.9 format but should be able to handle latches. If you are not able to support this feature let us know. There is also a new version of the AIGSIM tool available in the new release aiger-1.9.9.tar.gz which works more smoothly in this context, particularly when using bad state constraints as outputs.

This previous paragraph is an excerpt of the competition home page.  So please be prepared to see uninitialized latches in the single and deep bound track. If you can not support this feature let us know as soon as possible. Note, that already for those discussed benchmarks we replaced 1 initialized by 0 initialized latches. Thus even though it is not a big deal to implement 1 initialized latches (if you have already 0 initialized and non-initialized), we will not use 1 initialized latches in the single and deep bound track.

Finally the 'aigreset' tool can be used to change or check initialization (the latter with the '-c' option), e.g.

$ aigreset -c oski1rub04.aig
*** [aigreset] latch 51 literal 22994 uninitialized


Armin

Armin Biere

unread,
May 22, 2014, 6:21:44 AM5/22/14
to hw...@googlegroups.com
Find attached four trivial test benchmarks (two sat and two unsat).
If your model checker assumes latches to be initialized to false they
probably will all remain unsat.

Armin
noinit.zip
Reply all
Reply to author
Forward
0 new messages