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

1 files changed, 400 insertions, 0 deletions

diff --git a/examples/smtbmc/glift/alu2.v b/examples/smtbmc/glift/alu2.v
new file mode 100755
index 000000000..6b6e3d7af
--- /dev/null
+++ b/examples/smtbmc/glift/alu2.v
@@ -0,0 +1,400 @@
+module alu2_lev2(pi0,  pi1,  pi2,  pi3,  pi4,  pi5,  pi6,  pi7,  pi8,  pi9,  
+	po0,  po1,  po2,  po3,  po4,  po5);
+
+input pi0, pi1, pi2, pi3, pi4, pi5, pi6, pi7, pi8, pi9;
+
+output po0, po1, po2, po3, po4, po5;
+
+wire 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, n557, 
+	n558, n559, n560, n561, n562, n563, n564, n565, n566, n567, 
+	n568, n569, n570, n571, n572, n573, n574, n575, n576, n577, 
+	n578, n579, n580, n581, n582, n583, n584, n585, n586, n587, 
+	n588, n589, n590, n591, n592, n593, n594, n595, n596, n597, 
+	n598, n599, n600, n601, n602, n603, n604, n605, n606, n607, 
+	n608, n609, n610, n611, n612, n613, n614, n615, n616, n617, 
+	n618, n619, n620, n621, n622, n623, n624, n625, n626, n627, 
+	n628, n629, n630, n631, n632, n633, n634, n635, n636, n637, 
+	n638, n639, n640, n641, n642, n643, n644, n645, n646, n647, 
+	n648, n649, n650, n651, n652, n653, n654, n655, n656, n657, 
+	n658, n659, n660, n661, n662, n663, n664, n665, n666, n667, 
+	n668, n669, n670, n671, n672, n673, n674, n675, n676, n677, 
+	n678, n679, n680, n681, n682, n683, n684, n685, n686, n687;
+
+  AN2 U363 ( .A(n358),  .B(po2),  .Z(po5));
+  OR2 U364 ( .A(n359),  .B(n360),  .Z(n358));
+  AN2 U365 ( .A(n361),  .B(n362),  .Z(n359));
+  AN2 U366 ( .A(pi9),  .B(n363),  .Z(po4));
+  OR2 U367 ( .A(n364),  .B(n365),  .Z(n363));
+  OR2 U368 ( .A(n366),  .B(n367),  .Z(n365));
+  AN2 U369 ( .A(pi6),  .B(n368),  .Z(n367));
+  OR2 U370 ( .A(n369),  .B(n370),  .Z(n368));
+  OR2 U371 ( .A(n371),  .B(n372),  .Z(n370));
+  OR2 U372 ( .A(n373),  .B(n374),  .Z(n372));
+  AN2 U373 ( .A(n375),  .B(n376),  .Z(n374));
+  AN2 U374 ( .A(n377),  .B(n378),  .Z(n375));
+  OR2 U375 ( .A(n379),  .B(n380),  .Z(n377));
+  OR2 U376 ( .A(n381),  .B(n382),  .Z(n380));
+  OR2 U377 ( .A(n383),  .B(n384),  .Z(n379));
+  AN2 U378 ( .A(n385),  .B(pi5),  .Z(n384));
+  AN2 U379 ( .A(n386),  .B(n387),  .Z(n383));
+  AN2 U380 ( .A(pi4),  .B(n361),  .Z(n386));
+  AN2 U381 ( .A(n388),  .B(n389),  .Z(n373));
+  OR2 U382 ( .A(n390),  .B(n391),  .Z(n388));
+  AN2 U383 ( .A(pi1),  .B(n392),  .Z(n390));
+  OR2 U384 ( .A(n393),  .B(n394),  .Z(n392));
+  OR2 U385 ( .A(pi7),  .B(n395),  .Z(n394));
+  AN2 U386 ( .A(n381),  .B(n396),  .Z(n395));
+  OR2 U387 ( .A(n397),  .B(n398),  .Z(n369));
+  AN2 U388 ( .A(n399),  .B(n400),  .Z(n398));
+  AN2 U389 ( .A(n387),  .B(n401),  .Z(n399));
+  AN2 U390 ( .A(n402),  .B(n403),  .Z(n397));
+  AN2 U391 ( .A(pi0),  .B(n404),  .Z(n402));
+  OR2 U392 ( .A(pi1),  .B(n389),  .Z(n404));
+  AN2 U393 ( .A(n405),  .B(n406),  .Z(n366));
+  OR2 U394 ( .A(n407),  .B(n408),  .Z(n406));
+  AN2 U395 ( .A(n360),  .B(n409),  .Z(n408));
+  OR2 U396 ( .A(n410),  .B(n411),  .Z(n409));
+  OR2 U397 ( .A(n412),  .B(n413),  .Z(n411));
+  AN2 U398 ( .A(n414),  .B(pi3),  .Z(n413));
+  AN2 U399 ( .A(n389),  .B(n415),  .Z(n410));
+  AN2 U400 ( .A(po3),  .B(n416),  .Z(n407));
+  OR2 U401 ( .A(n417),  .B(n414),  .Z(n416));
+  OR2 U402 ( .A(n418),  .B(n419),  .Z(n364));
+  OR2 U403 ( .A(n420),  .B(n421),  .Z(n419));
+  AN2 U404 ( .A(n422),  .B(n382),  .Z(n421));
+  AN2 U405 ( .A(pi7),  .B(n389),  .Z(n422));
+  AN2 U406 ( .A(n423),  .B(n424),  .Z(n418));
+  AN2 U407 ( .A(n425),  .B(n426),  .Z(n423));
+  OR2 U408 ( .A(n427),  .B(po3),  .Z(po2));
+  AN2 U409 ( .A(n428),  .B(n429),  .Z(n427));
+  OR2 U410 ( .A(n430),  .B(n431),  .Z(po1));
+  AN2 U411 ( .A(pi9),  .B(n432),  .Z(n431));
+  OR2 U412 ( .A(n433),  .B(n434),  .Z(n432));
+  OR2 U413 ( .A(n435),  .B(n436),  .Z(n434));
+  AN2 U414 ( .A(n437),  .B(n438),  .Z(n436));
+  IV2 U415 ( .A(n425),  .Z(n438));
+  AN2 U416 ( .A(n424),  .B(n426),  .Z(n437));
+  OR2 U417 ( .A(n439),  .B(n440),  .Z(n424));
+  OR2 U418 ( .A(n441),  .B(n442),  .Z(n440));
+  AN2 U419 ( .A(n381),  .B(n443),  .Z(n442));
+  OR2 U420 ( .A(n444),  .B(n445),  .Z(n443));
+  AN2 U421 ( .A(n446),  .B(n447),  .Z(n441));
+  AN2 U422 ( .A(n387),  .B(n361),  .Z(n446));
+  AN2 U423 ( .A(n448),  .B(n425),  .Z(n435));
+  OR2 U424 ( .A(n449),  .B(n450),  .Z(n425));
+  OR2 U425 ( .A(n420),  .B(n451),  .Z(n450));
+  OR2 U426 ( .A(n452),  .B(n453),  .Z(n451));
+  AN2 U427 ( .A(pi6),  .B(n454),  .Z(n453));
+  OR2 U428 ( .A(n371),  .B(n455),  .Z(n454));
+  AN2 U429 ( .A(n376),  .B(n456),  .Z(n455));
+  OR2 U430 ( .A(n457),  .B(n458),  .Z(n456));
+  OR2 U431 ( .A(n459),  .B(n460),  .Z(n458));
+  AN2 U432 ( .A(n461),  .B(n378),  .Z(n460));
+  OR2 U433 ( .A(n462),  .B(n463),  .Z(n461));
+  AN2 U434 ( .A(n385),  .B(n464),  .Z(n462));
+  OR2 U435 ( .A(n465),  .B(pi5),  .Z(n464));
+  AN2 U436 ( .A(pi7),  .B(n466),  .Z(n459));
+  OR2 U437 ( .A(n467),  .B(n468),  .Z(n466));
+  OR2 U438 ( .A(n469),  .B(n470),  .Z(n468));
+  AN2 U439 ( .A(n381),  .B(pi1),  .Z(n470));
+  AN2 U440 ( .A(n471),  .B(n428),  .Z(n469));
+  AN2 U441 ( .A(pi0),  .B(n387),  .Z(n471));
+  AN2 U442 ( .A(n412),  .B(n361),  .Z(n467));
+  AN2 U443 ( .A(n472),  .B(n473),  .Z(n457));
+  AN2 U444 ( .A(n360),  .B(n428),  .Z(n472));
+  AN2 U445 ( .A(n463),  .B(n428),  .Z(n371));
+  AN2 U446 ( .A(n474),  .B(n475),  .Z(n452));
+  OR2 U447 ( .A(n476),  .B(n477),  .Z(n474));
+  OR2 U448 ( .A(n478),  .B(n479),  .Z(n477));
+  AN2 U449 ( .A(n480),  .B(n428),  .Z(n479));
+  AN2 U450 ( .A(n481),  .B(n482),  .Z(n480));
+  OR2 U451 ( .A(n360),  .B(n389),  .Z(n482));
+  OR2 U452 ( .A(n401),  .B(n483),  .Z(n481));
+  AN2 U453 ( .A(pi7),  .B(n484),  .Z(n483));
+  OR2 U454 ( .A(n393),  .B(n485),  .Z(n484));
+  AN2 U455 ( .A(n376),  .B(n415),  .Z(n485));
+  AN2 U456 ( .A(n414),  .B(n429),  .Z(n393));
+  AN2 U457 ( .A(n486),  .B(n378),  .Z(n478));
+  OR2 U458 ( .A(n412),  .B(n389),  .Z(n486));
+  AN2 U459 ( .A(n487),  .B(pi1),  .Z(n412));
+  OR2 U460 ( .A(n488),  .B(n489),  .Z(n476));
+  AN2 U461 ( .A(n490),  .B(n401),  .Z(n488));
+  AN2 U462 ( .A(pi1),  .B(n429),  .Z(n490));
+  AN2 U463 ( .A(n385),  .B(n491),  .Z(n420));
+  IV2 U464 ( .A(n492),  .Z(n491));
+  OR2 U465 ( .A(n493),  .B(n487),  .Z(n492));
+  AN2 U466 ( .A(n494),  .B(n495),  .Z(n493));
+  OR2 U467 ( .A(pi6),  .B(n389),  .Z(n495));
+  OR2 U468 ( .A(pi7),  .B(pi1),  .Z(n494));
+  OR2 U469 ( .A(n496),  .B(n497),  .Z(n449));
+  AN2 U470 ( .A(n498),  .B(n376),  .Z(n497));
+  AN2 U471 ( .A(n381),  .B(n382),  .Z(n498));
+  AN2 U472 ( .A(n499),  .B(n389),  .Z(n496));
+  OR2 U473 ( .A(n500),  .B(n501),  .Z(n499));
+  OR2 U474 ( .A(n502),  .B(n503),  .Z(n501));
+  AN2 U475 ( .A(n385),  .B(n504),  .Z(n503));
+  OR2 U476 ( .A(n505),  .B(n506),  .Z(n504));
+  AN2 U477 ( .A(po3),  .B(n400),  .Z(n506));
+  AN2 U478 ( .A(n507),  .B(n428),  .Z(n505));
+  AN2 U479 ( .A(n508),  .B(n387),  .Z(n502));
+  OR2 U480 ( .A(n509),  .B(n510),  .Z(n508));
+  OR2 U481 ( .A(n489),  .B(n511),  .Z(n510));
+  OR2 U482 ( .A(n465),  .B(n512),  .Z(n511));
+  AN2 U483 ( .A(n513),  .B(pi1),  .Z(n512));
+  AN2 U484 ( .A(pi0),  .B(n514),  .Z(n513));
+  OR2 U485 ( .A(n507),  .B(n515),  .Z(n514));
+  AN2 U486 ( .A(n361),  .B(n428),  .Z(n465));
+  AN2 U487 ( .A(po3),  .B(n360),  .Z(n489));
+  OR2 U488 ( .A(n516),  .B(n517),  .Z(n509));
+  OR2 U489 ( .A(n518),  .B(n519),  .Z(n517));
+  AN2 U490 ( .A(n391),  .B(n362),  .Z(n519));
+  AN2 U491 ( .A(n428),  .B(n400),  .Z(n391));
+  AN2 U492 ( .A(n520),  .B(n521),  .Z(n518));
+  OR2 U493 ( .A(n522),  .B(n362),  .Z(n521));
+  AN2 U494 ( .A(n429),  .B(n523),  .Z(n520));
+  AN2 U495 ( .A(n417),  .B(n378),  .Z(n516));
+  AN2 U496 ( .A(n522),  .B(n382),  .Z(n500));
+  AN2 U497 ( .A(pi1),  .B(n396),  .Z(n382));
+  AN2 U498 ( .A(n361),  .B(n378),  .Z(n522));
+  OR2 U499 ( .A(n524),  .B(n525),  .Z(n448));
+  OR2 U500 ( .A(n526),  .B(n527),  .Z(n525));
+  OR2 U501 ( .A(pi8),  .B(n528),  .Z(n524));
+  AN2 U502 ( .A(n529),  .B(n530),  .Z(n430));
+  OR2 U503 ( .A(n531),  .B(n532),  .Z(n529));
+  OR2 U504 ( .A(n533),  .B(n534),  .Z(n532));
+  OR2 U505 ( .A(n535),  .B(n536),  .Z(n534));
+  AN2 U506 ( .A(n537),  .B(n376),  .Z(n536));
+  IV2 U507 ( .A(n389),  .Z(n376));
+  AN2 U508 ( .A(n538),  .B(n389),  .Z(n535));
+  OR2 U509 ( .A(n539),  .B(n540),  .Z(n389));
+  OR2 U510 ( .A(n541),  .B(n542),  .Z(n540));
+  OR2 U511 ( .A(n543),  .B(n544),  .Z(n542));
+  AN2 U512 ( .A(pi1),  .B(n545),  .Z(n544));
+  AN2 U513 ( .A(n546),  .B(n428),  .Z(n543));
+  AN2 U514 ( .A(n547),  .B(n548),  .Z(n546));
+  OR2 U515 ( .A(pi3),  .B(n396),  .Z(n548));
+  AN2 U516 ( .A(pi9),  .B(n549),  .Z(n541));
+  OR2 U517 ( .A(n550),  .B(n551),  .Z(n549));
+  OR2 U518 ( .A(n552),  .B(n553),  .Z(n551));
+  AN2 U519 ( .A(n554),  .B(n507),  .Z(n553));
+  AN2 U520 ( .A(n396),  .B(pi0),  .Z(n554));
+  AN2 U521 ( .A(n555),  .B(n556),  .Z(n552));
+  AN2 U522 ( .A(n557),  .B(n415),  .Z(n556));
+  AN2 U523 ( .A(po3),  .B(n558),  .Z(n555));
+  OR2 U524 ( .A(n559),  .B(n560),  .Z(n550));
+  AN2 U525 ( .A(n561),  .B(n429),  .Z(n560));
+  AN2 U526 ( .A(n417),  .B(n562),  .Z(n561));
+  OR2 U527 ( .A(n563),  .B(n564),  .Z(n562));
+  AN2 U528 ( .A(n558),  .B(n428),  .Z(n564));
+  AN2 U529 ( .A(pi1),  .B(n565),  .Z(n563));
+  AN2 U530 ( .A(pi3),  .B(n566),  .Z(n559));
+  OR2 U531 ( .A(n567),  .B(n414),  .Z(n566));
+  AN2 U532 ( .A(n568),  .B(n569),  .Z(n567));
+  AN2 U533 ( .A(n565),  .B(n428),  .Z(n568));
+  OR2 U534 ( .A(n570),  .B(n571),  .Z(n539));
+  AN2 U535 ( .A(n572),  .B(n429),  .Z(n571));
+  AN2 U536 ( .A(po3),  .B(n573),  .Z(n570));
+  OR2 U537 ( .A(n574),  .B(n575),  .Z(n538));
+  OR2 U538 ( .A(n445),  .B(n576),  .Z(n575));
+  AN2 U539 ( .A(n577),  .B(pi3),  .Z(n576));
+  AN2 U540 ( .A(n578),  .B(pi1),  .Z(n574));
+  AN2 U541 ( .A(n507),  .B(pi1),  .Z(n533));
+  OR2 U542 ( .A(n579),  .B(n580),  .Z(n531));
+  OR2 U543 ( .A(n581),  .B(n582),  .Z(n580));
+  AN2 U544 ( .A(n444),  .B(po3),  .Z(n582));
+  AN2 U545 ( .A(pi1),  .B(pi3),  .Z(po3));
+  AN2 U546 ( .A(n583),  .B(n557),  .Z(n581));
+  AN2 U547 ( .A(n584),  .B(n429),  .Z(n583));
+  OR2 U548 ( .A(n585),  .B(n414),  .Z(n584));
+  AN2 U549 ( .A(n417),  .B(n428),  .Z(n585));
+  AN2 U550 ( .A(n586),  .B(pi7),  .Z(n579));
+  AN2 U551 ( .A(n587),  .B(n588),  .Z(n586));
+  OR2 U552 ( .A(pi3),  .B(n589),  .Z(n588));
+  AN2 U553 ( .A(pi1),  .B(n523),  .Z(n589));
+  OR2 U554 ( .A(n429),  .B(n590),  .Z(n587));
+  OR2 U555 ( .A(n417),  .B(n591),  .Z(n590));
+  AN2 U556 ( .A(n592),  .B(n428),  .Z(n591));
+  IV2 U557 ( .A(pi1),  .Z(n428));
+  IV2 U558 ( .A(pi3),  .Z(n429));
+  OR2 U559 ( .A(n593),  .B(n594),  .Z(po0));
+  OR2 U560 ( .A(n595),  .B(n596),  .Z(n594));
+  AN2 U561 ( .A(n597),  .B(pi8),  .Z(n596));
+  AN2 U562 ( .A(n598),  .B(n381),  .Z(n597));
+  AN2 U563 ( .A(pi0),  .B(n385),  .Z(n381));
+  AN2 U564 ( .A(n507),  .B(n487),  .Z(n598));
+  AN2 U565 ( .A(n528),  .B(n426),  .Z(n595));
+  AN2 U566 ( .A(pi6),  .B(n599),  .Z(n528));
+  IV2 U567 ( .A(n600),  .Z(n599));
+  OR2 U568 ( .A(n601),  .B(n361),  .Z(n600));
+  AN2 U569 ( .A(n602),  .B(n603),  .Z(n601));
+  AN2 U570 ( .A(n604),  .B(n605),  .Z(n603));
+  OR2 U571 ( .A(pi7),  .B(n606),  .Z(n605));
+  OR2 U572 ( .A(n607),  .B(n387),  .Z(n606));
+  OR2 U573 ( .A(n378),  .B(n487),  .Z(n604));
+  AN2 U574 ( .A(n608),  .B(n609),  .Z(n602));
+  OR2 U575 ( .A(pi2),  .B(n415),  .Z(n608));
+  OR2 U576 ( .A(n610),  .B(n611),  .Z(n593));
+  AN2 U577 ( .A(pi9),  .B(n612),  .Z(n611));
+  OR2 U578 ( .A(n613),  .B(n614),  .Z(n612));
+  OR2 U579 ( .A(n433),  .B(n615),  .Z(n614));
+  AN2 U580 ( .A(n527),  .B(n426),  .Z(n615));
+  OR2 U581 ( .A(n616),  .B(n617),  .Z(n527));
+  AN2 U582 ( .A(n618),  .B(n361),  .Z(n617));
+  OR2 U583 ( .A(n619),  .B(n620),  .Z(n618));
+  OR2 U584 ( .A(n621),  .B(n622),  .Z(n620));
+  AN2 U585 ( .A(n592),  .B(n362),  .Z(n622));
+  AN2 U586 ( .A(n385),  .B(n623),  .Z(n621));
+  OR2 U587 ( .A(n624),  .B(n625),  .Z(n623));
+  AN2 U588 ( .A(n626),  .B(n415),  .Z(n625));
+  AN2 U589 ( .A(n507),  .B(n523),  .Z(n624));
+  AN2 U590 ( .A(n473),  .B(n557),  .Z(n619));
+  AN2 U591 ( .A(n523),  .B(n387),  .Z(n473));
+  AN2 U592 ( .A(n569),  .B(n387),  .Z(n616));
+  AN2 U593 ( .A(n578),  .B(n627),  .Z(n433));
+  AN2 U594 ( .A(n378),  .B(n475),  .Z(n627));
+  OR2 U595 ( .A(n628),  .B(n629),  .Z(n613));
+  AN2 U596 ( .A(n526),  .B(n426),  .Z(n629));
+  IV2 U597 ( .A(pi8),  .Z(n426));
+  AN2 U598 ( .A(n360),  .B(n405),  .Z(n526));
+  AN2 U599 ( .A(pi8),  .B(n630),  .Z(n628));
+  OR2 U600 ( .A(n631),  .B(n439),  .Z(n630));
+  OR2 U601 ( .A(n632),  .B(n633),  .Z(n439));
+  OR2 U602 ( .A(n634),  .B(n635),  .Z(n633));
+  AN2 U603 ( .A(n636),  .B(n378),  .Z(n635));
+  OR2 U604 ( .A(n637),  .B(n360),  .Z(n636));
+  AN2 U605 ( .A(n387),  .B(n475),  .Z(n637));
+  AN2 U606 ( .A(n638),  .B(n475),  .Z(n634));
+  OR2 U607 ( .A(n639),  .B(n640),  .Z(n638));
+  AN2 U608 ( .A(n558),  .B(pi4),  .Z(n639));
+  OR2 U609 ( .A(n463),  .B(n641),  .Z(n632));
+  AN2 U610 ( .A(n642),  .B(n385),  .Z(n641));
+  AN2 U611 ( .A(n557),  .B(n361),  .Z(n642));
+  AN2 U612 ( .A(n361),  .B(n578),  .Z(n463));
+  AN2 U613 ( .A(n403),  .B(n361),  .Z(n631));
+  IV2 U614 ( .A(n609),  .Z(n403));
+  OR2 U615 ( .A(n385),  .B(n378),  .Z(n609));
+  AN2 U616 ( .A(n643),  .B(n530),  .Z(n610));
+  OR2 U617 ( .A(n644),  .B(n645),  .Z(n643));
+  OR2 U618 ( .A(n646),  .B(n647),  .Z(n645));
+  OR2 U619 ( .A(n648),  .B(n649),  .Z(n647));
+  AN2 U620 ( .A(n537),  .B(n385),  .Z(n649));
+  IV2 U621 ( .A(n387),  .Z(n385));
+  OR2 U622 ( .A(n650),  .B(n651),  .Z(n537));
+  AN2 U623 ( .A(n396),  .B(pi6),  .Z(n651));
+  AN2 U624 ( .A(n400),  .B(n475),  .Z(n650));
+  AN2 U625 ( .A(n652),  .B(n387),  .Z(n648));
+  OR2 U626 ( .A(n653),  .B(n654),  .Z(n387));
+  OR2 U627 ( .A(n655),  .B(n656),  .Z(n654));
+  OR2 U628 ( .A(n657),  .B(n658),  .Z(n656));
+  AN2 U629 ( .A(n360),  .B(n573),  .Z(n658));
+  OR2 U630 ( .A(n659),  .B(n660),  .Z(n573));
+  AN2 U631 ( .A(n405),  .B(n578),  .Z(n660));
+  AN2 U632 ( .A(n396),  .B(n661),  .Z(n659));
+  OR2 U633 ( .A(n405),  .B(n557),  .Z(n661));
+  AN2 U634 ( .A(n475),  .B(pi7),  .Z(n405));
+  IV2 U635 ( .A(n607),  .Z(n396));
+  OR2 U636 ( .A(pi5),  .B(pi4),  .Z(n607));
+  AN2 U637 ( .A(n640),  .B(n417),  .Z(n657));
+  AN2 U638 ( .A(n572),  .B(n362),  .Z(n655));
+  OR2 U639 ( .A(n662),  .B(n663),  .Z(n572));
+  OR2 U640 ( .A(n664),  .B(n665),  .Z(n663));
+  AN2 U641 ( .A(n578),  .B(n557),  .Z(n665));
+  AN2 U642 ( .A(n417),  .B(n626),  .Z(n664));
+  AN2 U643 ( .A(n507),  .B(n530),  .Z(n662));
+  OR2 U644 ( .A(n666),  .B(n667),  .Z(n653));
+  OR2 U645 ( .A(n668),  .B(n669),  .Z(n667));
+  AN2 U646 ( .A(n670),  .B(n545),  .Z(n669));
+  OR2 U647 ( .A(n400),  .B(n671),  .Z(n545));
+  AN2 U648 ( .A(pi9),  .B(n414),  .Z(n671));
+  AN2 U649 ( .A(n378),  .B(n414),  .Z(n400));
+  IV2 U650 ( .A(pi7),  .Z(n378));
+  OR2 U651 ( .A(pi0),  .B(pi2),  .Z(n670));
+  AN2 U652 ( .A(n672),  .B(n547),  .Z(n668));
+  AN2 U653 ( .A(n475),  .B(n530),  .Z(n547));
+  IV2 U654 ( .A(pi9),  .Z(n530));
+  AN2 U655 ( .A(n361),  .B(n415),  .Z(n672));
+  AN2 U656 ( .A(n558),  .B(n569),  .Z(n666));
+  AN2 U657 ( .A(n557),  .B(n417),  .Z(n569));
+  OR2 U658 ( .A(n673),  .B(n674),  .Z(n652));
+  OR2 U659 ( .A(n445),  .B(n675),  .Z(n674));
+  AN2 U660 ( .A(n577),  .B(pi2),  .Z(n675));
+  AN2 U661 ( .A(n523),  .B(n447),  .Z(n445));
+  OR2 U662 ( .A(n577),  .B(n507),  .Z(n447));
+  AN2 U663 ( .A(n475),  .B(n415),  .Z(n577));
+  AN2 U664 ( .A(n578),  .B(pi0),  .Z(n673));
+  IV2 U665 ( .A(n487),  .Z(n578));
+  OR2 U666 ( .A(n415),  .B(n523),  .Z(n487));
+  AN2 U667 ( .A(n507),  .B(pi0),  .Z(n646));
+  AN2 U668 ( .A(pi6),  .B(pi7),  .Z(n507));
+  OR2 U669 ( .A(n676),  .B(n677),  .Z(n644));
+  OR2 U670 ( .A(n678),  .B(n679),  .Z(n677));
+  AN2 U671 ( .A(n444),  .B(n360),  .Z(n679));
+  IV2 U672 ( .A(n401),  .Z(n360));
+  OR2 U673 ( .A(n362),  .B(n361),  .Z(n401));
+  AN2 U674 ( .A(pi6),  .B(n417),  .Z(n444));
+  AN2 U675 ( .A(n680),  .B(n557),  .Z(n678));
+  IV2 U676 ( .A(n626),  .Z(n557));
+  OR2 U677 ( .A(pi7),  .B(n475),  .Z(n626));
+  AN2 U678 ( .A(n681),  .B(n362),  .Z(n680));
+  OR2 U679 ( .A(n682),  .B(n414),  .Z(n681));
+  AN2 U680 ( .A(n417),  .B(n361),  .Z(n682));
+  IV2 U681 ( .A(pi0),  .Z(n361));
+  AN2 U682 ( .A(pi7),  .B(n683),  .Z(n676));
+  OR2 U683 ( .A(n684),  .B(n685),  .Z(n683));
+  OR2 U684 ( .A(n686),  .B(n687),  .Z(n685));
+  AN2 U685 ( .A(n592),  .B(n558),  .Z(n687));
+  IV2 U686 ( .A(n565),  .Z(n558));
+  OR2 U687 ( .A(pi0),  .B(n362),  .Z(n565));
+  AN2 U688 ( .A(n475),  .B(n414),  .Z(n592));
+  IV2 U689 ( .A(n515),  .Z(n414));
+  OR2 U690 ( .A(pi5),  .B(n415),  .Z(n515));
+  IV2 U691 ( .A(pi6),  .Z(n475));
+  AN2 U692 ( .A(n640),  .B(n523),  .Z(n686));
+  IV2 U693 ( .A(pi5),  .Z(n523));
+  AN2 U694 ( .A(n362),  .B(pi0),  .Z(n640));
+  IV2 U695 ( .A(pi2),  .Z(n362));
+  AN2 U696 ( .A(n417),  .B(pi2),  .Z(n684));
+  AN2 U697 ( .A(n415),  .B(pi5),  .Z(n417));
+  IV2 U698 ( .A(pi4),  .Z(n415));
+
+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