riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
yosys/examples/smtbmc/glift/too_large.v

346 lines
14 KiB
Verilog
Raw Normal View History

glift: Add examples, including a number of benchmarks used in some academic works.
2020-04-24 03:23:08 -05:00
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