CNF Benchmark Suite: VLIW-SAT-4.0
========================================
Description: satisfiable formulas from formal verification of buggy VLIW processors with instruction queues
and 9-stage pipelines; the processors implement advanced loads, predicated execution,
branch prediction, and exceptions
# of instances: 10
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_iq3_C1_bug1.cnf 314723803 521188 13378641 39204979 2.930416
9vliw_m_9stages_iq3_C1_bug2.cnf 314721111 521158 13378532 39204686 2.930418
9vliw_m_9stages_iq3_C1_bug3.cnf 314662761 521046 13376161 39197797 2.930422
9vliw_m_9stages_iq3_C1_bug4.cnf 314000013 520721 13348117 39114325 2.930325
9vliw_m_9stages_iq3_C1_bug5.cnf 314757003 520770 13380350 39210884 2.930483
9vliw_m_9stages_iq3_C1_bug6.cnf 314726828 521192 13378781 39205391 2.930416
9vliw_m_9stages_iq3_C1_bug7.cnf 314707245 521147 13378010 39203144 2.930417
9vliw_m_9stages_iq3_C1_bug8.cnf 314722831 521179 13378617 39204907 2.930416
9vliw_m_9stages_iq3_C1_bug9.cnf 314722868 521187 13378624 39204898 2.930413
9vliw_m_9stages_iq3_C1_bug10.cnf 314723037 521182 13378625 39204931 2.930416
output of md5sum:
-------------------------------------------------------------------------------------------------
1911de49ec477d3e34b9a95eb8bf0845 9vliw_m_9stages_iq3_C1_bug1.cnf
de190892801b59cd9842bfb52b694299 9vliw_m_9stages_iq3_C1_bug2.cnf
dc050785d671b86f856b07b158553686 9vliw_m_9stages_iq3_C1_bug3.cnf
c9a9723a58c9cb8a0b55a82eb452ac90 9vliw_m_9stages_iq3_C1_bug4.cnf
c77a56af24208a6401c763e11a38de01 9vliw_m_9stages_iq3_C1_bug5.cnf
abc624ca713aad9563ab3886d918a526 9vliw_m_9stages_iq3_C1_bug6.cnf
6dcc1a7a687db45349fbaf9870c73e4b 9vliw_m_9stages_iq3_C1_bug7.cnf
5fe5b52b05e512edbe82e7d139ac7362 9vliw_m_9stages_iq3_C1_bug8.cnf
838f83d2fc04e408a3e66700f0dc0173 9vliw_m_9stages_iq3_C1_bug9.cnf
b96b75461795057ef2d559ebb6ae2ba1 9vliw_m_9stages_iq3_C1_bug10.cnf