These are sequential miters generated for the experimental results
in the paper A. Mishchenko, S. Chatterjee, R. Brayton, N. Een,
"Improvements to Combinational Equivalence Checking" (IWLS 2006)
http://www.eecs.berkeley.edu/~alanmi/publications/2006/iwls06_cec.pdf

seq_miter_bench.zip (9Mb) are sequential miters generated by
    comparing original IWLS benchmarks (all initial states set to 0)
    with these benchmarks after FPGA mapping/retiming using ABC commands:
    read <input_file>; resyn2; sfpga; miter -c; write <output_file>

seq_miter_rwsat_bench.zip (8Mb) are above sequential miters 
    postprocessed by combinational synthesis using script "rwsat"

comb_miter_bench.zip (18Mb) are sequential miters unrolled for
    a given number of timeframes using the following commands:
    read <input_file>; resyn2; sfpga; miter -c; frames -i -F <num>; 
    orpos; write <output_file>

comb_miter_rwsat_bench.zip (12Mb) are sequential miters unrolled and
    postprocessed by combinational synthesis using script "rwsat"

Please note that these benchmarks come directly from a Windows computer. 
To run them on Unix, you may need to preprocess them by "dos2unix".


Alan Mishchenko

April 21, 2006