Model checkers were required to produce witnesses for single safety properties. These traces were checked by the AIGSIM tool, which is part of the AIGER tools.
Otherwise, the competition was run almost the same way as in the previous two years, except that more powerful hardware was used.
The competition was run on a cluster at Aalto University, with exclusive access to 32 nodes of 2x Six-Core AMD Opteron 2435 2.6GHz with at least 16 GB of RAM. This meant 12 cores for each solver per benchmark, memory limit around 15 GB and time limit of 900 seconds.
Beside the requirement to produces witnesses, rules, input and output format did not change. Please consult the pages of HWMCC'12 for more details. The Oski benchmarks from 2013 which contained uninitialized latches were reencoded to conform to the pre AIGER 1.9 format. All benchmarks only have zero initialized latches.
There were three real silver medals handed out to the winners at the FLoC'14 Olympic Games ceremony in the second week.
Thus it was decided to only have three tracks: the single safety, the liveness and the deep bound track. There was no multiple property track for the CAV edition. It was technically the most challenging one and we only got three medals to hand out.