glift: Add examples, including a number of benchmarks used in some academic works.

1 files changed, 345 insertions, 0 deletions

diff --git a/examples/smtbmc/glift/too_large.v b/examples/smtbmc/glift/too_large.v
new file mode 100755
index 000000000..67605cc34
--- /dev/null
+++ b/examples/smtbmc/glift/too_large.v
@@ -0,0 +1,345 @@
+module too_large_lev2(pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09, 
+	pi10, pi11, pi12, pi13, pi14, pi15, pi16, pi17, pi18, pi19, 
+	pi20, pi21, pi22, pi23, pi24, pi25, pi26, pi27, pi28, pi29, 
+	pi30, pi31, pi32, pi33, pi34, pi35, pi36, pi37, po0, po1, 
+	po2);
+
+input pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09, 
+	pi10, pi11, pi12, pi13, pi14, pi15, pi16, pi17, pi18, pi19, 
+	pi20, pi21, pi22, pi23, pi24, pi25, pi26, pi27, pi28, pi29, 
+	pi30, pi31, pi32, pi33, pi34, pi35, pi36, pi37;
+
+output po0, po1, po2;
+
+wire n280, n281, n282, n283, n284, n285, n286, n287, n288, n289, 
+	n290, n291, n292, n293, n294, n295, n296, n297, n298, n299, 
+	n300, n301, n302, n303, n304, n305, n306, n307, n308, n309, 
+	n310, n311, n312, n313, n314, n315, n316, n317, n318, n319, 
+	n320, n321, n322, n323, n324, n325, n326, n327, n328, n329, 
+	n330, n331, n332, n333, n334, n335, n336, n337, n338, n339, 
+	n340, n341, n342, n343, n344, n345, n346, n347, n348, n349, 
+	n350, n351, n352, n353, n354, n355, n356, n357, n358, n359, 
+	n360, n361, n362, n363, n364, n365, n366, n367, n368, n369, 
+	n370, n371, n372, n373, n374, n375, n376, n377, n378, n379, 
+	n380, n381, n382, n383, n384, n385, n386, n387, n388, n389, 
+	n390, n391, n392, n393, n394, n395, n396, n397, n398, n399, 
+	n400, n401, n402, n403, n404, n405, n406, n407, n408, n409, 
+	n410, n411, n412, n413, n414, n415, n416, n417, n418, n419, 
+	n420, n421, n422, n423, n424, n425, n426, n427, n428, n429, 
+	n430, n431, n432, n433, n434, n435, n436, n437, n438, n439, 
+	n440, n441, n442, n443, n444, n445, n446, n447, n448, n449, 
+	n450, n451, n452, n453, n454, n455, n456, n457, n458, n459, 
+	n460, n461, n462, n463, n464, n465, n466, n467, n468, n469, 
+	n470, n471, n472, n473, n474, n475, n476, n477, n478, n479, 
+	n480, n481, n482, n483, n484, n485, n486, n487, n488, n489, 
+	n490, n491, n492, n493, n494, n495, n496, n497, n498, n499, 
+	n500, n501, n502, n503, n504, n505, n506, n507, n508, n509, 
+	n510, n511, n512, n513, n514, n515, n516, n517, n518, n519, 
+	n520, n521, n522, n523, n524, n525, n526, n527, n528, n529, 
+	n530, n531, n532, n533, n534, n535, n536, n537, n538, n539, 
+	n540, n541, n542, n543, n544, n545, n546, n547, n548, n549, 
+	n550, n551, n552, n553, n554, n555, n556;
+
+  AN2 U283 ( .A(n280), .B(n281), .Z(po2));
+  OR2 U284 ( .A(n282), .B(n283), .Z(n280));
+  OR2 U285 ( .A(n284), .B(n285), .Z(n283));
+  AN2 U286 ( .A(n286), .B(n287), .Z(n285));
+  OR2 U287 ( .A(n288), .B(n289), .Z(n287));
+  OR2 U288 ( .A(n290), .B(n291), .Z(n289));
+  AN2 U289 ( .A(pi29), .B(n292), .Z(n291));
+  AN2 U290 ( .A(n293), .B(pi35), .Z(n290));
+  AN2 U291 ( .A(n294), .B(n295), .Z(n293));
+  OR2 U292 ( .A(pi29), .B(n296), .Z(n294));
+  AN2 U293 ( .A(n297), .B(pi18), .Z(n284));
+  AN2 U294 ( .A(n298), .B(n299), .Z(n297));
+  IV2 U295 ( .A(n300), .Z(n299));
+  OR2 U296 ( .A(n301), .B(n302), .Z(n298));
+  AN2 U297 ( .A(n303), .B(n304), .Z(n302));
+  OR2 U298 ( .A(n305), .B(n306), .Z(n304));
+  AN2 U299 ( .A(n307), .B(n308), .Z(n306));
+  AN2 U300 ( .A(n309), .B(n310), .Z(n305));
+  OR2 U301 ( .A(n311), .B(n312), .Z(n310));
+  AN2 U302 ( .A(n308), .B(n313), .Z(n312));
+  OR2 U303 ( .A(n314), .B(n315), .Z(n308));
+  AN2 U304 ( .A(n316), .B(n317), .Z(n311));
+  AN2 U305 ( .A(n318), .B(n319), .Z(n317));
+  AN2 U306 ( .A(pi15), .B(n315), .Z(n316));
+  OR2 U307 ( .A(n320), .B(n321), .Z(n315));
+  AN2 U308 ( .A(n322), .B(n323), .Z(n309));
+  OR2 U309 ( .A(n324), .B(n325), .Z(n322));
+  AN2 U310 ( .A(n326), .B(n327), .Z(n301));
+  OR2 U311 ( .A(n328), .B(n307), .Z(n327));
+  AN2 U312 ( .A(n329), .B(n323), .Z(n328));
+  OR2 U313 ( .A(n330), .B(n331), .Z(n329));
+  AN2 U314 ( .A(n332), .B(n313), .Z(n331));
+  OR2 U315 ( .A(n333), .B(n325), .Z(n332));
+  AN2 U316 ( .A(n324), .B(n334), .Z(n333));
+  IV2 U317 ( .A(n335), .Z(n334));
+  AN2 U318 ( .A(n336), .B(pi08), .Z(n335));
+  OR2 U319 ( .A(n320), .B(n314), .Z(n336));
+  AN2 U320 ( .A(n337), .B(n338), .Z(n314));
+  OR2 U321 ( .A(pi20), .B(n339), .Z(n337));
+  AN2 U322 ( .A(n340), .B(n341), .Z(n330));
+  AN2 U323 ( .A(n342), .B(n319), .Z(n341));
+  OR2 U324 ( .A(n343), .B(n325), .Z(n342));
+  AN2 U325 ( .A(n324), .B(n344), .Z(n343));
+  IV2 U326 ( .A(n345), .Z(n344));
+  AN2 U327 ( .A(n346), .B(n295), .Z(n324));
+  AN2 U328 ( .A(pi15), .B(n318), .Z(n340));
+  OR2 U329 ( .A(n347), .B(n348), .Z(n318));
+  AN2 U330 ( .A(n349), .B(n350), .Z(n347));
+  AN2 U331 ( .A(n351), .B(n352), .Z(n326));
+  OR2 U332 ( .A(n353), .B(n354), .Z(n282));
+  AN2 U333 ( .A(n355), .B(n356), .Z(n354));
+  AN2 U334 ( .A(n357), .B(n358), .Z(n355));
+  OR2 U335 ( .A(pi26), .B(pi27), .Z(n357));
+  AN2 U336 ( .A(n359), .B(n360), .Z(n353));
+  OR2 U337 ( .A(n361), .B(n362), .Z(n360));
+  AN2 U338 ( .A(n288), .B(n363), .Z(n362));
+  OR2 U339 ( .A(n364), .B(n365), .Z(n288));
+  AN2 U340 ( .A(n292), .B(n296), .Z(n364));
+  OR2 U341 ( .A(n366), .B(n367), .Z(n296));
+  IV2 U342 ( .A(n368), .Z(n367));
+  AN2 U343 ( .A(n369), .B(n370), .Z(n368));
+  OR2 U344 ( .A(pi33), .B(pi22), .Z(n366));
+  AN2 U345 ( .A(pi29), .B(n371), .Z(n361));
+  OR2 U346 ( .A(n372), .B(n373), .Z(n371));
+  AN2 U347 ( .A(n374), .B(n292), .Z(n372));
+  IV2 U348 ( .A(n356), .Z(n359));
+  AN2 U349 ( .A(n295), .B(pi35), .Z(n356));
+  IV2 U350 ( .A(pi28), .Z(n295));
+  OR2 U351 ( .A(n375), .B(n376), .Z(po1));
+  OR2 U352 ( .A(n377), .B(n378), .Z(n376));
+  AN2 U353 ( .A(n379), .B(n380), .Z(n378));
+  AN2 U354 ( .A(n381), .B(n382), .Z(n380));
+  IV2 U355 ( .A(n365), .Z(n382));
+  AN2 U356 ( .A(n383), .B(pi05), .Z(n379));
+  AN2 U357 ( .A(n384), .B(n385), .Z(n377));
+  OR2 U358 ( .A(n386), .B(n387), .Z(n385));
+  AN2 U359 ( .A(n388), .B(n369), .Z(n387));
+  OR2 U360 ( .A(n389), .B(n390), .Z(n388));
+  AN2 U361 ( .A(n391), .B(n370), .Z(n390));
+  OR2 U362 ( .A(n392), .B(n393), .Z(n391));
+  OR2 U363 ( .A(n394), .B(n395), .Z(n393));
+  AN2 U364 ( .A(n396), .B(pi35), .Z(n395));
+  AN2 U365 ( .A(n397), .B(n358), .Z(n396));
+  AN2 U366 ( .A(n398), .B(n399), .Z(n394));
+  IV2 U367 ( .A(n400), .Z(n399));
+  AN2 U368 ( .A(n286), .B(pi08), .Z(n398));
+  AN2 U369 ( .A(n401), .B(n402), .Z(n392));
+  OR2 U370 ( .A(n403), .B(n286), .Z(n402));
+  AN2 U371 ( .A(n400), .B(n363), .Z(n403));
+  OR2 U372 ( .A(n404), .B(n300), .Z(n401));
+  AN2 U373 ( .A(pi37), .B(pi13), .Z(n404));
+  AN2 U374 ( .A(n405), .B(n406), .Z(n389));
+  AN2 U375 ( .A(n407), .B(n352), .Z(n406));
+  AN2 U376 ( .A(pi05), .B(n408), .Z(n405));
+  OR2 U377 ( .A(n409), .B(n410), .Z(n408));
+  AN2 U378 ( .A(n411), .B(n351), .Z(n410));
+  AN2 U379 ( .A(n412), .B(n413), .Z(n409));
+  OR2 U380 ( .A(n414), .B(n415), .Z(n412));
+  AN2 U381 ( .A(n416), .B(n351), .Z(n415));
+  OR2 U382 ( .A(n417), .B(n418), .Z(n416));
+  AN2 U383 ( .A(n286), .B(n319), .Z(n417));
+  AN2 U384 ( .A(n419), .B(n420), .Z(n414));
+  AN2 U385 ( .A(pi02), .B(n421), .Z(n419));
+  AN2 U386 ( .A(n422), .B(n423), .Z(n386));
+  AN2 U387 ( .A(n424), .B(n425), .Z(n423));
+  OR2 U388 ( .A(n426), .B(n427), .Z(n425));
+  AN2 U389 ( .A(n428), .B(n429), .Z(n427));
+  AN2 U390 ( .A(n430), .B(n407), .Z(n426));
+  IV2 U391 ( .A(n431), .Z(n407));
+  AN2 U392 ( .A(n432), .B(pi21), .Z(n431));
+  OR2 U393 ( .A(pi01), .B(pi20), .Z(n432));
+  OR2 U394 ( .A(n433), .B(n434), .Z(n430));
+  AN2 U395 ( .A(n429), .B(n339), .Z(n433));
+  OR2 U396 ( .A(n435), .B(n411), .Z(n424));
+  AN2 U397 ( .A(n436), .B(n437), .Z(n411));
+  AN2 U398 ( .A(n438), .B(n286), .Z(n437));
+  IV2 U399 ( .A(n439), .Z(n436));
+  OR2 U400 ( .A(pi26), .B(pi06), .Z(n439));
+  AN2 U401 ( .A(pi05), .B(n303), .Z(n422));
+  AN2 U402 ( .A(n440), .B(n441), .Z(n375));
+  OR2 U403 ( .A(n442), .B(n443), .Z(n441));
+  AN2 U404 ( .A(pi35), .B(n397), .Z(n443));
+  OR2 U405 ( .A(pi27), .B(pi28), .Z(n397));
+  AN2 U406 ( .A(n300), .B(n400), .Z(n442));
+  OR2 U407 ( .A(pi26), .B(n413), .Z(n400));
+  OR2 U408 ( .A(n444), .B(n445), .Z(po0));
+  OR2 U409 ( .A(n446), .B(n447), .Z(n445));
+  AN2 U410 ( .A(n448), .B(pi04), .Z(n447));
+  AN2 U411 ( .A(n383), .B(n381), .Z(n448));
+  OR2 U412 ( .A(n449), .B(n450), .Z(n381));
+  AN2 U413 ( .A(n420), .B(n451), .Z(n450));
+  AN2 U414 ( .A(n452), .B(n453), .Z(n449));
+  OR2 U415 ( .A(n454), .B(n374), .Z(n452));
+  AN2 U416 ( .A(n373), .B(n455), .Z(n454));
+  AN2 U417 ( .A(n456), .B(n457), .Z(n383));
+  AN2 U418 ( .A(n413), .B(n281), .Z(n457));
+  AN2 U419 ( .A(n384), .B(n458), .Z(n446));
+  OR2 U420 ( .A(n459), .B(n460), .Z(n458));
+  OR2 U421 ( .A(n461), .B(n462), .Z(n460));
+  AN2 U422 ( .A(n463), .B(n369), .Z(n462));
+  OR2 U423 ( .A(n464), .B(n465), .Z(n463));
+  AN2 U424 ( .A(n466), .B(n467), .Z(n465));
+  OR2 U425 ( .A(n468), .B(n469), .Z(n467));
+  OR2 U426 ( .A(n470), .B(n471), .Z(n469));
+  AN2 U427 ( .A(n365), .B(n350), .Z(n471));
+  AN2 U428 ( .A(n472), .B(pi37), .Z(n470));
+  AN2 U429 ( .A(pi13), .B(n473), .Z(n472));
+  OR2 U430 ( .A(n474), .B(n475), .Z(n473));
+  AN2 U431 ( .A(n370), .B(n338), .Z(n475));
+  AN2 U432 ( .A(pi16), .B(n476), .Z(n474));
+  OR2 U433 ( .A(n477), .B(n428), .Z(n476));
+  AN2 U434 ( .A(n478), .B(n350), .Z(n477));
+  AN2 U435 ( .A(n300), .B(n479), .Z(n468));
+  OR2 U436 ( .A(n480), .B(n286), .Z(n466));
+  AN2 U437 ( .A(n481), .B(n363), .Z(n480));
+  AN2 U438 ( .A(n482), .B(n483), .Z(n464));
+  AN2 U439 ( .A(n370), .B(n358), .Z(n482));
+  AN2 U440 ( .A(n484), .B(n485), .Z(n461));
+  AN2 U441 ( .A(n286), .B(n486), .Z(n484));
+  OR2 U442 ( .A(n487), .B(n488), .Z(n486));
+  AN2 U443 ( .A(n489), .B(n370), .Z(n488));
+  OR2 U444 ( .A(n490), .B(n345), .Z(n489));
+  AN2 U445 ( .A(n320), .B(pi08), .Z(n345));
+  AN2 U446 ( .A(pi06), .B(n369), .Z(n490));
+  AN2 U447 ( .A(n491), .B(n429), .Z(n487));
+  AN2 U448 ( .A(pi08), .B(n492), .Z(n491));
+  AN2 U449 ( .A(pi04), .B(n493), .Z(n459));
+  OR2 U450 ( .A(n494), .B(n495), .Z(n493));
+  AN2 U451 ( .A(n303), .B(n496), .Z(n495));
+  OR2 U452 ( .A(n497), .B(n498), .Z(n496));
+  AN2 U453 ( .A(n499), .B(n500), .Z(n498));
+  OR2 U454 ( .A(n501), .B(n307), .Z(n500));
+  AN2 U455 ( .A(n374), .B(n502), .Z(n307));
+  AN2 U456 ( .A(n413), .B(n453), .Z(n502));
+  AN2 U457 ( .A(n503), .B(n313), .Z(n501));
+  OR2 U458 ( .A(n504), .B(n505), .Z(n503));
+  AN2 U459 ( .A(n325), .B(n323), .Z(n504));
+  AN2 U460 ( .A(n413), .B(n506), .Z(n325));
+  AN2 U461 ( .A(n434), .B(n370), .Z(n499));
+  OR2 U462 ( .A(n507), .B(n320), .Z(n434));
+  AN2 U463 ( .A(n321), .B(n508), .Z(n507));
+  IV2 U464 ( .A(pi07), .Z(n321));
+  AN2 U465 ( .A(n509), .B(n429), .Z(n497));
+  AN2 U466 ( .A(n508), .B(n338), .Z(n429));
+  IV2 U467 ( .A(pi15), .Z(n338));
+  AN2 U468 ( .A(n510), .B(n492), .Z(n509));
+  OR2 U469 ( .A(n511), .B(n428), .Z(n492));
+  AN2 U470 ( .A(n479), .B(pi20), .Z(n428));
+  AN2 U471 ( .A(n339), .B(n350), .Z(n511));
+  OR2 U472 ( .A(n478), .B(n348), .Z(n339));
+  IV2 U473 ( .A(pi16), .Z(n348));
+  IV2 U474 ( .A(n349), .Z(n478));
+  AN2 U475 ( .A(n512), .B(n513), .Z(n349));
+  OR2 U476 ( .A(pi25), .B(pi17), .Z(n513));
+  OR2 U477 ( .A(n514), .B(pi24), .Z(n512));
+  IV2 U478 ( .A(pi09), .Z(n514));
+  OR2 U479 ( .A(n515), .B(n435), .Z(n510));
+  AN2 U480 ( .A(n516), .B(n413), .Z(n435));
+  OR2 U481 ( .A(n517), .B(n418), .Z(n516));
+  AN2 U482 ( .A(n363), .B(n453), .Z(n418));
+  OR2 U483 ( .A(n373), .B(n374), .Z(n363));
+  AN2 U484 ( .A(n323), .B(pi02), .Z(n373));
+  AN2 U485 ( .A(n505), .B(n438), .Z(n515));
+  OR2 U486 ( .A(n453), .B(n319), .Z(n438));
+  IV2 U487 ( .A(n518), .Z(n303));
+  OR2 U488 ( .A(n519), .B(n520), .Z(n518));
+  OR2 U489 ( .A(pi08), .B(n521), .Z(n520));
+  OR2 U490 ( .A(pi10), .B(n522), .Z(n519));
+  OR2 U491 ( .A(pi12), .B(pi11), .Z(n522));
+  AN2 U492 ( .A(n523), .B(n524), .Z(n494));
+  OR2 U493 ( .A(n525), .B(n526), .Z(n524));
+  AN2 U494 ( .A(n527), .B(n528), .Z(n526));
+  OR2 U495 ( .A(n529), .B(n530), .Z(n528));
+  AN2 U496 ( .A(n531), .B(n351), .Z(n530));
+  AN2 U497 ( .A(n358), .B(n453), .Z(n531));
+  OR2 U498 ( .A(n532), .B(n374), .Z(n358));
+  AN2 U499 ( .A(n506), .B(n323), .Z(n532));
+  AN2 U500 ( .A(n517), .B(n533), .Z(n529));
+  AN2 U501 ( .A(n421), .B(n534), .Z(n533));
+  IV2 U502 ( .A(pi14), .Z(n421));
+  AN2 U503 ( .A(n420), .B(n506), .Z(n517));
+  OR2 U504 ( .A(pi02), .B(n346), .Z(n506));
+  AN2 U505 ( .A(n323), .B(n319), .Z(n420));
+  AN2 U506 ( .A(n369), .B(n413), .Z(n527));
+  OR2 U507 ( .A(n320), .B(n508), .Z(n369));
+  AN2 U508 ( .A(n535), .B(n536), .Z(n525));
+  AN2 U509 ( .A(n313), .B(n351), .Z(n536));
+  IV2 U510 ( .A(n521), .Z(n351));
+  AN2 U511 ( .A(pi00), .B(pi14), .Z(n521));
+  OR2 U512 ( .A(n537), .B(n453), .Z(n313));
+  IV2 U513 ( .A(pi13), .Z(n453));
+  AN2 U514 ( .A(n319), .B(n534), .Z(n537));
+  IV2 U515 ( .A(pi37), .Z(n534));
+  IV2 U516 ( .A(pi03), .Z(n319));
+  AN2 U517 ( .A(n505), .B(n538), .Z(n535));
+  OR2 U518 ( .A(n539), .B(n320), .Z(n538));
+  IV2 U519 ( .A(pi19), .Z(n320));
+  AN2 U520 ( .A(n540), .B(n508), .Z(n539));
+  IV2 U521 ( .A(pi23), .Z(n508));
+  IV2 U522 ( .A(pi08), .Z(n540));
+  AN2 U523 ( .A(n541), .B(n286), .Z(n505));
+  AN2 U524 ( .A(n346), .B(n323), .Z(n286));
+  IV2 U525 ( .A(pi27), .Z(n541));
+  AN2 U526 ( .A(n370), .B(n352), .Z(n523));
+  IV2 U527 ( .A(pi36), .Z(n352));
+  OR2 U528 ( .A(n350), .B(n479), .Z(n370));
+  IV2 U529 ( .A(pi21), .Z(n479));
+  IV2 U530 ( .A(pi20), .Z(n350));
+  IV2 U531 ( .A(n542), .Z(n384));
+  OR2 U532 ( .A(n543), .B(n544), .Z(n542));
+  OR2 U533 ( .A(pi29), .B(pi22), .Z(n544));
+  OR2 U534 ( .A(pi34), .B(pi33), .Z(n543));
+  AN2 U535 ( .A(n440), .B(n545), .Z(n444));
+  OR2 U536 ( .A(n546), .B(n483), .Z(n545));
+  OR2 U537 ( .A(n547), .B(n548), .Z(n483));
+  AN2 U538 ( .A(pi28), .B(pi35), .Z(n548));
+  AN2 U539 ( .A(pi26), .B(n485), .Z(n547));
+  IV2 U540 ( .A(n481), .Z(n485));
+  AN2 U541 ( .A(n549), .B(n481), .Z(n546));
+  OR2 U542 ( .A(pi27), .B(n413), .Z(n481));
+  IV2 U543 ( .A(pi35), .Z(n413));
+  OR2 U544 ( .A(n365), .B(n300), .Z(n549));
+  AN2 U545 ( .A(pi01), .B(pi31), .Z(n300));
+  AN2 U546 ( .A(pi01), .B(pi21), .Z(n365));
+  AN2 U547 ( .A(n456), .B(n550), .Z(n440));
+  AN2 U548 ( .A(n281), .B(n551), .Z(n550));
+  OR2 U549 ( .A(n374), .B(n552), .Z(n551));
+  AN2 U550 ( .A(n323), .B(n451), .Z(n552));
+  OR2 U551 ( .A(n553), .B(n554), .Z(n451));
+  AN2 U552 ( .A(n555), .B(n346), .Z(n554));
+  IV2 U553 ( .A(pi32), .Z(n346));
+  AN2 U554 ( .A(pi02), .B(n455), .Z(n553));
+  IV2 U555 ( .A(pi29), .Z(n455));
+  IV2 U556 ( .A(pi30), .Z(n323));
+  AN2 U557 ( .A(n555), .B(pi03), .Z(n374));
+  IV2 U558 ( .A(pi02), .Z(n555));
+  IV2 U559 ( .A(pi34), .Z(n281));
+  IV2 U560 ( .A(n292), .Z(n456));
+  OR2 U561 ( .A(pi00), .B(n556), .Z(n292));
+  OR2 U562 ( .A(pi37), .B(pi36), .Z(n556));
+
+endmodule
+
+module IV2(A,  Z);
+  input A;
+  output Z;
+
+  assign Z = ~A;
+endmodule
+
+module AN2(A,  B,  Z);
+  input A,  B;
+  output Z;
+
+  assign Z = A & B;
+endmodule
+
+module OR2(A,  B,  Z);
+  input A,  B;
+  output Z;
+
+  assign Z = A | B;
+endmodule