CNF Benchmark Suite: VLIW-UNSAT-4.0
========================================
Description: unsatisfiable formulas from formal verification of VLIW processors with instruction queues
and 9-stage pipelines; the processors implement advanced loads, predicated execution,
branch prediction, and exceptions
# of instances: 4
Author: Miroslav N. Velev (mvelev@ece.cmu.edu)
http://www.ece.cmu.edu/~mvelev
Date: October 24, 2003
CNF Formula Size [Bytes] Variables Clauses Literals Avg. Literals/Clause
---------------------------------------------------------------------------------------------------------
9vliw_m_9stages_C1.cnf 37200981 96177 1814189 5280501 2.910668
9vliw_m_9stages_iq1_C1.cnf 71310550 154309 3230738 9429252 2.918606
9vliw_m_9stages_iq2_C1.cnf 118501874 230662 5267084 15402036 2.924205
9vliw_m_9stages_iq3_C1.cnf 187076761 333336 8122058 23781172 2.927974
output of md5sum:
-------------------------------------------------------------------------------------------------
59166ee8132e6b3febc29df90fb207f2 9vliw_m_9stages_C1.cnf
026e3e8fb7fb7d06d1454149870c79b1 9vliw_m_9stages_iq1_C1.cnf
3ef35acac5ab20591292c0715cb27636 9vliw_m_9stages_iq2_C1.cnf
ccc997c36c54c2291e2a143cfc9dd2d3 9vliw_m_9stages_iq3_C1.cnf