Call for Model Checkers and Benchmarks HWMCC'14 CAV Edition
Armin Biere
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
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
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