mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity

Merge pull request #2019 from boqwxp/glift

Browse source 
Add `glift` command for creating gate-level information flow tracking models and optimization problems
This commit is contained in:
Claire Xen 2022-02-11 15:51:24 +01:00 • committed by GitHub
commit e016518866
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
21 changed files with 7849 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
CODEOWNERS
View file

@ -42,4 +42,5 @@ backends/firrtl @ucbjrl @azidar
passes/sat/qbfsat.cc @boqwxp
passes/sat/qbfsat.h @boqwxp
passes/cmds/exec.cc @boqwxp
passes/cmds/glift.cc @boqwxp
passes/cmds/printattrs.cc @boqwxp

6
examples/smtbmc/Makefile
View file

@ -1,5 +1,5 @@
all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9
all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9 glift_mux
demo1: demo1.smt2
yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
@ -31,6 +31,9 @@ demo8: demo8.smt2
demo9: demo9.smt2
yosys-smtbmc -s z3 -t 1 -g demo9.smt2
glift_mux:
yosys -ql glift_mux.yslog glift/mux2.ys
demo1.smt2: demo1.v
yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
@ -68,6 +71,7 @@ clean:
rm -f demo7.yslog demo7.smt2
rm -f demo8.yslog demo8.smt2
rm -f demo9.yslog demo9.smt2
rm -f glift_mux.ys
.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9 clean

4194
examples/smtbmc/glift/C7552.v Executable file
View file

File diff suppressed because it is too large Load diff

41
examples/smtbmc/glift/C7552.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog C7552.v
techmap
flatten
select C7552_lev2
glift -create-instrumented-model
techmap
opt
rename C7552_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog C7552.v
techmap
flatten
select C7552_lev2
glift -create-precise-model
techmap
opt
rename C7552_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution C7552.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file C7552.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

451
examples/smtbmc/glift/C880.v Executable file
View file

@ -0,0 +1,451 @@
module C880_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, pi38, pi39,
pi40, pi41, pi42, pi43, pi44, pi45, pi46, pi47, pi48, pi49,
pi50, pi51, pi52, pi53, pi54, pi55, pi56, pi57, pi58, pi59,
po00, po01, po02, po03, po04, po05, po06, po07, po08, po09,
po10, po11, po12, po13, po14, po15, po16, po17, po18, po19,
po20, po21, po22, po23, po24, po25);
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, pi38, pi39,
pi40, pi41, pi42, pi43, pi44, pi45, pi46, pi47, pi48, pi49,
pi50, pi51, pi52, pi53, pi54, pi55, pi56, pi57, pi58, pi59;
output po00, po01, po02, po03, po04, po05, po06, po07, po08, po09,
po10, po11, po12, po13, po14, po15, po16, po17, po18, po19,
po20, po21, po22, po23, po24, po25;
wire n137, n346, n364, n415, n295, n427, n351, n377, n454, n357,
n358, n359, n360, n361, n362, n363, n365, n366, n367, n368,
n369, n370, n371, n372, n373, n374, n375, n376, 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, n416, n417, n418, n419, n420,
n421, n422, n423, n424, n425, n426, 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, 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, n688, n689, n690, n691, n692,
n693, n694, n695, n696;
assign po22 = n137;
assign po19 = n346;
assign po16 = n364;
assign po17 = n415;
assign po18 = n295;
assign po00 = n427;
assign po09 = n351;
assign po04 = n377;
assign po06 = n454;
AN2 U371 ( .A(pi11), .B(pi08), .Z(n357));
AN2 U372 ( .A(pi28), .B(n357), .Z(n346));
AN2 U373 ( .A(pi41), .B(pi25), .Z(n369));
AN2 U374 ( .A(pi52), .B(n369), .Z(n361));
AN2 U375 ( .A(pi51), .B(pi54), .Z(n359));
AN2 U376 ( .A(pi28), .B(pi31), .Z(n604));
AN2 U377 ( .A(n604), .B(pi55), .Z(n358));
AN2 U378 ( .A(n359), .B(n358), .Z(n602));
AN2 U379 ( .A(pi53), .B(n602), .Z(n360));
AN2 U380 ( .A(n361), .B(n360), .Z(n577));
IV2 U381 ( .A(pi20), .Z(n607));
OR2 U382 ( .A(n607), .B(pi25), .Z(n362));
IV2 U383 ( .A(n362), .Z(n365));
AN2 U384 ( .A(pi25), .B(n607), .Z(n363));
OR2 U385 ( .A(n365), .B(n363), .Z(n367));
AN2 U386 ( .A(pi41), .B(pi24), .Z(n378));
AN2 U387 ( .A(n346), .B(n378), .Z(n366));
AN2 U388 ( .A(n367), .B(n366), .Z(n373));
AN2 U389 ( .A(pi28), .B(pi54), .Z(n368));
AN2 U390 ( .A(pi20), .B(n368), .Z(n603));
AN2 U391 ( .A(pi08), .B(n603), .Z(n371));
IV2 U392 ( .A(pi56), .Z(n694));
IV2 U393 ( .A(n369), .Z(n692));
OR2 U394 ( .A(n694), .B(n692), .Z(n370));
AN2 U395 ( .A(n371), .B(n370), .Z(n372));
OR2 U396 ( .A(n373), .B(n372), .Z(n424));
AN2 U397 ( .A(pi14), .B(n424), .Z(n384));
AN2 U398 ( .A(pi56), .B(pi48), .Z(n608));
AN2 U399 ( .A(n608), .B(n346), .Z(n374));
AN2 U400 ( .A(pi07), .B(n374), .Z(n376));
IV2 U401 ( .A(pi43), .Z(n375));
AN2 U402 ( .A(n376), .B(n375), .Z(n406));
AN2 U403 ( .A(pi20), .B(n406), .Z(n403));
IV2 U404 ( .A(n378), .Z(n379));
AN2 U405 ( .A(n346), .B(n379), .Z(n407));
AN2 U406 ( .A(pi55), .B(n407), .Z(n399));
AN2 U407 ( .A(pi44), .B(n399), .Z(n381));
AN2 U408 ( .A(pi37), .B(pi54), .Z(n380));
OR2 U409 ( .A(n381), .B(n380), .Z(n382));
OR2 U410 ( .A(n403), .B(n382), .Z(n383));
OR2 U411 ( .A(n384), .B(n383), .Z(n436));
AN2 U412 ( .A(pi26), .B(n436), .Z(n385));
OR2 U413 ( .A(n577), .B(n385), .Z(n386));
AN2 U414 ( .A(pi34), .B(n386), .Z(n448));
AN2 U415 ( .A(pi43), .B(pi05), .Z(n388));
AN2 U416 ( .A(pi32), .B(n436), .Z(n387));
OR2 U417 ( .A(n388), .B(n387), .Z(n446));
AN2 U418 ( .A(pi08), .B(pi37), .Z(n393));
AN2 U419 ( .A(pi50), .B(n399), .Z(n390));
AN2 U420 ( .A(pi18), .B(n424), .Z(n389));
OR2 U421 ( .A(n390), .B(n389), .Z(n391));
OR2 U422 ( .A(n403), .B(n391), .Z(n392));
OR2 U423 ( .A(n393), .B(n392), .Z(n494));
AN2 U424 ( .A(pi27), .B(n494), .Z(n497));
OR2 U425 ( .A(pi27), .B(n494), .Z(n499));
AN2 U426 ( .A(pi20), .B(pi37), .Z(n398));
AN2 U427 ( .A(pi45), .B(n399), .Z(n395));
AN2 U428 ( .A(pi22), .B(n424), .Z(n394));
OR2 U429 ( .A(n395), .B(n394), .Z(n396));
OR2 U430 ( .A(n403), .B(n396), .Z(n397));
OR2 U431 ( .A(n398), .B(n397), .Z(n536));
AN2 U432 ( .A(pi17), .B(n536), .Z(n539));
OR2 U433 ( .A(pi17), .B(n536), .Z(n541));
AN2 U434 ( .A(pi23), .B(n424), .Z(n405));
AN2 U435 ( .A(pi30), .B(pi37), .Z(n401));
AN2 U436 ( .A(pi29), .B(n399), .Z(n400));
OR2 U437 ( .A(n401), .B(n400), .Z(n402));
OR2 U438 ( .A(n403), .B(n402), .Z(n404));
OR2 U439 ( .A(n405), .B(n404), .Z(n579));
AN2 U440 ( .A(pi21), .B(n579), .Z(n582));
OR2 U441 ( .A(pi21), .B(n579), .Z(n584));
AN2 U442 ( .A(n406), .B(pi55), .Z(n429));
IV2 U443 ( .A(pi28), .Z(n409));
AN2 U444 ( .A(n407), .B(pi20), .Z(n408));
OR2 U445 ( .A(n409), .B(n408), .Z(n423));
AN2 U446 ( .A(pi50), .B(n423), .Z(n411));
AN2 U447 ( .A(pi42), .B(n424), .Z(n410));
OR2 U448 ( .A(n411), .B(n410), .Z(n412));
OR2 U449 ( .A(n429), .B(n412), .Z(n514));
AN2 U450 ( .A(pi15), .B(n514), .Z(n517));
OR2 U451 ( .A(pi15), .B(n514), .Z(n519));
AN2 U452 ( .A(pi45), .B(n423), .Z(n414));
AN2 U453 ( .A(pi40), .B(n424), .Z(n413));
OR2 U454 ( .A(n414), .B(n413), .Z(n416));
OR2 U455 ( .A(n429), .B(n416), .Z(n556));
AN2 U456 ( .A(pi03), .B(n556), .Z(n559));
OR2 U457 ( .A(pi03), .B(n556), .Z(n561));
AN2 U458 ( .A(pi29), .B(n423), .Z(n418));
AN2 U459 ( .A(pi04), .B(n424), .Z(n417));
OR2 U460 ( .A(n418), .B(n417), .Z(n419));
OR2 U461 ( .A(n429), .B(n419), .Z(n471));
AN2 U462 ( .A(pi10), .B(n471), .Z(n480));
OR2 U463 ( .A(pi10), .B(n471), .Z(n482));
AN2 U464 ( .A(pi46), .B(n482), .Z(n420));
OR2 U465 ( .A(n480), .B(n420), .Z(n562));
AN2 U466 ( .A(n561), .B(n562), .Z(n421));
OR2 U467 ( .A(n559), .B(n421), .Z(n520));
AN2 U468 ( .A(n519), .B(n520), .Z(n422));
OR2 U469 ( .A(n517), .B(n422), .Z(n449));
AN2 U470 ( .A(pi44), .B(n423), .Z(n426));
AN2 U471 ( .A(pi49), .B(n424), .Z(n425));
OR2 U472 ( .A(n426), .B(n425), .Z(n428));
OR2 U473 ( .A(n429), .B(n428), .Z(n464));
AN2 U474 ( .A(n449), .B(n464), .Z(n432));
OR2 U475 ( .A(n449), .B(n464), .Z(n430));
AN2 U476 ( .A(pi09), .B(n430), .Z(n431));
OR2 U477 ( .A(n432), .B(n431), .Z(n585));
AN2 U478 ( .A(n584), .B(n585), .Z(n433));
OR2 U479 ( .A(n582), .B(n433), .Z(n542));
AN2 U480 ( .A(n541), .B(n542), .Z(n434));
OR2 U481 ( .A(n539), .B(n434), .Z(n500));
AN2 U482 ( .A(n499), .B(n500), .Z(n435));
OR2 U483 ( .A(n497), .B(n435), .Z(n597));
OR2 U484 ( .A(pi34), .B(n436), .Z(n598));
AN2 U485 ( .A(n436), .B(pi34), .Z(n600));
IV2 U486 ( .A(n600), .Z(n437));
AN2 U487 ( .A(n598), .B(n437), .Z(n442));
OR2 U488 ( .A(n597), .B(n442), .Z(n440));
AN2 U489 ( .A(n597), .B(n442), .Z(n438));
IV2 U490 ( .A(n438), .Z(n439));
AN2 U491 ( .A(n440), .B(n439), .Z(n441));
AN2 U492 ( .A(pi12), .B(n441), .Z(n444));
AN2 U493 ( .A(n442), .B(pi19), .Z(n443));
OR2 U494 ( .A(n444), .B(n443), .Z(n445));
OR2 U495 ( .A(n446), .B(n445), .Z(n447));
OR2 U496 ( .A(n448), .B(n447), .Z(n137));
IV2 U497 ( .A(n464), .Z(n459));
AN2 U498 ( .A(pi12), .B(n449), .Z(n456));
AN2 U499 ( .A(n459), .B(n456), .Z(n453));
IV2 U500 ( .A(n449), .Z(n450));
AN2 U501 ( .A(n450), .B(pi12), .Z(n451));
OR2 U502 ( .A(pi19), .B(n451), .Z(n458));
AN2 U503 ( .A(n464), .B(n458), .Z(n452));
OR2 U504 ( .A(n453), .B(n452), .Z(n455));
IV2 U505 ( .A(pi09), .Z(n612));
AN2 U506 ( .A(n455), .B(n612), .Z(n470));
OR2 U507 ( .A(pi26), .B(n456), .Z(n457));
AN2 U508 ( .A(n464), .B(n457), .Z(n462));
AN2 U509 ( .A(n459), .B(n458), .Z(n460));
OR2 U510 ( .A(n577), .B(n460), .Z(n461));
OR2 U511 ( .A(n462), .B(n461), .Z(n463));
AN2 U512 ( .A(pi09), .B(n463), .Z(n468));
AN2 U513 ( .A(pi23), .B(pi05), .Z(n466));
AN2 U514 ( .A(pi32), .B(n464), .Z(n465));
OR2 U515 ( .A(n466), .B(n465), .Z(n467));
OR2 U516 ( .A(n468), .B(n467), .Z(n469));
OR2 U517 ( .A(n470), .B(n469), .Z(n295));
AN2 U518 ( .A(pi26), .B(n480), .Z(n479));
AN2 U519 ( .A(pi40), .B(pi05), .Z(n473));
AN2 U520 ( .A(pi32), .B(n471), .Z(n472));
OR2 U521 ( .A(n473), .B(n472), .Z(n477));
AN2 U522 ( .A(pi38), .B(pi36), .Z(n475));
AN2 U523 ( .A(pi10), .B(n577), .Z(n474));
OR2 U524 ( .A(n475), .B(n474), .Z(n476));
OR2 U525 ( .A(n477), .B(n476), .Z(n478));
OR2 U526 ( .A(n479), .B(n478), .Z(n491));
IV2 U527 ( .A(n480), .Z(n481));
AN2 U528 ( .A(n482), .B(n481), .Z(n487));
OR2 U529 ( .A(pi46), .B(n487), .Z(n485));
AN2 U530 ( .A(pi46), .B(n487), .Z(n483));
IV2 U531 ( .A(n483), .Z(n484));
AN2 U532 ( .A(n485), .B(n484), .Z(n486));
AN2 U533 ( .A(pi12), .B(n486), .Z(n489));
AN2 U534 ( .A(n487), .B(pi19), .Z(n488));
OR2 U535 ( .A(n489), .B(n488), .Z(n490));
OR2 U536 ( .A(n491), .B(n490), .Z(n351));
AN2 U537 ( .A(pi26), .B(n494), .Z(n492));
OR2 U538 ( .A(n577), .B(n492), .Z(n493));
AN2 U539 ( .A(pi27), .B(n493), .Z(n511));
AN2 U540 ( .A(pi14), .B(pi05), .Z(n496));
AN2 U541 ( .A(pi32), .B(n494), .Z(n495));
OR2 U542 ( .A(n496), .B(n495), .Z(n509));
IV2 U543 ( .A(n497), .Z(n498));
AN2 U544 ( .A(n499), .B(n498), .Z(n505));
OR2 U545 ( .A(n500), .B(n505), .Z(n503));
AN2 U546 ( .A(n500), .B(n505), .Z(n501));
IV2 U547 ( .A(n501), .Z(n502));
AN2 U548 ( .A(n503), .B(n502), .Z(n504));
AN2 U549 ( .A(pi12), .B(n504), .Z(n507));
AN2 U550 ( .A(n505), .B(pi19), .Z(n506));
OR2 U551 ( .A(n507), .B(n506), .Z(n508));
OR2 U552 ( .A(n509), .B(n508), .Z(n510));
OR2 U553 ( .A(n511), .B(n510), .Z(n364));
AN2 U554 ( .A(pi26), .B(n514), .Z(n512));
OR2 U555 ( .A(n577), .B(n512), .Z(n513));
AN2 U556 ( .A(pi15), .B(n513), .Z(n533));
AN2 U557 ( .A(pi49), .B(pi05), .Z(n531));
AN2 U558 ( .A(pi33), .B(pi36), .Z(n516));
AN2 U559 ( .A(pi32), .B(n514), .Z(n515));
OR2 U560 ( .A(n516), .B(n515), .Z(n529));
IV2 U561 ( .A(n517), .Z(n518));
AN2 U562 ( .A(n519), .B(n518), .Z(n525));
OR2 U563 ( .A(n520), .B(n525), .Z(n523));
AN2 U564 ( .A(n520), .B(n525), .Z(n521));
IV2 U565 ( .A(n521), .Z(n522));
AN2 U566 ( .A(n523), .B(n522), .Z(n524));
AN2 U567 ( .A(pi12), .B(n524), .Z(n527));
AN2 U568 ( .A(n525), .B(pi19), .Z(n526));
OR2 U569 ( .A(n527), .B(n526), .Z(n528));
OR2 U570 ( .A(n529), .B(n528), .Z(n530));
OR2 U571 ( .A(n531), .B(n530), .Z(n532));
OR2 U572 ( .A(n533), .B(n532), .Z(n377));
AN2 U573 ( .A(pi26), .B(n536), .Z(n534));
OR2 U574 ( .A(n577), .B(n534), .Z(n535));
AN2 U575 ( .A(pi17), .B(n535), .Z(n553));
AN2 U576 ( .A(pi18), .B(pi05), .Z(n538));
AN2 U577 ( .A(pi32), .B(n536), .Z(n537));
OR2 U578 ( .A(n538), .B(n537), .Z(n551));
IV2 U579 ( .A(n539), .Z(n540));
AN2 U580 ( .A(n541), .B(n540), .Z(n547));
OR2 U581 ( .A(n542), .B(n547), .Z(n545));
AN2 U582 ( .A(n542), .B(n547), .Z(n543));
IV2 U583 ( .A(n543), .Z(n544));
AN2 U584 ( .A(n545), .B(n544), .Z(n546));
AN2 U585 ( .A(pi12), .B(n546), .Z(n549));
AN2 U586 ( .A(n547), .B(pi19), .Z(n548));
OR2 U587 ( .A(n549), .B(n548), .Z(n550));
OR2 U588 ( .A(n551), .B(n550), .Z(n552));
OR2 U589 ( .A(n553), .B(n552), .Z(n415));
AN2 U590 ( .A(pi26), .B(n556), .Z(n554));
OR2 U591 ( .A(n577), .B(n554), .Z(n555));
AN2 U592 ( .A(pi03), .B(n555), .Z(n575));
AN2 U593 ( .A(pi42), .B(pi05), .Z(n573));
AN2 U594 ( .A(pi47), .B(pi36), .Z(n558));
AN2 U595 ( .A(pi32), .B(n556), .Z(n557));
OR2 U596 ( .A(n558), .B(n557), .Z(n571));
IV2 U597 ( .A(n559), .Z(n560));
AN2 U598 ( .A(n561), .B(n560), .Z(n567));
OR2 U599 ( .A(n562), .B(n567), .Z(n565));
AN2 U600 ( .A(n562), .B(n567), .Z(n563));
IV2 U601 ( .A(n563), .Z(n564));
AN2 U602 ( .A(n565), .B(n564), .Z(n566));
AN2 U603 ( .A(pi12), .B(n566), .Z(n569));
AN2 U604 ( .A(n567), .B(pi19), .Z(n568));
OR2 U605 ( .A(n569), .B(n568), .Z(n570));
OR2 U606 ( .A(n571), .B(n570), .Z(n572));
OR2 U607 ( .A(n573), .B(n572), .Z(n574));
OR2 U608 ( .A(n575), .B(n574), .Z(n427));
AN2 U609 ( .A(pi26), .B(n579), .Z(n576));
OR2 U610 ( .A(n577), .B(n576), .Z(n578));
AN2 U611 ( .A(pi21), .B(n578), .Z(n596));
AN2 U612 ( .A(pi22), .B(pi05), .Z(n581));
AN2 U613 ( .A(pi32), .B(n579), .Z(n580));
OR2 U614 ( .A(n581), .B(n580), .Z(n594));
IV2 U615 ( .A(n582), .Z(n583));
AN2 U616 ( .A(n584), .B(n583), .Z(n590));
OR2 U617 ( .A(n585), .B(n590), .Z(n588));
AN2 U618 ( .A(n585), .B(n590), .Z(n586));
IV2 U619 ( .A(n586), .Z(n587));
AN2 U620 ( .A(n588), .B(n587), .Z(n589));
AN2 U621 ( .A(pi12), .B(n589), .Z(n592));
AN2 U622 ( .A(n590), .B(pi19), .Z(n591));
OR2 U623 ( .A(n592), .B(n591), .Z(n593));
OR2 U624 ( .A(n594), .B(n593), .Z(n595));
OR2 U625 ( .A(n596), .B(n595), .Z(n454));
AN2 U626 ( .A(n598), .B(n597), .Z(n599));
OR2 U627 ( .A(n600), .B(n599), .Z(po07));
OR2 U628 ( .A(pi58), .B(pi00), .Z(n609));
AN2 U629 ( .A(pi59), .B(n609), .Z(po24));
AN2 U630 ( .A(n602), .B(pi57), .Z(n601));
AN2 U631 ( .A(pi41), .B(n601), .Z(po13));
AN2 U632 ( .A(pi48), .B(n602), .Z(po08));
AN2 U633 ( .A(n603), .B(pi31), .Z(po03));
AN2 U634 ( .A(pi48), .B(pi16), .Z(n610));
AN2 U635 ( .A(pi25), .B(n610), .Z(po25));
AN2 U636 ( .A(pi11), .B(n604), .Z(n605));
IV2 U637 ( .A(n605), .Z(n606));
OR2 U638 ( .A(n607), .B(n606), .Z(n691));
OR2 U639 ( .A(po25), .B(n691), .Z(po02));
AN2 U640 ( .A(n608), .B(pi25), .Z(po10));
AN2 U641 ( .A(pi13), .B(n609), .Z(po12));
AN2 U642 ( .A(pi07), .B(n610), .Z(po14));
IV2 U643 ( .A(pi15), .Z(n611));
AN2 U644 ( .A(pi09), .B(n611), .Z(n614));
AN2 U645 ( .A(pi15), .B(n612), .Z(n613));
OR2 U646 ( .A(n614), .B(n613), .Z(n618));
IV2 U647 ( .A(pi35), .Z(n654));
OR2 U648 ( .A(n654), .B(pi06), .Z(n617));
IV2 U649 ( .A(pi06), .Z(n615));
OR2 U650 ( .A(n615), .B(pi35), .Z(n616));
AN2 U651 ( .A(n617), .B(n616), .Z(n619));
OR2 U652 ( .A(n618), .B(n619), .Z(n622));
AN2 U653 ( .A(n619), .B(n618), .Z(n620));
IV2 U654 ( .A(n620), .Z(n621));
AN2 U655 ( .A(n622), .B(n621), .Z(n628));
IV2 U656 ( .A(pi10), .Z(n624));
OR2 U657 ( .A(n624), .B(pi03), .Z(n623));
IV2 U658 ( .A(n623), .Z(n626));
AN2 U659 ( .A(pi03), .B(n624), .Z(n625));
OR2 U660 ( .A(n626), .B(n625), .Z(n627));
OR2 U661 ( .A(n628), .B(n627), .Z(n631));
AN2 U662 ( .A(n628), .B(n627), .Z(n629));
IV2 U663 ( .A(n629), .Z(n630));
AN2 U664 ( .A(n631), .B(n630), .Z(n637));
IV2 U665 ( .A(pi34), .Z(n632));
AN2 U666 ( .A(pi27), .B(n632), .Z(n635));
OR2 U667 ( .A(n632), .B(pi27), .Z(n633));
IV2 U668 ( .A(n633), .Z(n634));
OR2 U669 ( .A(n635), .B(n634), .Z(n636));
OR2 U670 ( .A(n637), .B(n636), .Z(n640));
AN2 U671 ( .A(n637), .B(n636), .Z(n638));
IV2 U672 ( .A(n638), .Z(n639));
AN2 U673 ( .A(n640), .B(n639), .Z(n647));
IV2 U674 ( .A(pi21), .Z(n642));
OR2 U675 ( .A(n642), .B(pi17), .Z(n641));
IV2 U676 ( .A(n641), .Z(n644));
AN2 U677 ( .A(pi17), .B(n642), .Z(n643));
OR2 U678 ( .A(n644), .B(n643), .Z(n646));
OR2 U679 ( .A(n647), .B(n646), .Z(n645));
IV2 U680 ( .A(n645), .Z(n649));
AN2 U681 ( .A(n647), .B(n646), .Z(n648));
OR2 U682 ( .A(n649), .B(n648), .Z(po15));
IV2 U683 ( .A(pi42), .Z(n650));
AN2 U684 ( .A(pi49), .B(n650), .Z(n653));
IV2 U685 ( .A(pi49), .Z(n651));
AN2 U686 ( .A(pi42), .B(n651), .Z(n652));
OR2 U687 ( .A(n653), .B(n652), .Z(n658));
OR2 U688 ( .A(n654), .B(pi39), .Z(n657));
IV2 U689 ( .A(pi39), .Z(n655));
OR2 U690 ( .A(n655), .B(pi35), .Z(n656));
AN2 U691 ( .A(n657), .B(n656), .Z(n659));
OR2 U692 ( .A(n658), .B(n659), .Z(n662));
AN2 U693 ( .A(n659), .B(n658), .Z(n660));
IV2 U694 ( .A(n660), .Z(n661));
AN2 U695 ( .A(n662), .B(n661), .Z(n668));
IV2 U696 ( .A(pi04), .Z(n664));
OR2 U697 ( .A(n664), .B(pi18), .Z(n663));
IV2 U698 ( .A(n663), .Z(n666));
AN2 U699 ( .A(pi18), .B(n664), .Z(n665));
OR2 U700 ( .A(n666), .B(n665), .Z(n667));
OR2 U701 ( .A(n668), .B(n667), .Z(n671));
AN2 U702 ( .A(n668), .B(n667), .Z(n669));
IV2 U703 ( .A(n669), .Z(n670));
AN2 U704 ( .A(n671), .B(n670), .Z(n677));
IV2 U705 ( .A(pi22), .Z(n673));
OR2 U706 ( .A(n673), .B(pi14), .Z(n672));
IV2 U707 ( .A(n672), .Z(n675));
AN2 U708 ( .A(pi14), .B(n673), .Z(n674));
OR2 U709 ( .A(n675), .B(n674), .Z(n676));
OR2 U710 ( .A(n677), .B(n676), .Z(n680));
AN2 U711 ( .A(n677), .B(n676), .Z(n678));
IV2 U712 ( .A(n678), .Z(n679));
AN2 U713 ( .A(n680), .B(n679), .Z(n687));
IV2 U714 ( .A(pi40), .Z(n682));
OR2 U715 ( .A(n682), .B(pi23), .Z(n681));
IV2 U716 ( .A(n681), .Z(n684));
AN2 U717 ( .A(pi23), .B(n682), .Z(n683));
OR2 U718 ( .A(n684), .B(n683), .Z(n686));
OR2 U719 ( .A(n687), .B(n686), .Z(n685));
IV2 U720 ( .A(n685), .Z(n689));
AN2 U721 ( .A(n687), .B(n686), .Z(n688));
OR2 U722 ( .A(n689), .B(n688), .Z(po20));
AN2 U723 ( .A(pi01), .B(pi02), .Z(po21));
IV2 U724 ( .A(po25), .Z(n690));
OR2 U725 ( .A(n691), .B(n690), .Z(po23));
IV2 U726 ( .A(pi16), .Z(n696));
OR2 U727 ( .A(n692), .B(n696), .Z(po11));
AN2 U728 ( .A(pi07), .B(pi41), .Z(n693));
IV2 U729 ( .A(n693), .Z(n695));
OR2 U730 ( .A(n694), .B(n695), .Z(po01));
OR2 U731 ( .A(n696), .B(n695), .Z(po05));
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

41
examples/smtbmc/glift/C880.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog C880.v
techmap
flatten
select C880_lev2
glift -create-instrumented-model
techmap
opt
rename C880_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog C880.v
techmap
flatten
select C880_lev2
glift -create-precise-model
techmap
opt
rename C880_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution C880.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file C880.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

400
examples/smtbmc/glift/alu2.v Executable file
View file

@ -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

41
examples/smtbmc/glift/alu2.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog alu2.v
techmap
flatten
select alu2_lev2
glift -create-instrumented-model
techmap
opt
rename alu2_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog alu2.v
techmap
flatten
select alu2_lev2
glift -create-precise-model
techmap
opt
rename alu2_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution alu2.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file alu2.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

802
examples/smtbmc/glift/alu4.v Executable file
View file

@ -0,0 +1,802 @@
module alu4_lev2(pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09,
pi10, pi11, pi12, pi13, po0, po1, po2, po3, po4, po5, po6, po7);
input pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09,
pi10, pi11, pi12, pi13;
output po0, po1, po2, po3, po4, po5, po6, po7;
wire n705, n706, n707, n708, n709, n710, n711, n712, n713, n714,
n715, n716, n717, n718, n719, n720, n721, n722, n723, n724,
n725, n726, n727, n728, n729, n730, n731, n732, n733, n734,
n735, n736, n737, n738, n739, n740, n741, n742, n743, n744,
n745, n746, n747, n748, n749, n750, n751, n752, n753, n754,
n755, n756, n757, n758, n759, n760, n761, n762, n763, n764,
n765, n766, n767, n768, n769, n770, n771, n772, n773, n774,
n775, n776, n777, n778, n779, n780, n781, n782, n783, n784,
n785, n786, n787, n788, n789, n790, n791, n792, n793, n794,
n795, n796, n797, n798, n799, n800, n801, n802, n803, n804,
n805, n806, n807, n808, n809, n810, n811, n812, n813, n814,
n815, n816, n817, n818, n819, n820, n821, n822, n823, n824,
n825, n826, n827, n828, n829, n830, n831, n832, n833, n834,
n835, n836, n837, n838, n839, n840, n841, n842, n843, n844,
n845, n846, n847, n848, n849, n850, n851, n852, n853, n854,
n855, n856, n857, n858, n859, n860, n861, n862, n863, n864,
n865, n866, n867, n868, n869, n870, n871, n872, n873, n874,
n875, n876, n877, n878, n879, n880, n881, n882, n883, n884,
n885, n886, n887, n888, n889, n890, n891, n892, n893, n894,
n895, n896, n897, n898, n899, n900, n901, n902, n903, n904,
n905, n906, n907, n908, n909, n910, n911, n912, n913, n914,
n915, n916, n917, n918, n919, n920, n921, n922, n923, n924,
n925, n926, n927, n928, n929, n930, n931, n932, n933, n934,
n935, n936, n937, n938, n939, n940, n941, n942, n943, n944,
n945, n946, n947, n948, n949, n950, n951, n952, n953, n954,
n955, n956, n957, n958, n959, n960, n961, n962, n963, n964,
n965, n966, n967, n968, n969, n970, n971, n972, n973, n974,
n975, n976, n977, n978, n979, n980, n981, n982, n983, n984,
n985, n986, n987, n988, n989, n990, n991, n992, n993, n994,
n995, n996, n997, n998, n999, n1000, n1001, n1002, n1003, n1004,
n1005, n1006, n1007, n1008, n1009, n1010, n1011, n1012, n1013, n1014,
n1015, n1016, n1017, n1018, n1019, n1020, n1021, n1022, n1023, n1024,
n1025, n1026, n1027, n1028, n1029, n1030, n1031, n1032, n1033, n1034,
n1035, n1036, n1037, n1038, n1039, n1040, n1041, n1042, n1043, n1044,
n1045, n1046, n1047, n1048, n1049, n1050, n1051, n1052, n1053, n1054,
n1055, n1056, n1057, n1058, n1059, n1060, n1061, n1062, n1063, n1064,
n1065, n1066, n1067, n1068, n1069, n1070, n1071, n1072, n1073, n1074,
n1075, n1076, n1077, n1078, n1079, n1080, n1081, n1082, n1083, n1084,
n1085, n1086, n1087, n1088, n1089, n1090, n1091, n1092, n1093, n1094,
n1095, n1096, n1097, n1098, n1099, n1100, n1101, n1102, n1103, n1104,
n1105, n1106, n1107, n1108, n1109, n1110, n1111, n1112, n1113, n1114,
n1115, n1116, n1117, n1118, n1119, n1120, n1121, n1122, n1123, n1124,
n1125, n1126, n1127, n1128, n1129, n1130, n1131, n1132, n1133, n1134,
n1135, n1136, n1137, n1138, n1139, n1140, n1141, n1142, n1143, n1144,
n1145, n1146, n1147, n1148, n1149, n1150, n1151, n1152, n1153, n1154,
n1155, n1156, n1157, n1158, n1159, n1160, n1161, n1162, n1163, n1164,
n1165, n1166, n1167, n1168, n1169, n1170, n1171, n1172, n1173, n1174,
n1175, n1176, n1177, n1178, n1179, n1180, n1181, n1182, n1183, n1184,
n1185, n1186, n1187, n1188, n1189, n1190, n1191, n1192, n1193, n1194,
n1195, n1196, n1197, n1198, n1199, n1200, n1201, n1202, n1203, n1204,
n1205, n1206, n1207, n1208, n1209, n1210, n1211, n1212, n1213, n1214,
n1215, n1216, n1217, n1218, n1219, n1220, n1221, n1222, n1223, n1224,
n1225, n1226, n1227, n1228, n1229, n1230, n1231, n1232, n1233, n1234,
n1235, n1236, n1237, n1238, n1239, n1240, n1241, n1242, n1243, n1244,
n1245, n1246, n1247, n1248, n1249, n1250, n1251, n1252, n1253, n1254,
n1255, n1256, n1257, n1258, n1259, n1260, n1261, n1262, n1263, n1264,
n1265, n1266, n1267, n1268, n1269, n1270, n1271, n1272, n1273, n1274,
n1275, n1276, n1277, n1278, n1279, n1280, n1281, n1282, n1283, n1284,
n1285, n1286, n1287, n1288, n1289, n1290, n1291, n1292, n1293, n1294,
n1295, n1296, n1297, n1298, n1299, n1300, n1301, n1302, n1303, n1304,
n1305, n1306, n1307, n1308, n1309, n1310, n1311, n1312, n1313, n1314,
n1315, n1316, n1317, n1318, n1319, n1320, n1321, n1322, n1323, n1324,
n1325, n1326, n1327, n1328, n1329, n1330, n1331, n1332, n1333, n1334,
n1335, n1336, n1337, n1338, n1339, n1340, n1341, n1342, n1343, n1344,
n1345, n1346, n1347, n1348, n1349, n1350, n1351, n1352, n1353, n1354,
n1355, n1356, n1357, n1358, n1359, n1360, n1361, n1362, n1363, n1364,
n1365, n1366, n1367, n1368, n1369, n1370, n1371, n1372, n1373, n1374,
n1375, n1376, n1377, n1378, n1379, n1380, n1381, n1382, n1383, n1384,
n1385, n1386, n1387, n1388, n1389, n1390, n1391, n1392, n1393, n1394,
n1395, n1396;
AN2 U712 ( .A(n705), .B(po4), .Z(po7));
OR2 U713 ( .A(n706), .B(n707), .Z(n705));
AN2 U714 ( .A(n708), .B(n709), .Z(n707));
OR2 U715 ( .A(n710), .B(n711), .Z(n708));
AN2 U716 ( .A(n712), .B(n713), .Z(n711));
AN2 U717 ( .A(n714), .B(n715), .Z(n710));
AN2 U718 ( .A(n716), .B(n717), .Z(n714));
AN2 U719 ( .A(n718), .B(n719), .Z(n706));
OR2 U720 ( .A(n720), .B(n712), .Z(n719));
OR2 U721 ( .A(n721), .B(n722), .Z(n712));
AN2 U722 ( .A(n723), .B(n724), .Z(n722));
AN2 U723 ( .A(n725), .B(n726), .Z(n721));
OR2 U724 ( .A(n724), .B(n727), .Z(n726));
AN2 U725 ( .A(n727), .B(n723), .Z(n720));
OR2 U726 ( .A(n728), .B(n729), .Z(po6));
AN2 U727 ( .A(pi13), .B(n730), .Z(n729));
OR2 U728 ( .A(n731), .B(n732), .Z(n730));
OR2 U729 ( .A(n733), .B(n734), .Z(n732));
OR2 U730 ( .A(n735), .B(n736), .Z(n734));
AN2 U731 ( .A(n737), .B(n738), .Z(n736));
OR2 U732 ( .A(n739), .B(n740), .Z(n737));
OR2 U733 ( .A(n741), .B(n742), .Z(n740));
AN2 U734 ( .A(n743), .B(n744), .Z(n742));
OR2 U735 ( .A(n745), .B(n746), .Z(n743));
AN2 U736 ( .A(pi03), .B(n747), .Z(n745));
AN2 U737 ( .A(n748), .B(n749), .Z(n741));
AN2 U738 ( .A(n750), .B(n751), .Z(n748));
AN2 U739 ( .A(pi11), .B(n752), .Z(n735));
OR2 U740 ( .A(n753), .B(n754), .Z(n752));
OR2 U741 ( .A(n755), .B(n756), .Z(n754));
AN2 U742 ( .A(n757), .B(n747), .Z(n756));
OR2 U743 ( .A(n758), .B(n759), .Z(n757));
IV2 U744 ( .A(n760), .Z(n755));
AN2 U745 ( .A(n761), .B(n762), .Z(n753));
OR2 U746 ( .A(n763), .B(po5), .Z(n762));
AN2 U747 ( .A(n764), .B(n765), .Z(n763));
AN2 U748 ( .A(n766), .B(n767), .Z(n733));
OR2 U749 ( .A(n768), .B(n769), .Z(n767));
AN2 U750 ( .A(n770), .B(n771), .Z(n768));
IV2 U751 ( .A(n772), .Z(n766));
OR2 U752 ( .A(n773), .B(n774), .Z(n731));
AN2 U753 ( .A(n775), .B(n776), .Z(n774));
AN2 U754 ( .A(n777), .B(n778), .Z(n775));
AN2 U755 ( .A(n779), .B(n780), .Z(n773));
AN2 U756 ( .A(n781), .B(n782), .Z(n779));
AN2 U757 ( .A(n783), .B(n781), .Z(n728));
AN2 U758 ( .A(n782), .B(n784), .Z(n783));
OR2 U759 ( .A(n785), .B(n786), .Z(po3));
OR2 U760 ( .A(n787), .B(n788), .Z(n786));
OR2 U761 ( .A(n789), .B(n790), .Z(n788));
OR2 U762 ( .A(n791), .B(n792), .Z(n790));
AN2 U763 ( .A(n793), .B(n782), .Z(n792));
AN2 U764 ( .A(n794), .B(n795), .Z(n791));
OR2 U765 ( .A(n796), .B(n797), .Z(n789));
IV2 U766 ( .A(n798), .Z(n797));
OR2 U767 ( .A(n799), .B(n778), .Z(n798));
AN2 U768 ( .A(n778), .B(n799), .Z(n796));
OR2 U769 ( .A(n800), .B(n801), .Z(n799));
IV2 U770 ( .A(n802), .Z(n778));
OR2 U771 ( .A(n803), .B(n804), .Z(n802));
AN2 U772 ( .A(n805), .B(n806), .Z(n803));
AN2 U773 ( .A(n807), .B(n808), .Z(n806));
AN2 U774 ( .A(n809), .B(n810), .Z(n808));
OR2 U775 ( .A(pi11), .B(n811), .Z(n810));
AN2 U776 ( .A(n812), .B(n813), .Z(n811));
AN2 U777 ( .A(n814), .B(n815), .Z(n813));
OR2 U778 ( .A(n782), .B(n816), .Z(n815));
OR2 U779 ( .A(n817), .B(n818), .Z(n814));
OR2 U780 ( .A(n819), .B(n820), .Z(n818));
AN2 U781 ( .A(n750), .B(n821), .Z(n820));
AN2 U782 ( .A(n749), .B(n747), .Z(n819));
IV2 U783 ( .A(n821), .Z(n749));
AN2 U784 ( .A(n822), .B(n823), .Z(n812));
OR2 U785 ( .A(n824), .B(n825), .Z(n823));
OR2 U786 ( .A(n826), .B(n827), .Z(n822));
AN2 U787 ( .A(pi10), .B(n828), .Z(n826));
OR2 U788 ( .A(n829), .B(n830), .Z(n828));
OR2 U789 ( .A(n831), .B(n738), .Z(n809));
AN2 U790 ( .A(n832), .B(n833), .Z(n831));
AN2 U791 ( .A(n834), .B(n760), .Z(n833));
OR2 U792 ( .A(n817), .B(n835), .Z(n760));
OR2 U793 ( .A(pi03), .B(n836), .Z(n835));
OR2 U794 ( .A(n817), .B(n837), .Z(n834));
OR2 U795 ( .A(n715), .B(n827), .Z(n837));
IV2 U796 ( .A(n836), .Z(n715));
AN2 U797 ( .A(n838), .B(n839), .Z(n832));
OR2 U798 ( .A(n765), .B(n840), .Z(n839));
OR2 U799 ( .A(n841), .B(n825), .Z(n840));
OR2 U800 ( .A(n816), .B(n842), .Z(n838));
OR2 U801 ( .A(n843), .B(n844), .Z(n842));
AN2 U802 ( .A(n845), .B(n846), .Z(n844));
OR2 U803 ( .A(n847), .B(n848), .Z(n845));
AN2 U804 ( .A(n758), .B(n747), .Z(n848));
IV2 U805 ( .A(n849), .Z(n758));
AN2 U806 ( .A(n750), .B(n849), .Z(n847));
AN2 U807 ( .A(n849), .B(n759), .Z(n843));
OR2 U808 ( .A(n850), .B(n851), .Z(n849));
AN2 U809 ( .A(n852), .B(n853), .Z(n850));
IV2 U810 ( .A(n854), .Z(n816));
AN2 U811 ( .A(n855), .B(n856), .Z(n807));
OR2 U812 ( .A(n857), .B(n858), .Z(n856));
OR2 U813 ( .A(n859), .B(n860), .Z(n858));
AN2 U814 ( .A(n861), .B(n739), .Z(n859));
OR2 U815 ( .A(n862), .B(n863), .Z(n739));
AN2 U816 ( .A(n759), .B(n795), .Z(n862));
OR2 U817 ( .A(n846), .B(n864), .Z(n861));
IV2 U818 ( .A(n865), .Z(n864));
AN2 U819 ( .A(n795), .B(n863), .Z(n865));
IV2 U820 ( .A(n759), .Z(n846));
OR2 U821 ( .A(n866), .B(n867), .Z(n759));
AN2 U822 ( .A(n868), .B(po5), .Z(n867));
AN2 U823 ( .A(n750), .B(n869), .Z(n866));
OR2 U824 ( .A(n825), .B(n870), .Z(n855));
OR2 U825 ( .A(n871), .B(n872), .Z(n870));
AN2 U826 ( .A(n764), .B(n873), .Z(n872));
IV2 U827 ( .A(po5), .Z(n873));
AN2 U828 ( .A(n841), .B(po4), .Z(n871));
OR2 U829 ( .A(n874), .B(po5), .Z(po4));
IV2 U830 ( .A(n764), .Z(n841));
OR2 U831 ( .A(n875), .B(n724), .Z(n764));
AN2 U832 ( .A(n876), .B(n877), .Z(n875));
AN2 U833 ( .A(n878), .B(n879), .Z(n805));
AN2 U834 ( .A(n880), .B(n881), .Z(n879));
OR2 U835 ( .A(n782), .B(n882), .Z(n881));
OR2 U836 ( .A(n781), .B(n883), .Z(n882));
IV2 U837 ( .A(n884), .Z(n781));
OR2 U838 ( .A(n795), .B(n885), .Z(n880));
AN2 U839 ( .A(n886), .B(n887), .Z(n878));
OR2 U840 ( .A(pi03), .B(n888), .Z(n887));
AN2 U841 ( .A(n889), .B(n890), .Z(n888));
IV2 U842 ( .A(n891), .Z(n890));
AN2 U843 ( .A(n830), .B(n892), .Z(n891));
OR2 U844 ( .A(n893), .B(n894), .Z(n830));
IV2 U845 ( .A(n895), .Z(n894));
OR2 U846 ( .A(n746), .B(n750), .Z(n895));
AN2 U847 ( .A(n750), .B(n746), .Z(n893));
OR2 U848 ( .A(n896), .B(n897), .Z(n746));
AN2 U849 ( .A(pi02), .B(n898), .Z(n896));
IV2 U850 ( .A(n747), .Z(n750));
OR2 U851 ( .A(n899), .B(n900), .Z(n747));
AN2 U852 ( .A(n901), .B(n771), .Z(n900));
OR2 U853 ( .A(pi03), .B(n795), .Z(n771));
AN2 U854 ( .A(n902), .B(n903), .Z(n899));
OR2 U855 ( .A(n904), .B(n905), .Z(n903));
OR2 U856 ( .A(n906), .B(n907), .Z(n905));
AN2 U857 ( .A(n782), .B(n892), .Z(n907));
AN2 U858 ( .A(n769), .B(n751), .Z(n906));
AN2 U859 ( .A(po5), .B(n908), .Z(n904));
OR2 U860 ( .A(n909), .B(n772), .Z(n889));
AN2 U861 ( .A(n910), .B(n911), .Z(n909));
OR2 U862 ( .A(n912), .B(n795), .Z(n911));
OR2 U863 ( .A(n782), .B(n770), .Z(n910));
OR2 U864 ( .A(n827), .B(n913), .Z(n886));
OR2 U865 ( .A(n914), .B(n772), .Z(n913));
OR2 U866 ( .A(n915), .B(n916), .Z(n914));
AN2 U867 ( .A(n912), .B(n795), .Z(n916));
IV2 U868 ( .A(n770), .Z(n912));
AN2 U869 ( .A(n782), .B(n770), .Z(n915));
OR2 U870 ( .A(n917), .B(n918), .Z(n770));
AN2 U871 ( .A(n919), .B(n920), .Z(n917));
IV2 U872 ( .A(n795), .Z(n782));
OR2 U873 ( .A(n921), .B(n922), .Z(n787));
AN2 U874 ( .A(n923), .B(n824), .Z(n922));
AN2 U875 ( .A(n924), .B(n925), .Z(n923));
OR2 U876 ( .A(n926), .B(n927), .Z(n925));
AN2 U877 ( .A(pi11), .B(pi03), .Z(n926));
AN2 U878 ( .A(pi07), .B(n928), .Z(n921));
OR2 U879 ( .A(n929), .B(n930), .Z(n928));
AN2 U880 ( .A(n931), .B(n804), .Z(n929));
OR2 U881 ( .A(n932), .B(n933), .Z(n931));
AN2 U882 ( .A(n854), .B(n795), .Z(n933));
AN2 U883 ( .A(n934), .B(n827), .Z(n932));
OR2 U884 ( .A(n935), .B(n936), .Z(n785));
OR2 U885 ( .A(n937), .B(n938), .Z(n936));
AN2 U886 ( .A(n939), .B(n940), .Z(n938));
OR2 U887 ( .A(n941), .B(n942), .Z(n940));
OR2 U888 ( .A(n769), .B(n943), .Z(n942));
AN2 U889 ( .A(n874), .B(n944), .Z(n943));
AN2 U890 ( .A(n795), .B(pi03), .Z(n769));
OR2 U891 ( .A(n945), .B(n946), .Z(n795));
OR2 U892 ( .A(n947), .B(n948), .Z(n946));
AN2 U893 ( .A(n949), .B(n824), .Z(n948));
AN2 U894 ( .A(n950), .B(n765), .Z(n947));
IV2 U895 ( .A(n874), .Z(n765));
OR2 U896 ( .A(n951), .B(n952), .Z(n945));
OR2 U897 ( .A(n953), .B(n954), .Z(n952));
AN2 U898 ( .A(n955), .B(n827), .Z(n954));
OR2 U899 ( .A(n956), .B(n957), .Z(n955));
AN2 U900 ( .A(n958), .B(n784), .Z(n956));
AN2 U901 ( .A(pi07), .B(n959), .Z(n958));
AN2 U902 ( .A(po5), .B(n960), .Z(n953));
OR2 U903 ( .A(n961), .B(n962), .Z(n960));
AN2 U904 ( .A(n892), .B(n963), .Z(n962));
AN2 U905 ( .A(n964), .B(n965), .Z(n961));
AN2 U906 ( .A(pi13), .B(n966), .Z(n951));
OR2 U907 ( .A(n967), .B(n968), .Z(n966));
OR2 U908 ( .A(n969), .B(n970), .Z(n968));
AN2 U909 ( .A(n971), .B(pi02), .Z(n970));
AN2 U910 ( .A(n972), .B(n973), .Z(n969));
AN2 U911 ( .A(n974), .B(n975), .Z(n972));
OR2 U912 ( .A(n874), .B(n959), .Z(n975));
AN2 U913 ( .A(n827), .B(n824), .Z(n874));
IV2 U914 ( .A(pi03), .Z(n827));
OR2 U915 ( .A(n964), .B(n976), .Z(n974));
AN2 U916 ( .A(pi03), .B(n824), .Z(n976));
IV2 U917 ( .A(pi07), .Z(n824));
IV2 U918 ( .A(n959), .Z(n964));
OR2 U919 ( .A(n977), .B(n978), .Z(n959));
AN2 U920 ( .A(n979), .B(pi02), .Z(n978));
AN2 U921 ( .A(n980), .B(n717), .Z(n977));
OR2 U922 ( .A(n979), .B(pi02), .Z(n980));
AN2 U923 ( .A(n981), .B(po5), .Z(n967));
AN2 U924 ( .A(po5), .B(n982), .Z(n941));
AN2 U925 ( .A(pi03), .B(pi07), .Z(po5));
AN2 U926 ( .A(n983), .B(pi03), .Z(n935));
OR2 U927 ( .A(n984), .B(n985), .Z(po2));
OR2 U928 ( .A(n986), .B(n987), .Z(n985));
OR2 U929 ( .A(n988), .B(n989), .Z(n987));
OR2 U930 ( .A(n990), .B(n991), .Z(n989));
AN2 U931 ( .A(n793), .B(n992), .Z(n991));
AN2 U932 ( .A(n794), .B(n993), .Z(n990));
OR2 U933 ( .A(n994), .B(n995), .Z(n988));
AN2 U934 ( .A(n777), .B(n801), .Z(n995));
IV2 U935 ( .A(n800), .Z(n777));
AN2 U936 ( .A(n776), .B(n800), .Z(n994));
OR2 U937 ( .A(n996), .B(n804), .Z(n800));
AN2 U938 ( .A(n997), .B(n998), .Z(n996));
AN2 U939 ( .A(n999), .B(n1000), .Z(n998));
AN2 U940 ( .A(n1001), .B(n1002), .Z(n1000));
OR2 U941 ( .A(n1003), .B(n817), .Z(n1002));
AN2 U942 ( .A(n1004), .B(n836), .Z(n1003));
OR2 U943 ( .A(pi00), .B(n1005), .Z(n836));
OR2 U944 ( .A(pi02), .B(pi01), .Z(n1005));
AN2 U945 ( .A(n1006), .B(n1007), .Z(n1004));
OR2 U946 ( .A(pi11), .B(n1008), .Z(n1007));
AN2 U947 ( .A(n1009), .B(n821), .Z(n1008));
OR2 U948 ( .A(n898), .B(n1010), .Z(n821));
OR2 U949 ( .A(n1011), .B(n851), .Z(n1009));
AN2 U950 ( .A(n1012), .B(n1013), .Z(n1011));
OR2 U951 ( .A(n738), .B(n1014), .Z(n1006));
OR2 U952 ( .A(n1015), .B(n1016), .Z(n1014));
AN2 U953 ( .A(n713), .B(n1017), .Z(n1015));
OR2 U954 ( .A(n1018), .B(n1019), .Z(n1001));
OR2 U955 ( .A(n744), .B(n1020), .Z(n1019));
OR2 U956 ( .A(n1021), .B(n1022), .Z(n1018));
AN2 U957 ( .A(n717), .B(n1023), .Z(n1022));
AN2 U958 ( .A(n863), .B(n1024), .Z(n1021));
OR2 U959 ( .A(n1025), .B(n1026), .Z(n1024));
OR2 U960 ( .A(n992), .B(n852), .Z(n1026));
IV2 U961 ( .A(n1027), .Z(n1025));
OR2 U962 ( .A(n1028), .B(n1027), .Z(n863));
OR2 U963 ( .A(n1029), .B(n1030), .Z(n1027));
AN2 U964 ( .A(n1031), .B(n1032), .Z(n1029));
AN2 U965 ( .A(n1033), .B(n993), .Z(n1028));
AN2 U966 ( .A(n885), .B(n1034), .Z(n999));
OR2 U967 ( .A(n825), .B(n1035), .Z(n1034));
OR2 U968 ( .A(n1036), .B(n1037), .Z(n1035));
AN2 U969 ( .A(n1038), .B(n1039), .Z(n1037));
IV2 U970 ( .A(n724), .Z(n1039));
OR2 U971 ( .A(n877), .B(n738), .Z(n1038));
IV2 U972 ( .A(n876), .Z(n1036));
OR2 U973 ( .A(n1040), .B(n884), .Z(n885));
OR2 U974 ( .A(n1041), .B(n1042), .Z(n884));
OR2 U975 ( .A(n993), .B(n1032), .Z(n1042));
AN2 U976 ( .A(n1043), .B(n1044), .Z(n997));
AN2 U977 ( .A(n1045), .B(n1046), .Z(n1044));
OR2 U978 ( .A(pi02), .B(n1047), .Z(n1046));
AN2 U979 ( .A(n1048), .B(n1049), .Z(n1047));
OR2 U980 ( .A(n876), .B(n1050), .Z(n1049));
OR2 U981 ( .A(n717), .B(n825), .Z(n1050));
AN2 U982 ( .A(n1051), .B(n1052), .Z(n1048));
OR2 U983 ( .A(n1053), .B(n1054), .Z(n1052));
OR2 U984 ( .A(n1055), .B(n772), .Z(n1051));
AN2 U985 ( .A(n1056), .B(n1057), .Z(n1055));
OR2 U986 ( .A(n1058), .B(n993), .Z(n1057));
OR2 U987 ( .A(n992), .B(n919), .Z(n1056));
OR2 U988 ( .A(n1059), .B(n1016), .Z(n1045));
AN2 U989 ( .A(n1060), .B(n1061), .Z(n1059));
AN2 U990 ( .A(n1062), .B(n1063), .Z(n1061));
OR2 U991 ( .A(n876), .B(n1064), .Z(n1062));
OR2 U992 ( .A(pi06), .B(n825), .Z(n1064));
OR2 U993 ( .A(n1065), .B(n725), .Z(n876));
AN2 U994 ( .A(n718), .B(n1066), .Z(n1065));
AN2 U995 ( .A(n1067), .B(n1068), .Z(n1060));
OR2 U996 ( .A(n772), .B(n1069), .Z(n1068));
OR2 U997 ( .A(n1070), .B(n1071), .Z(n1069));
AN2 U998 ( .A(n1058), .B(n993), .Z(n1071));
IV2 U999 ( .A(n919), .Z(n1058));
AN2 U1000 ( .A(n992), .B(n919), .Z(n1070));
OR2 U1001 ( .A(n1072), .B(n1073), .Z(n919));
AN2 U1002 ( .A(n1074), .B(n1075), .Z(n1072));
OR2 U1003 ( .A(n1054), .B(n1076), .Z(n1067));
IV2 U1004 ( .A(n1053), .Z(n1076));
AN2 U1005 ( .A(n1077), .B(n1078), .Z(n1053));
OR2 U1006 ( .A(n897), .B(n851), .Z(n1078));
IV2 U1007 ( .A(n1079), .Z(n1077));
AN2 U1008 ( .A(n851), .B(n897), .Z(n1079));
OR2 U1009 ( .A(n1080), .B(n1081), .Z(n897));
AN2 U1010 ( .A(pi01), .B(n1082), .Z(n1080));
AN2 U1011 ( .A(n1083), .B(n1084), .Z(n1043));
OR2 U1012 ( .A(pi10), .B(n1085), .Z(n1084));
OR2 U1013 ( .A(n1086), .B(n1087), .Z(n1085));
AN2 U1014 ( .A(n1088), .B(n1089), .Z(n1087));
AN2 U1015 ( .A(n852), .B(n898), .Z(n1088));
IV2 U1016 ( .A(n1033), .Z(n852));
AN2 U1017 ( .A(n1090), .B(n853), .Z(n1086));
IV2 U1018 ( .A(n1089), .Z(n853));
AN2 U1019 ( .A(n1091), .B(n1082), .Z(n1089));
OR2 U1020 ( .A(n1031), .B(n1092), .Z(n1091));
OR2 U1021 ( .A(n851), .B(n1033), .Z(n1090));
OR2 U1022 ( .A(n1093), .B(n1094), .Z(n1033));
AN2 U1023 ( .A(n868), .B(n724), .Z(n1094));
AN2 U1024 ( .A(n851), .B(n869), .Z(n1093));
IV2 U1025 ( .A(n898), .Z(n851));
OR2 U1026 ( .A(n1095), .B(n1096), .Z(n898));
AN2 U1027 ( .A(n901), .B(n920), .Z(n1096));
OR2 U1028 ( .A(pi02), .B(n993), .Z(n920));
AN2 U1029 ( .A(n902), .B(n1097), .Z(n1095));
OR2 U1030 ( .A(n1098), .B(n1099), .Z(n1097));
OR2 U1031 ( .A(n1100), .B(n1101), .Z(n1099));
AN2 U1032 ( .A(n992), .B(n892), .Z(n1101));
AN2 U1033 ( .A(n918), .B(n751), .Z(n1100));
AN2 U1034 ( .A(n908), .B(n724), .Z(n1098));
OR2 U1035 ( .A(n1102), .B(n992), .Z(n1083));
IV2 U1036 ( .A(n993), .Z(n992));
AN2 U1037 ( .A(n1103), .B(n1104), .Z(n1102));
OR2 U1038 ( .A(n883), .B(n1105), .Z(n1104));
IV2 U1039 ( .A(n1106), .Z(n883));
IV2 U1040 ( .A(n801), .Z(n776));
OR2 U1041 ( .A(n1107), .B(n1108), .Z(n801));
OR2 U1042 ( .A(pi12), .B(n1109), .Z(n1108));
OR2 U1043 ( .A(n1110), .B(n1111), .Z(n986));
AN2 U1044 ( .A(n1112), .B(n717), .Z(n1111));
AN2 U1045 ( .A(n924), .B(n1113), .Z(n1112));
OR2 U1046 ( .A(n1114), .B(n927), .Z(n1113));
AN2 U1047 ( .A(pi11), .B(pi02), .Z(n1114));
AN2 U1048 ( .A(pi06), .B(n1115), .Z(n1110));
OR2 U1049 ( .A(n1116), .B(n930), .Z(n1115));
AN2 U1050 ( .A(n1117), .B(n804), .Z(n1116));
OR2 U1051 ( .A(n1118), .B(n1119), .Z(n1117));
AN2 U1052 ( .A(n854), .B(n993), .Z(n1119));
AN2 U1053 ( .A(n934), .B(n1016), .Z(n1118));
OR2 U1054 ( .A(n1120), .B(n1121), .Z(n984));
OR2 U1055 ( .A(n937), .B(n1122), .Z(n1121));
AN2 U1056 ( .A(n939), .B(n1123), .Z(n1122));
OR2 U1057 ( .A(n1124), .B(n1125), .Z(n1123));
OR2 U1058 ( .A(n918), .B(n1126), .Z(n1125));
AN2 U1059 ( .A(n724), .B(n982), .Z(n1126));
AN2 U1060 ( .A(n993), .B(pi02), .Z(n918));
OR2 U1061 ( .A(n1127), .B(n1128), .Z(n993));
OR2 U1062 ( .A(n1129), .B(n1130), .Z(n1128));
AN2 U1063 ( .A(n949), .B(n717), .Z(n1130));
AN2 U1064 ( .A(n950), .B(n877), .Z(n1129));
IV2 U1065 ( .A(n727), .Z(n877));
OR2 U1066 ( .A(n1131), .B(n1132), .Z(n1127));
OR2 U1067 ( .A(n1133), .B(n1134), .Z(n1132));
AN2 U1068 ( .A(n1135), .B(n1016), .Z(n1134));
OR2 U1069 ( .A(n1136), .B(n957), .Z(n1135));
AN2 U1070 ( .A(n1137), .B(n979), .Z(n1136));
AN2 U1071 ( .A(n784), .B(pi06), .Z(n1137));
AN2 U1072 ( .A(n724), .B(n1138), .Z(n1133));
OR2 U1073 ( .A(n1139), .B(n1140), .Z(n1138));
AN2 U1074 ( .A(n965), .B(n1141), .Z(n1139));
AN2 U1075 ( .A(pi02), .B(pi06), .Z(n724));
AN2 U1076 ( .A(pi13), .B(n1142), .Z(n1131));
OR2 U1077 ( .A(n1143), .B(n1144), .Z(n1142));
AN2 U1078 ( .A(n971), .B(pi01), .Z(n1144));
AN2 U1079 ( .A(n1145), .B(n973), .Z(n1143));
AN2 U1080 ( .A(n1146), .B(n1147), .Z(n1145));
OR2 U1081 ( .A(n727), .B(n979), .Z(n1147));
IV2 U1082 ( .A(n1141), .Z(n979));
OR2 U1083 ( .A(n1148), .B(n1141), .Z(n1146));
OR2 U1084 ( .A(n1149), .B(n1150), .Z(n1141));
AN2 U1085 ( .A(n1151), .B(n1017), .Z(n1150));
AN2 U1086 ( .A(pi05), .B(n1152), .Z(n1149));
OR2 U1087 ( .A(n1151), .B(n1017), .Z(n1152));
AN2 U1088 ( .A(pi02), .B(n717), .Z(n1148));
AN2 U1089 ( .A(n944), .B(n727), .Z(n1124));
AN2 U1090 ( .A(n1016), .B(n717), .Z(n727));
IV2 U1091 ( .A(pi06), .Z(n717));
IV2 U1092 ( .A(pi02), .Z(n1016));
AN2 U1093 ( .A(n983), .B(pi02), .Z(n1120));
OR2 U1094 ( .A(n1153), .B(n1154), .Z(po1));
OR2 U1095 ( .A(n1155), .B(n1156), .Z(n1154));
OR2 U1096 ( .A(n1157), .B(n1158), .Z(n1156));
OR2 U1097 ( .A(n1159), .B(n1160), .Z(n1158));
AN2 U1098 ( .A(n793), .B(n1105), .Z(n1160));
AN2 U1099 ( .A(n794), .B(n1032), .Z(n1159));
OR2 U1100 ( .A(n1161), .B(n1162), .Z(n1157));
AN2 U1101 ( .A(n1163), .B(n1107), .Z(n1162));
IV2 U1102 ( .A(n1164), .Z(n1161));
OR2 U1103 ( .A(n1107), .B(n1163), .Z(n1164));
AN2 U1104 ( .A(n1165), .B(n1166), .Z(n1163));
OR2 U1105 ( .A(n1167), .B(n804), .Z(n1107));
AN2 U1106 ( .A(n1168), .B(n1169), .Z(n1167));
AN2 U1107 ( .A(n1170), .B(n1171), .Z(n1169));
OR2 U1108 ( .A(n817), .B(n1172), .Z(n1171));
OR2 U1109 ( .A(pi11), .B(n1173), .Z(n1172));
AN2 U1110 ( .A(n1010), .B(n1174), .Z(n1173));
OR2 U1111 ( .A(n1012), .B(n1013), .Z(n1174));
OR2 U1112 ( .A(n1175), .B(n1082), .Z(n1010));
AN2 U1113 ( .A(n1176), .B(n1177), .Z(n1170));
OR2 U1114 ( .A(pi10), .B(n1178), .Z(n1177));
OR2 U1115 ( .A(n1179), .B(n1180), .Z(n1178));
AN2 U1116 ( .A(n1181), .B(n1031), .Z(n1180));
IV2 U1117 ( .A(n1182), .Z(n1179));
OR2 U1118 ( .A(n1181), .B(n1031), .Z(n1182));
OR2 U1119 ( .A(n1183), .B(n1184), .Z(n1181));
AN2 U1120 ( .A(n1185), .B(n1082), .Z(n1184));
AN2 U1121 ( .A(n1012), .B(n1092), .Z(n1183));
OR2 U1122 ( .A(n825), .B(n1186), .Z(n1176));
OR2 U1123 ( .A(n1187), .B(n1188), .Z(n1186));
AN2 U1124 ( .A(n1189), .B(n1190), .Z(n1187));
IV2 U1125 ( .A(n725), .Z(n1190));
OR2 U1126 ( .A(n1066), .B(n738), .Z(n1189));
AN2 U1127 ( .A(n1191), .B(n1192), .Z(n1168));
AN2 U1128 ( .A(n1193), .B(n1194), .Z(n1192));
OR2 U1129 ( .A(n1195), .B(n1017), .Z(n1194));
AN2 U1130 ( .A(n1196), .B(n1197), .Z(n1195));
AN2 U1131 ( .A(n1198), .B(n1199), .Z(n1197));
OR2 U1132 ( .A(pi05), .B(n1200), .Z(n1199));
AN2 U1133 ( .A(n1201), .B(n1063), .Z(n1198));
OR2 U1134 ( .A(n1202), .B(n772), .Z(n1201));
AN2 U1135 ( .A(n1203), .B(n1204), .Z(n1202));
OR2 U1136 ( .A(n1074), .B(n1032), .Z(n1204));
OR2 U1137 ( .A(n1105), .B(n1205), .Z(n1203));
AN2 U1138 ( .A(n1206), .B(n1207), .Z(n1196));
OR2 U1139 ( .A(n1208), .B(n1054), .Z(n1207));
AN2 U1140 ( .A(n1209), .B(n1210), .Z(n1208));
OR2 U1141 ( .A(n1081), .B(n1082), .Z(n1210));
OR2 U1142 ( .A(n1012), .B(n1211), .Z(n1209));
IV2 U1143 ( .A(n1081), .Z(n1211));
OR2 U1144 ( .A(n817), .B(n1212), .Z(n1206));
OR2 U1145 ( .A(n713), .B(n738), .Z(n1212));
OR2 U1146 ( .A(pi01), .B(n1213), .Z(n1193));
AN2 U1147 ( .A(n1214), .B(n1215), .Z(n1213));
AN2 U1148 ( .A(n1216), .B(n1217), .Z(n1215));
OR2 U1149 ( .A(n1054), .B(n1218), .Z(n1216));
OR2 U1150 ( .A(n1012), .B(n1081), .Z(n1218));
AN2 U1151 ( .A(pi00), .B(n1175), .Z(n1081));
OR2 U1152 ( .A(pi08), .B(n1020), .Z(n1054));
AN2 U1153 ( .A(n1219), .B(n1220), .Z(n1214));
OR2 U1154 ( .A(n772), .B(n1221), .Z(n1220));
OR2 U1155 ( .A(n1222), .B(n1223), .Z(n1221));
AN2 U1156 ( .A(n1074), .B(n1032), .Z(n1223));
AN2 U1157 ( .A(n1105), .B(n1205), .Z(n1222));
OR2 U1158 ( .A(n1224), .B(n738), .Z(n772));
AN2 U1159 ( .A(n1225), .B(n829), .Z(n1224));
OR2 U1160 ( .A(n751), .B(n1023), .Z(n1225));
OR2 U1161 ( .A(n716), .B(n1200), .Z(n1219));
OR2 U1162 ( .A(n718), .B(n825), .Z(n1200));
IV2 U1163 ( .A(n761), .Z(n825));
AN2 U1164 ( .A(n1226), .B(n1227), .Z(n1191));
OR2 U1165 ( .A(n1228), .B(n1229), .Z(n1227));
OR2 U1166 ( .A(n1020), .B(n1230), .Z(n1229));
OR2 U1167 ( .A(n1231), .B(n1232), .Z(n1230));
AN2 U1168 ( .A(n1233), .B(n1234), .Z(n1232));
AN2 U1169 ( .A(n1235), .B(n1031), .Z(n1233));
OR2 U1170 ( .A(n1030), .B(n1032), .Z(n1235));
AN2 U1171 ( .A(n1092), .B(n1041), .Z(n1030));
IV2 U1172 ( .A(n1236), .Z(n1231));
OR2 U1173 ( .A(n1234), .B(n1031), .Z(n1236));
OR2 U1174 ( .A(n1237), .B(n1238), .Z(n1031));
AN2 U1175 ( .A(n868), .B(n725), .Z(n1238));
AN2 U1176 ( .A(n1012), .B(n869), .Z(n1237));
IV2 U1177 ( .A(n1082), .Z(n1012));
OR2 U1178 ( .A(n1239), .B(n1240), .Z(n1082));
AN2 U1179 ( .A(n901), .B(n1075), .Z(n1240));
OR2 U1180 ( .A(pi01), .B(n1032), .Z(n1075));
AN2 U1181 ( .A(n902), .B(n1241), .Z(n1239));
OR2 U1182 ( .A(n1242), .B(n1243), .Z(n1241));
OR2 U1183 ( .A(n1244), .B(n1245), .Z(n1243));
AN2 U1184 ( .A(n1105), .B(n892), .Z(n1245));
AN2 U1185 ( .A(n1073), .B(n751), .Z(n1244));
AN2 U1186 ( .A(n908), .B(n725), .Z(n1242));
OR2 U1187 ( .A(n1185), .B(n1246), .Z(n1234));
OR2 U1188 ( .A(n1247), .B(n1105), .Z(n1246));
IV2 U1189 ( .A(n1248), .Z(n1020));
OR2 U1190 ( .A(n1249), .B(n744), .Z(n1228));
AN2 U1191 ( .A(n716), .B(n1023), .Z(n1249));
AN2 U1192 ( .A(n1250), .B(n1251), .Z(n1226));
OR2 U1193 ( .A(n1105), .B(n1103), .Z(n1251));
IV2 U1194 ( .A(n1252), .Z(n1103));
OR2 U1195 ( .A(n1253), .B(n1254), .Z(n1252));
AN2 U1196 ( .A(n1106), .B(n1041), .Z(n1254));
OR2 U1197 ( .A(n1255), .B(n780), .Z(n1106));
AN2 U1198 ( .A(n973), .B(n738), .Z(n1255));
AN2 U1199 ( .A(n854), .B(n738), .Z(n1253));
IV2 U1200 ( .A(n1032), .Z(n1105));
OR2 U1201 ( .A(n1032), .B(n1256), .Z(n1250));
OR2 U1202 ( .A(n1040), .B(n1041), .Z(n1256));
IV2 U1203 ( .A(n1257), .Z(n1040));
OR2 U1204 ( .A(n1258), .B(n1259), .Z(n1155));
AN2 U1205 ( .A(n1260), .B(n716), .Z(n1259));
AN2 U1206 ( .A(n924), .B(n1261), .Z(n1260));
OR2 U1207 ( .A(n1262), .B(n927), .Z(n1261));
AN2 U1208 ( .A(pi11), .B(pi01), .Z(n1262));
AN2 U1209 ( .A(pi05), .B(n1263), .Z(n1258));
OR2 U1210 ( .A(n1264), .B(n930), .Z(n1263));
AN2 U1211 ( .A(n1265), .B(n804), .Z(n1264));
OR2 U1212 ( .A(n1266), .B(n1267), .Z(n1265));
AN2 U1213 ( .A(n854), .B(n1032), .Z(n1267));
AN2 U1214 ( .A(n934), .B(n1017), .Z(n1266));
AN2 U1215 ( .A(pi11), .B(n761), .Z(n934));
OR2 U1216 ( .A(n1268), .B(n1269), .Z(n1153));
OR2 U1217 ( .A(n937), .B(n1270), .Z(n1269));
AN2 U1218 ( .A(n939), .B(n1271), .Z(n1270));
OR2 U1219 ( .A(n1272), .B(n1273), .Z(n1271));
OR2 U1220 ( .A(n1073), .B(n1274), .Z(n1273));
AN2 U1221 ( .A(n725), .B(n982), .Z(n1274));
AN2 U1222 ( .A(n1032), .B(pi01), .Z(n1073));
OR2 U1223 ( .A(n1275), .B(n1276), .Z(n1032));
OR2 U1224 ( .A(n1277), .B(n1278), .Z(n1276));
AN2 U1225 ( .A(n949), .B(n716), .Z(n1278));
AN2 U1226 ( .A(n950), .B(n1066), .Z(n1277));
IV2 U1227 ( .A(n723), .Z(n1066));
OR2 U1228 ( .A(n1279), .B(n1280), .Z(n1275));
OR2 U1229 ( .A(n1281), .B(n1282), .Z(n1280));
AN2 U1230 ( .A(n1283), .B(n1017), .Z(n1282));
OR2 U1231 ( .A(n1284), .B(n957), .Z(n1283));
AN2 U1232 ( .A(n1285), .B(n784), .Z(n1284));
AN2 U1233 ( .A(pi05), .B(n1286), .Z(n1285));
AN2 U1234 ( .A(n725), .B(n1287), .Z(n1281));
OR2 U1235 ( .A(n1288), .B(n1140), .Z(n1287));
AN2 U1236 ( .A(n965), .B(n1151), .Z(n1288));
AN2 U1237 ( .A(n744), .B(n902), .Z(n965));
AN2 U1238 ( .A(pi01), .B(pi05), .Z(n725));
AN2 U1239 ( .A(pi13), .B(n1289), .Z(n1279));
OR2 U1240 ( .A(n1290), .B(n1291), .Z(n1289));
AN2 U1241 ( .A(n971), .B(pi00), .Z(n1291));
AN2 U1242 ( .A(n892), .B(n1292), .Z(n971));
AN2 U1243 ( .A(pi10), .B(pi11), .Z(n1292));
AN2 U1244 ( .A(n1293), .B(n973), .Z(n1290));
AN2 U1245 ( .A(n1294), .B(n1295), .Z(n1293));
OR2 U1246 ( .A(n723), .B(n1286), .Z(n1295));
IV2 U1247 ( .A(n1151), .Z(n1286));
OR2 U1248 ( .A(n1151), .B(n1296), .Z(n1294));
AN2 U1249 ( .A(pi01), .B(n716), .Z(n1296));
AN2 U1250 ( .A(n944), .B(n723), .Z(n1272));
AN2 U1251 ( .A(n1017), .B(n716), .Z(n723));
IV2 U1252 ( .A(pi05), .Z(n716));
IV2 U1253 ( .A(pi01), .Z(n1017));
AN2 U1254 ( .A(n983), .B(pi01), .Z(n1268));
AN2 U1255 ( .A(pi11), .B(n1297), .Z(n983));
OR2 U1256 ( .A(n1298), .B(n1299), .Z(po0));
OR2 U1257 ( .A(n1300), .B(n1301), .Z(n1299));
OR2 U1258 ( .A(n1302), .B(n1303), .Z(n1301));
OR2 U1259 ( .A(n1304), .B(n1305), .Z(n1303));
AN2 U1260 ( .A(n793), .B(n1247), .Z(n1305));
AN2 U1261 ( .A(n924), .B(n1306), .Z(n793));
IV2 U1262 ( .A(n1307), .Z(n1306));
OR2 U1263 ( .A(n854), .B(n1308), .Z(n1307));
AN2 U1264 ( .A(pi08), .B(n1063), .Z(n1308));
IV2 U1265 ( .A(n1309), .Z(n1063));
AN2 U1266 ( .A(n794), .B(n1041), .Z(n1304));
AN2 U1267 ( .A(n1310), .B(n924), .Z(n794));
OR2 U1268 ( .A(pi11), .B(n854), .Z(n1310));
AN2 U1269 ( .A(pi11), .B(n1311), .Z(n1302));
OR2 U1270 ( .A(n1312), .B(n1313), .Z(n1311));
OR2 U1271 ( .A(n1314), .B(n1315), .Z(n1313));
AN2 U1272 ( .A(n924), .B(n1316), .Z(n1315));
AN2 U1273 ( .A(n1317), .B(n761), .Z(n1314));
AN2 U1274 ( .A(n1023), .B(n908), .Z(n761));
AN2 U1275 ( .A(n1151), .B(n804), .Z(n1317));
AN2 U1276 ( .A(n1297), .B(pi00), .Z(n1312));
AN2 U1277 ( .A(n804), .B(n1318), .Z(n1297));
OR2 U1278 ( .A(pi10), .B(n892), .Z(n1318));
OR2 U1279 ( .A(n1319), .B(n1320), .Z(n1300));
AN2 U1280 ( .A(n1321), .B(n709), .Z(n1320));
AN2 U1281 ( .A(n927), .B(n924), .Z(n1321));
AN2 U1282 ( .A(pi04), .B(n1322), .Z(n1319));
OR2 U1283 ( .A(n1323), .B(n930), .Z(n1322));
AN2 U1284 ( .A(n939), .B(n1324), .Z(n930));
AN2 U1285 ( .A(n744), .B(pi11), .Z(n1324));
AN2 U1286 ( .A(n957), .B(n1041), .Z(n1323));
OR2 U1287 ( .A(n1325), .B(n1326), .Z(n1298));
OR2 U1288 ( .A(n937), .B(n1327), .Z(n1326));
AN2 U1289 ( .A(pi13), .B(n1328), .Z(n1327));
OR2 U1290 ( .A(n1329), .B(n1330), .Z(n1328));
AN2 U1291 ( .A(n1109), .B(n1166), .Z(n1330));
IV2 U1292 ( .A(pi12), .Z(n1166));
IV2 U1293 ( .A(n1165), .Z(n1109));
AN2 U1294 ( .A(pi12), .B(n1165), .Z(n1329));
OR2 U1295 ( .A(n1331), .B(n1332), .Z(n1165));
AN2 U1296 ( .A(pi13), .B(n1333), .Z(n1332));
OR2 U1297 ( .A(n1334), .B(n1335), .Z(n1333));
OR2 U1298 ( .A(n1336), .B(n1337), .Z(n1335));
AN2 U1299 ( .A(n1247), .B(n1257), .Z(n1337));
OR2 U1300 ( .A(n1338), .B(n780), .Z(n1257));
AN2 U1301 ( .A(n1023), .B(n751), .Z(n780));
AN2 U1302 ( .A(n944), .B(pi09), .Z(n1338));
AN2 U1303 ( .A(pi11), .B(n1339), .Z(n1336));
OR2 U1304 ( .A(n1340), .B(n1341), .Z(n1339));
OR2 U1305 ( .A(n1342), .B(n1343), .Z(n1341));
AN2 U1306 ( .A(n1344), .B(pi00), .Z(n1343));
AN2 U1307 ( .A(n1345), .B(n1247), .Z(n1344));
AN2 U1308 ( .A(pi10), .B(n1346), .Z(n1345));
AN2 U1309 ( .A(n1041), .B(n713), .Z(n1342));
IV2 U1310 ( .A(n1217), .Z(n1340));
OR2 U1311 ( .A(pi00), .B(n817), .Z(n1217));
OR2 U1312 ( .A(n1023), .B(n1346), .Z(n817));
OR2 U1313 ( .A(n1347), .B(n1348), .Z(n1334));
OR2 U1314 ( .A(n1349), .B(n1350), .Z(n1348));
AN2 U1315 ( .A(n1316), .B(n1023), .Z(n1350));
AN2 U1316 ( .A(n854), .B(n1351), .Z(n1349));
OR2 U1317 ( .A(n1352), .B(n1353), .Z(n1351));
AN2 U1318 ( .A(pi00), .B(n738), .Z(n1353));
AN2 U1319 ( .A(pi09), .B(n1041), .Z(n1352));
AN2 U1320 ( .A(n1248), .B(n1354), .Z(n1347));
OR2 U1321 ( .A(n1355), .B(n1356), .Z(n1354));
OR2 U1322 ( .A(n1357), .B(n1358), .Z(n1356));
AN2 U1323 ( .A(n1185), .B(n1041), .Z(n1358));
IV2 U1324 ( .A(n1092), .Z(n1185));
AN2 U1325 ( .A(n1247), .B(n1092), .Z(n1357));
OR2 U1326 ( .A(n1359), .B(n1360), .Z(n1092));
AN2 U1327 ( .A(n868), .B(n718), .Z(n1360));
AN2 U1328 ( .A(n1023), .B(n901), .Z(n868));
AN2 U1329 ( .A(n973), .B(pi11), .Z(n901));
AN2 U1330 ( .A(n869), .B(n1013), .Z(n1359));
AN2 U1331 ( .A(n1361), .B(n927), .Z(n869));
AN2 U1332 ( .A(n963), .B(pi08), .Z(n927));
IV2 U1333 ( .A(n1041), .Z(n1247));
AN2 U1334 ( .A(n1175), .B(n713), .Z(n1355));
IV2 U1335 ( .A(n1013), .Z(n1175));
AN2 U1336 ( .A(n1361), .B(n738), .Z(n1248));
AN2 U1337 ( .A(n1362), .B(n751), .Z(n1331));
AN2 U1338 ( .A(n902), .B(n1013), .Z(n1362));
OR2 U1339 ( .A(n1363), .B(n1364), .Z(n1013));
IV2 U1340 ( .A(n902), .Z(n1364));
AN2 U1341 ( .A(n1365), .B(n1366), .Z(n1363));
OR2 U1342 ( .A(n1188), .B(n857), .Z(n1366));
IV2 U1343 ( .A(n908), .Z(n857));
IV2 U1344 ( .A(n718), .Z(n1188));
AN2 U1345 ( .A(n1367), .B(n1368), .Z(n1365));
OR2 U1346 ( .A(n1346), .B(n1205), .Z(n1368));
IV2 U1347 ( .A(n1074), .Z(n1205));
IV2 U1348 ( .A(n751), .Z(n1346));
OR2 U1349 ( .A(n829), .B(n1041), .Z(n1367));
IV2 U1350 ( .A(n892), .Z(n829));
AN2 U1351 ( .A(n1309), .B(n1369), .Z(n937));
AN2 U1352 ( .A(pi13), .B(n751), .Z(n1369));
AN2 U1353 ( .A(n939), .B(n1370), .Z(n1325));
OR2 U1354 ( .A(n1371), .B(n1372), .Z(n1370));
OR2 U1355 ( .A(n1074), .B(n1373), .Z(n1372));
AN2 U1356 ( .A(n1374), .B(n944), .Z(n1373));
AN2 U1357 ( .A(n713), .B(n709), .Z(n1374));
AN2 U1358 ( .A(n1041), .B(pi00), .Z(n1074));
OR2 U1359 ( .A(n1375), .B(n1376), .Z(n1041));
OR2 U1360 ( .A(n1377), .B(n1378), .Z(n1376));
OR2 U1361 ( .A(n1379), .B(n1380), .Z(n1378));
AN2 U1362 ( .A(n949), .B(n709), .Z(n1380));
OR2 U1363 ( .A(n1381), .B(n1382), .Z(n949));
OR2 U1364 ( .A(n1383), .B(n1384), .Z(n1382));
AN2 U1365 ( .A(n751), .B(n963), .Z(n1384));
AN2 U1366 ( .A(n1385), .B(n860), .Z(n1383));
IV2 U1367 ( .A(n963), .Z(n860));
AN2 U1368 ( .A(n1386), .B(n924), .Z(n1381));
AN2 U1369 ( .A(n804), .B(n1361), .Z(n924));
AN2 U1370 ( .A(pi08), .B(pi10), .Z(n1386));
AN2 U1371 ( .A(n718), .B(n1140), .Z(n1379));
OR2 U1372 ( .A(n1387), .B(n981), .Z(n1140));
AN2 U1373 ( .A(pi11), .B(n1388), .Z(n981));
AN2 U1374 ( .A(n1023), .B(n1389), .Z(n1388));
OR2 U1375 ( .A(n751), .B(n892), .Z(n1389));
AN2 U1376 ( .A(n744), .B(n1361), .Z(n892));
AN2 U1377 ( .A(pi09), .B(pi08), .Z(n751));
AN2 U1378 ( .A(n944), .B(n1361), .Z(n1387));
AN2 U1379 ( .A(n744), .B(n963), .Z(n944));
AN2 U1380 ( .A(n784), .B(n1151), .Z(n1377));
AN2 U1381 ( .A(n713), .B(pi04), .Z(n1151));
AN2 U1382 ( .A(n973), .B(n902), .Z(n784));
AN2 U1383 ( .A(n963), .B(pi13), .Z(n902));
AN2 U1384 ( .A(n738), .B(pi10), .Z(n963));
OR2 U1385 ( .A(n1390), .B(n1391), .Z(n1375));
OR2 U1386 ( .A(n1392), .B(n1393), .Z(n1391));
AN2 U1387 ( .A(n950), .B(n1394), .Z(n1393));
OR2 U1388 ( .A(pi00), .B(pi04), .Z(n1394));
AN2 U1389 ( .A(n1395), .B(n908), .Z(n950));
AN2 U1390 ( .A(n1361), .B(pi08), .Z(n908));
IV2 U1391 ( .A(pi09), .Z(n1361));
OR2 U1392 ( .A(pi13), .B(n1309), .Z(n1395));
AN2 U1393 ( .A(n1023), .B(n738), .Z(n1309));
IV2 U1394 ( .A(pi11), .Z(n738));
AN2 U1395 ( .A(n1385), .B(n1316), .Z(n1392));
AN2 U1396 ( .A(n709), .B(pi00), .Z(n1316));
IV2 U1397 ( .A(pi04), .Z(n709));
AN2 U1398 ( .A(n973), .B(pi13), .Z(n1385));
AN2 U1399 ( .A(n744), .B(pi09), .Z(n973));
AN2 U1400 ( .A(n957), .B(n713), .Z(n1390));
IV2 U1401 ( .A(pi00), .Z(n713));
AN2 U1402 ( .A(n804), .B(n854), .Z(n957));
AN2 U1403 ( .A(n744), .B(n1023), .Z(n854));
IV2 U1404 ( .A(pi10), .Z(n1023));
AN2 U1405 ( .A(n718), .B(n982), .Z(n1371));
OR2 U1406 ( .A(n1396), .B(pi11), .Z(n982));
AN2 U1407 ( .A(pi10), .B(n744), .Z(n1396));
IV2 U1408 ( .A(pi08), .Z(n744));
AN2 U1409 ( .A(pi00), .B(pi04), .Z(n718));
AN2 U1410 ( .A(n804), .B(pi09), .Z(n939));
IV2 U1411 ( .A(pi13), .Z(n804));
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

41
examples/smtbmc/glift/alu4.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog alu4.v
techmap
flatten
select alu4_lev2
glift -create-instrumented-model
techmap
opt
rename alu4_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog alu4.v
techmap
flatten
select alu4_lev2
glift -create-precise-model
techmap
opt
rename alu4_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution alu4.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file alu4.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

40
examples/smtbmc/glift/mux2.ys Normal file
View file

@ -0,0 +1,40 @@
logger -expect log "SAT proof finished - no model found: SUCCESS!" 1
logger -expect log "Number of cells:.*[\t ]12" 1
logger -expect log "Number of cells:.*[\t ]20" 1
logger -expect log "Problem is satisfiable with \\gate.__glift_weight = 11." 1
logger -expect log "Problem is NOT satisfiable with \\gate.__glift_weight <= 10." 1
logger -expect log "Wire \\gate.__glift_weight is minimized at 11." 1
logger -expect log "Specializing .* from file with .* = 1." 2
logger -expect log "Specializing .* from file with .* = 0." 4
read_verilog <<EOT
module mux2(a, b, s, y);
input a, b, s;
output y;
wire s_n = ~s;
wire t0 = s & a;
wire t1 = s_n & b;
assign y = t0 | t1;
endmodule
EOT
techmap
copy mux2 spec
copy mux2 uut
copy mux2 solved
delete mux2
glift -create-precise-model spec
glift -create-instrumented-model uut
glift -create-instrumented-model -no-cost-model solved
design -push-copy
miter -equiv spec uut qbfmiter
flatten
delete spec uut solved
qbfsat -assume-outputs -assume-negative-polarity -write-solution mux2.soln qbfmiter
design -pop
qbfsat -specialize-from-file mux2.soln solved
opt
miter -equiv spec solved proofmiter
flatten proofmiter
sat -prove trigger 0 proofmiter
delete proofmiter
stat solved spec

83
examples/smtbmc/glift/t481.v Executable file
View file

@ -0,0 +1,83 @@
module t481_lev2(pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09,
pi10, pi11, pi12, pi13, pi14, pi15, po0);
input pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09,
pi10, pi11, pi12, pi13, pi14, pi15;
output po0;
wire n46, n47, n48, n49, n50, n51, n52, n53, n54, n55,
n56, n57, n58, n59, n60, n61, n62, n63, n64, n65,
n66, n67, n68, n69, n70, n71, n72, n73, n74, n75,
n76, n77, n78, n79, n80, n81, n82, n83, n84, n85,
n86, n87, n88, n89, n90;
OR2 U47 ( .A(n46), .B(n47), .Z(po0));
OR2 U48 ( .A(n48), .B(n49), .Z(n47));
AN2 U49 ( .A(n50), .B(n51), .Z(n49));
OR2 U50 ( .A(n52), .B(n53), .Z(n51));
AN2 U51 ( .A(n54), .B(n55), .Z(n53));
AN2 U52 ( .A(n56), .B(n57), .Z(n54));
AN2 U53 ( .A(n58), .B(n59), .Z(n52));
AN2 U54 ( .A(n60), .B(n61), .Z(n48));
IV2 U55 ( .A(n50), .Z(n61));
AN2 U56 ( .A(n62), .B(pi15), .Z(n50));
IV2 U57 ( .A(pi14), .Z(n62));
OR2 U58 ( .A(n63), .B(n64), .Z(n60));
AN2 U59 ( .A(n65), .B(n55), .Z(n64));
IV2 U60 ( .A(n59), .Z(n55));
AN2 U61 ( .A(n57), .B(n58), .Z(n65));
IV2 U62 ( .A(n56), .Z(n58));
AN2 U63 ( .A(n56), .B(n59), .Z(n63));
AN2 U64 ( .A(n66), .B(pi00), .Z(n56));
IV2 U65 ( .A(pi01), .Z(n66));
AN2 U66 ( .A(n67), .B(n59), .Z(n46));
OR2 U67 ( .A(n68), .B(n69), .Z(n59));
OR2 U68 ( .A(n70), .B(n71), .Z(n69));
AN2 U69 ( .A(n72), .B(n73), .Z(n71));
IV2 U70 ( .A(n74), .Z(n70));
OR2 U71 ( .A(n73), .B(n72), .Z(n74));
AN2 U72 ( .A(n75), .B(pi12), .Z(n72));
IV2 U73 ( .A(pi13), .Z(n75));
OR2 U74 ( .A(pi10), .B(n76), .Z(n73));
IV2 U75 ( .A(pi11), .Z(n76));
AN2 U76 ( .A(n77), .B(n78), .Z(n68));
OR2 U77 ( .A(n79), .B(n80), .Z(n78));
IV2 U78 ( .A(n81), .Z(n77));
AN2 U79 ( .A(n80), .B(n79), .Z(n81));
AN2 U80 ( .A(n82), .B(pi08), .Z(n79));
IV2 U81 ( .A(pi09), .Z(n82));
OR2 U82 ( .A(pi06), .B(n83), .Z(n80));
IV2 U83 ( .A(pi07), .Z(n83));
IV2 U84 ( .A(n57), .Z(n67));
OR2 U85 ( .A(n84), .B(n85), .Z(n57));
AN2 U86 ( .A(n86), .B(n87), .Z(n85));
IV2 U87 ( .A(n88), .Z(n84));
OR2 U88 ( .A(n87), .B(n86), .Z(n88));
AN2 U89 ( .A(n89), .B(pi04), .Z(n86));
IV2 U90 ( .A(pi05), .Z(n89));
OR2 U91 ( .A(pi02), .B(n90), .Z(n87));
IV2 U92 ( .A(pi03), .Z(n90));
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

41
examples/smtbmc/glift/t481.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog t481.v
techmap
flatten
select t481_lev2
glift -create-instrumented-model
techmap
opt
rename t481_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog t481.v
techmap
flatten
select t481_lev2
glift -create-precise-model
techmap
opt
rename t481_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution t481.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file t481.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

345
examples/smtbmc/glift/too_large.v Executable file
View file

@ -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

41
examples/smtbmc/glift/too_large.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog too_large.v
techmap
flatten
select too_large_lev2
glift -create-instrumented-model
techmap
opt
rename too_large_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog too_large.v
techmap
flatten
select too_large_lev2
glift -create-precise-model
techmap
opt
rename too_large_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution too_large.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file too_large.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

220
examples/smtbmc/glift/ttt2.v Executable file
View file

@ -0,0 +1,220 @@
module ttt2_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, po00, po01, po02, po03, po04, po05,
po06, po07, po08, po09, po10, po11, po12, po13, po14, po15,
po16, po17, po18, po19, po20);
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;
output po00, po01, po02, po03, po04, po05, po06, po07, po08, po09,
po10, po11, po12, po13, po14, po15, po16, po17, po18, po19,
po20;
wire n148, n149, n150, n151, n152, n153, n154, n155, n156, n157,
n158, n159, n160, n161, n162, n163, n164, n165, n166, n167,
n168, n169, n170, n171, n172, n173, n174, n175, n176, n177,
n178, n179, n180, n181, n182, n183, n184, n185, n186, n187,
n188, n189, n190, n191, n192, n193, n194, n195, n196, n197,
n198, n199, n200, n201, n202, n203, n204, n205, n206, n207,
n208, n209, n210, n211, n212, n213, n214, n215, n216, n217,
n218, n219, n220, n221, n222, n223, n224, n225, n226, n227,
n228, n229, n230, n231, n232, n233, n234, n235, n236, n237,
n238, n239, n240, n241, n242, n243, n244, n245, n246, n247,
n248, n249, n250, n251, n252, n253, n254, n255, n256, n257,
n258, n259, n260, n261, n262, n263, n264, n265, n266, n267,
n268, n269, n270, n271, n272, n273, n274, n275, n276, n277,
n278, n279, n280, n281, n282, n283, n284, n285, n286, n287,
n288, n289, n290, n291, n292, n293;
AN2 U168 ( .A(n148), .B(n149), .Z(po20));
OR2 U169 ( .A(n150), .B(n151), .Z(n148));
AN2 U170 ( .A(pi02), .B(n152), .Z(n151));
IV2 U171 ( .A(n153), .Z(n150));
OR2 U172 ( .A(n152), .B(pi02), .Z(n153));
IV2 U173 ( .A(pi23), .Z(n152));
AN2 U174 ( .A(n154), .B(n149), .Z(po19));
OR2 U175 ( .A(n155), .B(n156), .Z(n154));
AN2 U176 ( .A(pi01), .B(n157), .Z(n156));
AN2 U177 ( .A(pi22), .B(n158), .Z(n155));
IV2 U178 ( .A(pi01), .Z(n158));
AN2 U179 ( .A(n159), .B(n149), .Z(po18));
OR2 U180 ( .A(n160), .B(n161), .Z(po17));
AN2 U181 ( .A(pi20), .B(n162), .Z(n161));
OR2 U182 ( .A(n163), .B(n164), .Z(n162));
OR2 U183 ( .A(n165), .B(n166), .Z(n164));
AN2 U184 ( .A(n167), .B(pi18), .Z(n166));
AN2 U185 ( .A(n149), .B(n168), .Z(n167));
AN2 U186 ( .A(n169), .B(n170), .Z(n160));
AN2 U187 ( .A(n171), .B(n172), .Z(n169));
OR2 U188 ( .A(n165), .B(n173), .Z(po16));
OR2 U189 ( .A(n174), .B(n175), .Z(n173));
AN2 U190 ( .A(n176), .B(n168), .Z(n175));
AN2 U191 ( .A(n170), .B(n171), .Z(n176));
AN2 U192 ( .A(pi19), .B(n163), .Z(n174));
AN2 U193 ( .A(pi19), .B(n177), .Z(n165));
AN2 U194 ( .A(n178), .B(n149), .Z(n177));
OR2 U195 ( .A(n179), .B(n180), .Z(po15));
AN2 U196 ( .A(n181), .B(n178), .Z(n180));
AN2 U197 ( .A(n182), .B(n170), .Z(n181));
AN2 U198 ( .A(pi17), .B(n183), .Z(n182));
OR2 U199 ( .A(pi19), .B(n184), .Z(n183));
AN2 U200 ( .A(pi18), .B(n163), .Z(n179));
OR2 U201 ( .A(n185), .B(n186), .Z(n163));
AN2 U202 ( .A(n149), .B(n187), .Z(n185));
OR2 U203 ( .A(n188), .B(n189), .Z(po14));
AN2 U204 ( .A(pi17), .B(n186), .Z(n189));
OR2 U205 ( .A(n190), .B(n191), .Z(n186));
AN2 U206 ( .A(n192), .B(n149), .Z(n190));
OR2 U207 ( .A(pi14), .B(n193), .Z(n192));
AN2 U208 ( .A(n170), .B(n187), .Z(n188));
AN2 U209 ( .A(n194), .B(n195), .Z(n170));
AN2 U210 ( .A(n196), .B(n197), .Z(n195));
OR2 U211 ( .A(n198), .B(n199), .Z(po13));
AN2 U212 ( .A(pi16), .B(n200), .Z(n199));
OR2 U213 ( .A(n201), .B(n191), .Z(n200));
AN2 U214 ( .A(n202), .B(pi14), .Z(n198));
AN2 U215 ( .A(n203), .B(n149), .Z(n202));
OR2 U216 ( .A(n204), .B(n197), .Z(n203));
IV2 U217 ( .A(n193), .Z(n197));
AN2 U218 ( .A(n205), .B(n206), .Z(n204));
AN2 U219 ( .A(n207), .B(n208), .Z(n206));
AN2 U220 ( .A(pi15), .B(pi13), .Z(n205));
OR2 U221 ( .A(n201), .B(n209), .Z(po12));
OR2 U222 ( .A(n210), .B(n211), .Z(n209));
AN2 U223 ( .A(n212), .B(n213), .Z(n211));
AN2 U224 ( .A(pi14), .B(n194), .Z(n212));
AN2 U225 ( .A(pi15), .B(n191), .Z(n210));
AN2 U226 ( .A(pi15), .B(n214), .Z(n201));
AN2 U227 ( .A(n196), .B(n149), .Z(n214));
OR2 U228 ( .A(n215), .B(n216), .Z(po11));
AN2 U229 ( .A(n217), .B(n196), .Z(n216));
IV2 U230 ( .A(pi14), .Z(n196));
AN2 U231 ( .A(n194), .B(n193), .Z(n217));
OR2 U232 ( .A(pi15), .B(n208), .Z(n193));
IV2 U233 ( .A(pi16), .Z(n208));
AN2 U234 ( .A(pi13), .B(n218), .Z(n194));
AN2 U235 ( .A(pi14), .B(n191), .Z(n215));
OR2 U236 ( .A(n219), .B(n220), .Z(n191));
AN2 U237 ( .A(n149), .B(n221), .Z(n220));
OR2 U238 ( .A(n222), .B(n223), .Z(po10));
AN2 U239 ( .A(n219), .B(pi13), .Z(n223));
AN2 U240 ( .A(n224), .B(n157), .Z(n219));
IV2 U241 ( .A(pi22), .Z(n157));
OR2 U242 ( .A(n225), .B(n226), .Z(n224));
OR2 U243 ( .A(po06), .B(n227), .Z(n226));
AN2 U244 ( .A(n218), .B(n221), .Z(n222));
IV2 U245 ( .A(pi13), .Z(n221));
AN2 U246 ( .A(n207), .B(n149), .Z(n218));
OR2 U247 ( .A(n228), .B(pi22), .Z(n207));
AN2 U248 ( .A(n229), .B(pi09), .Z(n228));
AN2 U249 ( .A(n230), .B(n231), .Z(n229));
OR2 U250 ( .A(n232), .B(n233), .Z(po09));
AN2 U251 ( .A(pi12), .B(n234), .Z(n233));
OR2 U252 ( .A(n235), .B(po06), .Z(n234));
AN2 U253 ( .A(n227), .B(n236), .Z(n232));
OR2 U254 ( .A(n237), .B(n230), .Z(n236));
AN2 U255 ( .A(n238), .B(pi11), .Z(n237));
AN2 U256 ( .A(pi09), .B(n239), .Z(n238));
IV2 U257 ( .A(pi12), .Z(n239));
OR2 U258 ( .A(n235), .B(n240), .Z(po08));
OR2 U259 ( .A(n241), .B(n242), .Z(n240));
AN2 U260 ( .A(po06), .B(pi11), .Z(n242));
AN2 U261 ( .A(n243), .B(n244), .Z(n241));
AN2 U262 ( .A(n227), .B(pi09), .Z(n243));
AN2 U263 ( .A(n149), .B(pi10), .Z(n227));
AN2 U264 ( .A(pi11), .B(n245), .Z(n235));
AN2 U265 ( .A(n231), .B(n149), .Z(n245));
OR2 U266 ( .A(n246), .B(n247), .Z(po07));
AN2 U267 ( .A(po06), .B(pi10), .Z(n247));
AN2 U268 ( .A(n248), .B(n231), .Z(n246));
IV2 U269 ( .A(pi10), .Z(n231));
AN2 U270 ( .A(n225), .B(pi09), .Z(n248));
AN2 U271 ( .A(n249), .B(n149), .Z(n225));
IV2 U272 ( .A(n230), .Z(n249));
AN2 U273 ( .A(n244), .B(pi12), .Z(n230));
IV2 U274 ( .A(pi11), .Z(n244));
AN2 U275 ( .A(n250), .B(n149), .Z(po06));
IV2 U276 ( .A(pi00), .Z(n149));
IV2 U277 ( .A(pi09), .Z(n250));
AN2 U278 ( .A(n251), .B(n252), .Z(po05));
OR2 U279 ( .A(n253), .B(n254), .Z(n251));
OR2 U280 ( .A(n255), .B(n256), .Z(n254));
AN2 U281 ( .A(n257), .B(n187), .Z(n255));
AN2 U282 ( .A(pi08), .B(n258), .Z(n253));
OR2 U283 ( .A(n259), .B(n260), .Z(po04));
AN2 U284 ( .A(pi07), .B(n261), .Z(n260));
AN2 U285 ( .A(n262), .B(n257), .Z(n259));
AN2 U286 ( .A(n171), .B(n252), .Z(n262));
AN2 U287 ( .A(pi17), .B(pi18), .Z(n171));
OR2 U288 ( .A(n263), .B(n264), .Z(po03));
OR2 U289 ( .A(n265), .B(n266), .Z(n264));
AN2 U290 ( .A(pi06), .B(n261), .Z(n266));
AN2 U291 ( .A(n267), .B(n213), .Z(n265));
OR2 U292 ( .A(n172), .B(pi21), .Z(n267));
OR2 U293 ( .A(n268), .B(n269), .Z(n263));
OR2 U294 ( .A(n270), .B(n269), .Z(po02));
IV2 U295 ( .A(n271), .Z(n269));
OR2 U296 ( .A(n272), .B(n273), .Z(n271));
AN2 U297 ( .A(n274), .B(n275), .Z(n272));
OR2 U298 ( .A(n187), .B(n276), .Z(n275));
OR2 U299 ( .A(pi21), .B(n277), .Z(n274));
AN2 U300 ( .A(pi05), .B(n261), .Z(n270));
OR2 U301 ( .A(n278), .B(n279), .Z(po01));
OR2 U302 ( .A(n268), .B(n280), .Z(n279));
AN2 U303 ( .A(pi04), .B(n261), .Z(n280));
AN2 U304 ( .A(n252), .B(n258), .Z(n261));
IV2 U305 ( .A(n281), .Z(n268));
OR2 U306 ( .A(n282), .B(n283), .Z(n281));
OR2 U307 ( .A(n184), .B(n284), .Z(n283));
OR2 U308 ( .A(pi21), .B(pi17), .Z(n282));
AN2 U309 ( .A(n159), .B(n213), .Z(n278));
IV2 U310 ( .A(pi15), .Z(n213));
OR2 U311 ( .A(n285), .B(n286), .Z(n159));
AN2 U312 ( .A(pi21), .B(n287), .Z(n286));
OR2 U313 ( .A(n276), .B(n288), .Z(n287));
OR2 U314 ( .A(n273), .B(n187), .Z(n288));
OR2 U315 ( .A(pi23), .B(pi18), .Z(n276));
AN2 U316 ( .A(n172), .B(n277), .Z(n285));
AN2 U317 ( .A(pi23), .B(n289), .Z(n277));
AN2 U318 ( .A(n178), .B(n187), .Z(n289));
IV2 U319 ( .A(pi17), .Z(n187));
IV2 U320 ( .A(pi18), .Z(n178));
IV2 U321 ( .A(n273), .Z(n172));
OR2 U322 ( .A(pi20), .B(n168), .Z(n273));
AN2 U323 ( .A(n290), .B(n252), .Z(po00));
IV2 U324 ( .A(pi21), .Z(n252));
OR2 U325 ( .A(n256), .B(n291), .Z(n290));
OR2 U326 ( .A(n257), .B(n292), .Z(n291));
AN2 U327 ( .A(pi03), .B(n258), .Z(n292));
AN2 U328 ( .A(n284), .B(pi20), .Z(n258));
AN2 U329 ( .A(n184), .B(n168), .Z(n257));
IV2 U330 ( .A(pi19), .Z(n168));
IV2 U331 ( .A(pi20), .Z(n184));
AN2 U332 ( .A(n293), .B(pi17), .Z(n256));
IV2 U333 ( .A(n284), .Z(n293));
OR2 U334 ( .A(pi18), .B(pi19), .Z(n284));
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

41
examples/smtbmc/glift/ttt2.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog ttt2.v
techmap
flatten
select ttt2_lev2
glift -create-instrumented-model
techmap
opt
rename ttt2_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog ttt2.v
techmap
flatten
select ttt2_lev2
glift -create-precise-model
techmap
opt
rename ttt2_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution ttt2.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file ttt2.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

380
examples/smtbmc/glift/x1.v Executable file
View file

@ -0,0 +1,380 @@
module x1_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, pi38, pi39,
pi40, pi41, pi42, pi43, pi44, pi45, pi46, pi47, pi48, pi49,
pi50, po00, po01, po02, po03, po04, po05, po06, po07, po08,
po09, po10, po11, po12, po13, po14, po15, po16, po17, po18,
po19, po20, po21, po22, po23, po24, po25, po26, po27, po28,
po29, po30, po31, po32, po33, po34);
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, pi38, pi39,
pi40, pi41, pi42, pi43, pi44, pi45, pi46, pi47, pi48, pi49,
pi50;
output po00, po01, po02, po03, po04, po05, po06, po07, po08, po09,
po10, po11, po12, po13, po14, po15, po16, po17, po18, po19,
po20, po21, po22, po23, po24, po25, po26, po27, po28, po29,
po30, po31, po32, po33, po34;
wire po05, po16, po18, po24, po25, po28, po29, n270, n271, n272,
n273, n274, n275, n276, n277, n278, n279, 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;
assign po05 = pi32;
assign po16 = pi37;
assign po18 = pi38;
assign po24 = pi23;
assign po25 = pi24;
assign po28 = pi48;
assign po29 = pi49;
IV2 U294 ( .A(po32), .Z(po33));
OR2 U295 ( .A(n270), .B(n271), .Z(po32));
OR2 U296 ( .A(po25), .B(po05), .Z(n271));
AN2 U297 ( .A(n272), .B(n273), .Z(n270));
OR2 U298 ( .A(pi31), .B(po01), .Z(n273));
AN2 U299 ( .A(n274), .B(pi18), .Z(po31));
AN2 U300 ( .A(pi17), .B(n275), .Z(n274));
AN2 U301 ( .A(n276), .B(n272), .Z(po30));
OR2 U302 ( .A(n277), .B(n278), .Z(n276));
AN2 U303 ( .A(n279), .B(n280), .Z(n278));
OR2 U304 ( .A(n281), .B(pi31), .Z(n280));
AN2 U305 ( .A(pi35), .B(n282), .Z(n281));
AN2 U306 ( .A(n283), .B(n284), .Z(n277));
OR2 U307 ( .A(n285), .B(n286), .Z(n284));
AN2 U308 ( .A(pi31), .B(n287), .Z(n286));
IV2 U309 ( .A(pi05), .Z(n287));
AN2 U310 ( .A(n288), .B(pi35), .Z(n285));
AN2 U311 ( .A(pi21), .B(pi13), .Z(n288));
AN2 U312 ( .A(pi07), .B(n289), .Z(po27));
OR2 U313 ( .A(n290), .B(n291), .Z(po26));
OR2 U314 ( .A(n292), .B(n293), .Z(n291));
AN2 U315 ( .A(n294), .B(n295), .Z(n293));
AN2 U316 ( .A(n296), .B(n297), .Z(n295));
AN2 U317 ( .A(pi33), .B(n298), .Z(n294));
IV2 U318 ( .A(n299), .Z(n298));
AN2 U319 ( .A(pi19), .B(pi00), .Z(n299));
AN2 U320 ( .A(n300), .B(n301), .Z(n292));
AN2 U321 ( .A(n302), .B(n303), .Z(n301));
OR2 U322 ( .A(n304), .B(pi35), .Z(n303));
AN2 U323 ( .A(n305), .B(pi25), .Z(n304));
AN2 U324 ( .A(pi11), .B(n306), .Z(n305));
AN2 U325 ( .A(n272), .B(n307), .Z(n302));
AN2 U326 ( .A(n308), .B(pi01), .Z(n300));
AN2 U327 ( .A(n279), .B(pi17), .Z(n308));
AN2 U328 ( .A(pi34), .B(n309), .Z(n290));
OR2 U329 ( .A(n310), .B(n311), .Z(po23));
AN2 U330 ( .A(n312), .B(n313), .Z(n310));
OR2 U331 ( .A(n314), .B(n315), .Z(po22));
AN2 U332 ( .A(n316), .B(n317), .Z(n315));
AN2 U333 ( .A(n318), .B(n319), .Z(n317));
OR2 U334 ( .A(n320), .B(n272), .Z(n319));
AN2 U335 ( .A(n321), .B(n322), .Z(n320));
IV2 U336 ( .A(pi02), .Z(n322));
AN2 U337 ( .A(n296), .B(n323), .Z(n321));
OR2 U338 ( .A(pi09), .B(n324), .Z(n318));
AN2 U339 ( .A(pi05), .B(pi21), .Z(n324));
AN2 U340 ( .A(pi31), .B(n309), .Z(n316));
AN2 U341 ( .A(n325), .B(n326), .Z(n314));
AN2 U342 ( .A(n283), .B(n327), .Z(n325));
OR2 U343 ( .A(n328), .B(n329), .Z(n327));
OR2 U344 ( .A(n330), .B(n331), .Z(n329));
OR2 U345 ( .A(n332), .B(n333), .Z(n331));
AN2 U346 ( .A(po05), .B(n272), .Z(n333));
AN2 U347 ( .A(pi43), .B(n296), .Z(n332));
AN2 U348 ( .A(pi47), .B(pi39), .Z(n330));
OR2 U349 ( .A(n334), .B(n335), .Z(n328));
OR2 U350 ( .A(n336), .B(n337), .Z(n335));
AN2 U351 ( .A(n338), .B(pi40), .Z(n337));
AN2 U352 ( .A(n339), .B(n340), .Z(n338));
AN2 U353 ( .A(n341), .B(n342), .Z(n336));
AN2 U354 ( .A(n343), .B(n344), .Z(n342));
AN2 U355 ( .A(n345), .B(pi41), .Z(n341));
AN2 U356 ( .A(pi29), .B(n346), .Z(n334));
OR2 U357 ( .A(n347), .B(n348), .Z(po21));
AN2 U358 ( .A(pi09), .B(po05), .Z(n348));
AN2 U359 ( .A(n349), .B(n350), .Z(n347));
AN2 U360 ( .A(n346), .B(n279), .Z(n350));
AN2 U361 ( .A(n351), .B(n326), .Z(n349));
OR2 U362 ( .A(n352), .B(n353), .Z(po20));
OR2 U363 ( .A(n354), .B(n355), .Z(n353));
AN2 U364 ( .A(pi22), .B(po05), .Z(n355));
AN2 U365 ( .A(n356), .B(n357), .Z(n354));
OR2 U366 ( .A(n358), .B(n359), .Z(n356));
OR2 U367 ( .A(po05), .B(n360), .Z(n359));
AN2 U368 ( .A(n361), .B(n362), .Z(n360));
OR2 U369 ( .A(n363), .B(n364), .Z(n362));
AN2 U370 ( .A(n346), .B(n365), .Z(n364));
AN2 U371 ( .A(n366), .B(pi14), .Z(n346));
AN2 U372 ( .A(n367), .B(n343), .Z(n363));
OR2 U373 ( .A(n368), .B(n365), .Z(n367));
OR2 U374 ( .A(n351), .B(pi29), .Z(n365));
AN2 U375 ( .A(pi28), .B(n345), .Z(n368));
AN2 U376 ( .A(n309), .B(n369), .Z(n361));
AN2 U377 ( .A(pi07), .B(n370), .Z(n358));
OR2 U378 ( .A(pi28), .B(pi29), .Z(n370));
OR2 U379 ( .A(n371), .B(n372), .Z(n352));
AN2 U380 ( .A(pi01), .B(n373), .Z(n372));
OR2 U381 ( .A(n374), .B(pi30), .Z(n373));
AN2 U382 ( .A(pi10), .B(pi25), .Z(n374));
AN2 U383 ( .A(n375), .B(n376), .Z(n371));
OR2 U384 ( .A(pi40), .B(pi41), .Z(n376));
OR2 U385 ( .A(n377), .B(n378), .Z(po19));
OR2 U386 ( .A(n379), .B(n380), .Z(n378));
AN2 U387 ( .A(pi42), .B(pi01), .Z(n380));
AN2 U388 ( .A(pi12), .B(n381), .Z(n379));
OR2 U389 ( .A(n382), .B(n383), .Z(n381));
OR2 U390 ( .A(n384), .B(n385), .Z(n383));
AN2 U391 ( .A(n386), .B(n369), .Z(n384));
OR2 U392 ( .A(po34), .B(n387), .Z(n386));
OR2 U393 ( .A(pi40), .B(pi26), .Z(n387));
OR2 U394 ( .A(pi27), .B(pi28), .Z(po34));
OR2 U395 ( .A(pi31), .B(pi29), .Z(n382));
OR2 U396 ( .A(n388), .B(n389), .Z(n377));
OR2 U397 ( .A(n390), .B(n391), .Z(n389));
AN2 U398 ( .A(n392), .B(pi18), .Z(n391));
AN2 U399 ( .A(pi17), .B(n393), .Z(n392));
OR2 U400 ( .A(pi36), .B(pi40), .Z(n393));
AN2 U401 ( .A(n394), .B(pi22), .Z(n390));
AN2 U402 ( .A(n351), .B(n369), .Z(n394));
AN2 U403 ( .A(pi00), .B(n395), .Z(n388));
OR2 U404 ( .A(n396), .B(n397), .Z(n395));
OR2 U405 ( .A(n385), .B(n398), .Z(n397));
OR2 U406 ( .A(n399), .B(n400), .Z(n398));
AN2 U407 ( .A(pi31), .B(n272), .Z(n399));
OR2 U408 ( .A(n401), .B(n402), .Z(n385));
OR2 U409 ( .A(pi41), .B(pi35), .Z(n402));
OR2 U410 ( .A(po05), .B(pi43), .Z(n401));
OR2 U411 ( .A(n403), .B(n404), .Z(n396));
OR2 U412 ( .A(pi25), .B(n289), .Z(n404));
OR2 U413 ( .A(pi34), .B(pi28), .Z(n403));
IV2 U414 ( .A(po17), .Z(po15));
OR2 U415 ( .A(n405), .B(n406), .Z(po17));
OR2 U416 ( .A(n407), .B(n408), .Z(n406));
OR2 U417 ( .A(n409), .B(n410), .Z(n408));
AN2 U418 ( .A(pi28), .B(n411), .Z(n410));
OR2 U419 ( .A(pi03), .B(n296), .Z(n411));
AN2 U420 ( .A(n412), .B(n413), .Z(n409));
OR2 U421 ( .A(n414), .B(n415), .Z(n413));
AN2 U422 ( .A(pi02), .B(pi31), .Z(n415));
AN2 U423 ( .A(n416), .B(n417), .Z(n414));
AN2 U424 ( .A(n418), .B(n309), .Z(n416));
OR2 U425 ( .A(pi25), .B(n272), .Z(n418));
OR2 U426 ( .A(pi09), .B(n419), .Z(n412));
AN2 U427 ( .A(n420), .B(n421), .Z(n419));
AN2 U428 ( .A(n275), .B(n309), .Z(n421));
OR2 U429 ( .A(pi25), .B(pi35), .Z(n275));
AN2 U430 ( .A(n417), .B(pi21), .Z(n420));
OR2 U431 ( .A(pi26), .B(n313), .Z(n407));
AN2 U432 ( .A(pi33), .B(pi08), .Z(n313));
OR2 U433 ( .A(n422), .B(n423), .Z(n405));
OR2 U434 ( .A(po05), .B(pi27), .Z(n423));
AN2 U435 ( .A(n424), .B(n425), .Z(po14));
AN2 U436 ( .A(n426), .B(n309), .Z(n425));
OR2 U437 ( .A(n427), .B(n428), .Z(n426));
OR2 U438 ( .A(n429), .B(n430), .Z(n428));
AN2 U439 ( .A(pi29), .B(n431), .Z(n430));
OR2 U440 ( .A(pi43), .B(pi40), .Z(n427));
AN2 U441 ( .A(n326), .B(pi07), .Z(n424));
OR2 U442 ( .A(n432), .B(n433), .Z(po12));
OR2 U443 ( .A(n434), .B(n435), .Z(n433));
AN2 U444 ( .A(pi28), .B(n436), .Z(n435));
OR2 U445 ( .A(n437), .B(pi21), .Z(n436));
AN2 U446 ( .A(n438), .B(pi14), .Z(n437));
AN2 U447 ( .A(n439), .B(n323), .Z(n438));
OR2 U448 ( .A(n440), .B(n441), .Z(n439));
IV2 U449 ( .A(n442), .Z(n441));
AN2 U450 ( .A(n443), .B(pi15), .Z(n440));
AN2 U451 ( .A(n444), .B(n445), .Z(n434));
AN2 U452 ( .A(n446), .B(n312), .Z(n445));
AN2 U453 ( .A(n447), .B(n448), .Z(n446));
OR2 U454 ( .A(n282), .B(n307), .Z(n447));
IV2 U455 ( .A(pi18), .Z(n307));
AN2 U456 ( .A(n449), .B(pi40), .Z(n444));
AN2 U457 ( .A(n450), .B(n451), .Z(n449));
OR2 U458 ( .A(n339), .B(n297), .Z(n451));
IV2 U459 ( .A(n452), .Z(n450));
AN2 U460 ( .A(n453), .B(n339), .Z(n452));
OR2 U461 ( .A(n340), .B(pi12), .Z(n453));
AN2 U462 ( .A(pi02), .B(pi03), .Z(n340));
AN2 U463 ( .A(pi46), .B(pi39), .Z(n432));
IV2 U464 ( .A(po13), .Z(po11));
OR2 U465 ( .A(n454), .B(n455), .Z(po13));
OR2 U466 ( .A(n456), .B(n457), .Z(n455));
AN2 U467 ( .A(pi25), .B(n458), .Z(n457));
OR2 U468 ( .A(n459), .B(n460), .Z(n458));
OR2 U469 ( .A(n461), .B(n462), .Z(n460));
AN2 U470 ( .A(n463), .B(n464), .Z(n461));
OR2 U471 ( .A(n282), .B(n465), .Z(n464));
OR2 U472 ( .A(pi12), .B(pi09), .Z(n465));
IV2 U473 ( .A(pi50), .Z(n463));
AN2 U474 ( .A(pi07), .B(n466), .Z(n456));
OR2 U475 ( .A(n467), .B(n468), .Z(n466));
OR2 U476 ( .A(n469), .B(n429), .Z(n468));
AN2 U477 ( .A(pi28), .B(n470), .Z(n429));
AN2 U478 ( .A(n400), .B(n471), .Z(n469));
OR2 U479 ( .A(pi40), .B(n431), .Z(n471));
OR2 U480 ( .A(pi43), .B(n289), .Z(n467));
AN2 U481 ( .A(pi19), .B(pi33), .Z(n289));
OR2 U482 ( .A(po01), .B(n472), .Z(n454));
OR2 U483 ( .A(po28), .B(po16), .Z(n472));
OR2 U484 ( .A(n473), .B(n474), .Z(po10));
AN2 U485 ( .A(n475), .B(pi41), .Z(n474));
AN2 U486 ( .A(n476), .B(n477), .Z(n475));
OR2 U487 ( .A(n297), .B(n343), .Z(n476));
AN2 U488 ( .A(n478), .B(n479), .Z(n473));
AN2 U489 ( .A(n283), .B(n296), .Z(n479));
AN2 U490 ( .A(pi29), .B(n345), .Z(n478));
IV2 U491 ( .A(n480), .Z(n345));
IV2 U492 ( .A(po07), .Z(po09));
OR2 U493 ( .A(n481), .B(n482), .Z(po08));
AN2 U494 ( .A(pi45), .B(pi39), .Z(n482));
AN2 U495 ( .A(n483), .B(n484), .Z(n481));
OR2 U496 ( .A(n485), .B(n486), .Z(n484));
AN2 U497 ( .A(pi29), .B(n312), .Z(n486));
AN2 U498 ( .A(n296), .B(n309), .Z(n312));
AN2 U499 ( .A(n351), .B(n487), .Z(n485));
OR2 U500 ( .A(n488), .B(n326), .Z(n487));
AN2 U501 ( .A(pi06), .B(n357), .Z(n488));
AN2 U502 ( .A(pi03), .B(pi28), .Z(n351));
AN2 U503 ( .A(n323), .B(n431), .Z(n483));
OR2 U504 ( .A(n489), .B(n490), .Z(po07));
OR2 U505 ( .A(pi33), .B(n311), .Z(n490));
IV2 U506 ( .A(n491), .Z(n311));
OR2 U507 ( .A(n492), .B(n493), .Z(n491));
OR2 U508 ( .A(n494), .B(n297), .Z(n493));
IV2 U509 ( .A(pi08), .Z(n297));
AN2 U510 ( .A(n375), .B(n369), .Z(n494));
IV2 U511 ( .A(n448), .Z(n375));
OR2 U512 ( .A(n477), .B(n366), .Z(n448));
OR2 U513 ( .A(n431), .B(n344), .Z(n477));
IV2 U514 ( .A(pi16), .Z(n344));
OR2 U515 ( .A(n495), .B(n496), .Z(n492));
OR2 U516 ( .A(pi00), .B(n339), .Z(n496));
AN2 U517 ( .A(n369), .B(n343), .Z(n339));
IV2 U518 ( .A(n497), .Z(n495));
OR2 U519 ( .A(n498), .B(pi40), .Z(n497));
AN2 U520 ( .A(n369), .B(pi41), .Z(n498));
OR2 U521 ( .A(po05), .B(n422), .Z(n489));
OR2 U522 ( .A(po25), .B(po24), .Z(n422));
OR2 U523 ( .A(n499), .B(n500), .Z(po06));
AN2 U524 ( .A(pi27), .B(n501), .Z(n500));
AN2 U525 ( .A(n502), .B(n503), .Z(n499));
AN2 U526 ( .A(n504), .B(n480), .Z(n503));
OR2 U527 ( .A(n431), .B(n366), .Z(n480));
IV2 U528 ( .A(pi14), .Z(n431));
AN2 U529 ( .A(n470), .B(n296), .Z(n504));
IV2 U530 ( .A(pi07), .Z(n296));
IV2 U531 ( .A(pi03), .Z(n470));
AN2 U532 ( .A(pi28), .B(n279), .Z(n502));
AN2 U533 ( .A(pi26), .B(n501), .Z(po04));
OR2 U534 ( .A(pi21), .B(n323), .Z(n501));
AN2 U535 ( .A(n505), .B(n506), .Z(po03));
AN2 U536 ( .A(n507), .B(n279), .Z(n506));
AN2 U537 ( .A(n369), .B(n283), .Z(n279));
IV2 U538 ( .A(pi21), .Z(n369));
AN2 U539 ( .A(n442), .B(n400), .Z(n507));
OR2 U540 ( .A(pi29), .B(pi40), .Z(n400));
OR2 U541 ( .A(n366), .B(n343), .Z(n442));
IV2 U542 ( .A(pi06), .Z(n343));
IV2 U543 ( .A(pi15), .Z(n366));
AN2 U544 ( .A(n326), .B(pi14), .Z(n505));
AN2 U545 ( .A(n508), .B(n443), .Z(n326));
IV2 U546 ( .A(n357), .Z(n443));
OR2 U547 ( .A(pi04), .B(pi20), .Z(n357));
OR2 U548 ( .A(n509), .B(n510), .Z(po02));
OR2 U549 ( .A(n511), .B(n512), .Z(n510));
AN2 U550 ( .A(pi44), .B(pi39), .Z(n512));
AN2 U551 ( .A(n513), .B(n514), .Z(n511));
AN2 U552 ( .A(n515), .B(n516), .Z(n514));
AN2 U553 ( .A(n309), .B(n306), .Z(n515));
IV2 U554 ( .A(pi10), .Z(n306));
AN2 U555 ( .A(n417), .B(pi25), .Z(n513));
IV2 U556 ( .A(n517), .Z(n417));
OR2 U557 ( .A(n518), .B(n519), .Z(n509));
AN2 U558 ( .A(n520), .B(pi09), .Z(n519));
AN2 U559 ( .A(n521), .B(pi02), .Z(n520));
AN2 U560 ( .A(pi31), .B(n508), .Z(n521));
IV2 U561 ( .A(pi22), .Z(n508));
AN2 U562 ( .A(n522), .B(n272), .Z(n518));
IV2 U563 ( .A(pi09), .Z(n272));
AN2 U564 ( .A(n523), .B(n524), .Z(n522));
AN2 U565 ( .A(n525), .B(pi35), .Z(n524));
AN2 U566 ( .A(pi21), .B(n526), .Z(n525));
IV2 U567 ( .A(pi13), .Z(n526));
AN2 U568 ( .A(pi01), .B(n283), .Z(n523));
AN2 U569 ( .A(n323), .B(n309), .Z(n283));
IV2 U570 ( .A(pi00), .Z(n309));
IV2 U571 ( .A(pi12), .Z(n323));
OR2 U572 ( .A(n527), .B(n528), .Z(po00));
AN2 U573 ( .A(po01), .B(n459), .Z(n528));
OR2 U574 ( .A(pi30), .B(pi42), .Z(po01));
AN2 U575 ( .A(pi25), .B(n529), .Z(n527));
OR2 U576 ( .A(n530), .B(n517), .Z(n529));
OR2 U577 ( .A(n531), .B(n532), .Z(n517));
OR2 U578 ( .A(n462), .B(n459), .Z(n532));
IV2 U579 ( .A(pi01), .Z(n459));
IV2 U580 ( .A(pi11), .Z(n462));
OR2 U581 ( .A(pi13), .B(pi12), .Z(n531));
AN2 U582 ( .A(n533), .B(n282), .Z(n530));
IV2 U583 ( .A(pi17), .Z(n282));
IV2 U584 ( .A(n516), .Z(n533));
OR2 U585 ( .A(pi09), .B(pi21), .Z(n516));
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

41
examples/smtbmc/glift/x1.ys Normal file
View file

@ -0,0 +1,41 @@
read_verilog x1.v
techmap
flatten
select x1_lev2
glift -create-instrumented-model
techmap
opt
rename x1_lev2 uut
cd ..
delete [AIONX][NVXR]2
read_verilog x1.v
techmap
flatten
select x1_lev2
glift -create-precise-model
techmap
opt
rename x1_lev2 spec
cd ..
delete [AIONX][NVXR]2
design -push-copy
miter -equiv spec uut miter
flatten
delete uut spec
techmap
opt
stat miter
qbfsat -O2 -write-solution x1.soln -solver yices -timeout 3600 -nocleanup -assume-outputs -assume-negative-polarity miter
design -pop
stat
copy uut solved
qbfsat -specialize-from-file x1.soln solved
opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
stat
shell

1
passes/cmds/Makefile.inc
View file

@ -18,6 +18,7 @@ OBJS += passes/cmds/setattr.o
OBJS += passes/cmds/copy.o
OBJS += passes/cmds/splice.o
OBJS += passes/cmds/scc.o
OBJS += passes/cmds/glift.o
OBJS += passes/cmds/torder.o
OBJS += passes/cmds/logcmd.o
OBJS += passes/cmds/tee.o

599
passes/cmds/glift.cc Normal file
View file

@ -0,0 +1,599 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*
*/
#include "kernel/register.h"
#include "kernel/rtlil.h"
#include "kernel/utils.h"
#include "kernel/log.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct GliftWorker {
private:
bool is_top_module = false;
bool opt_create_precise_model = false, opt_create_imprecise_model = false, opt_create_instrumented_model = false;
bool opt_taintconstants = false, opt_keepoutputs = false, opt_simplecostmodel = false, opt_nocostmodel = false;
bool opt_instrumentmore = false;
std::vector<RTLIL::Wire *> new_taint_outputs;
std::vector<std::pair<RTLIL::SigSpec, RTLIL::IdString>> meta_mux_selects;
RTLIL::Module *module = nullptr;
const RTLIL::IdString cost_model_wire_name = ID(__glift_weight);
const RTLIL::IdString glift_attribute_name = ID(glift);
RTLIL::SigSpec get_corresponding_taint_signal(RTLIL::SigSpec sig) {
RTLIL::SigSpec ret;
//Get the connected wire for the cell port:
log_assert(sig.is_wire() || sig.is_fully_const());
log_assert(sig.is_wire() || sig.is_fully_const());
//Get a SigSpec for the corresponding taint signal for the cell port, creating one if necessary:
if (sig.is_wire()) {
RTLIL::Wire *w = module->wire(sig.as_wire()->name.str() + "_t");
if (w == nullptr) w = module->addWire(sig.as_wire()->name.str() + "_t", 1);
ret = w;
}
else if (sig.is_fully_const() && opt_taintconstants)
ret = RTLIL::State::S1;
else if (sig.is_fully_const())
ret = RTLIL::State::S0;
else
log_cmd_error("Cell port SigSpec has unexpected type.\n");
//Finally, if the cell port was a module input or output, make sure the corresponding taint signal is marked, too:
if(sig.is_wire() && sig.as_wire()->port_input)
ret.as_wire()->port_input = true;
if(sig.is_wire() && sig.as_wire()->port_output)
new_taint_outputs.push_back(ret.as_wire());
return ret;
}
void add_precise_GLIFT_logic(const RTLIL::Cell *cell, RTLIL::SigSpec &port_a, RTLIL::SigSpec &port_a_taint, RTLIL::SigSpec &port_b, RTLIL::SigSpec &port_b_taint, RTLIL::SigSpec &port_y_taint) {
//AKA AN2_SH2 or OR2_SH2
bool is_and = cell->type.in(ID($_AND_), ID($_NAND_));
RTLIL::SigSpec n_port_a = module->LogicNot(cell->name.str() + "_t_1_1", port_a, false, cell->get_src_attribute());
RTLIL::SigSpec n_port_b = module->LogicNot(cell->name.str() + "_t_1_2", port_b, false, cell->get_src_attribute());
auto subexpr1 = module->And(cell->name.str() + "_t_1_3", is_and? port_a : n_port_a, port_b_taint, false, cell->get_src_attribute());
auto subexpr2 = module->And(cell->name.str() + "_t_1_4", is_and? port_b : n_port_b, port_a_taint, false, cell->get_src_attribute());
auto subexpr3 = module->And(cell->name.str() + "_t_1_5", port_a_taint, port_b_taint, false, cell->get_src_attribute());
auto subexpr4 = module->Or(cell->name.str() + "_t_1_6", subexpr1, subexpr2, false, cell->get_src_attribute());
module->addOr(cell->name.str() + "_t_1_7", subexpr4, subexpr3, port_y_taint, false, cell->get_src_attribute());
}
void add_imprecise_GLIFT_logic_1(const RTLIL::Cell *cell, RTLIL::SigSpec &port_a, RTLIL::SigSpec &port_a_taint, RTLIL::SigSpec &port_b, RTLIL::SigSpec &port_b_taint, RTLIL::SigSpec &port_y_taint) {
//AKA AN2_SH3 or OR2_SH3
bool is_and = cell->type.in(ID($_AND_), ID($_NAND_));
RTLIL::SigSpec n_port_a = module->LogicNot(cell->name.str() + "_t_2_1", port_a, false, cell->get_src_attribute());
auto subexpr1 = module->And(cell->name.str() + "_t_2_2", is_and? port_b : n_port_a, is_and? port_a_taint : port_b_taint, false, cell->get_src_attribute());
module->addOr(cell->name.str() + "_t_2_3", is_and? port_b_taint : port_a_taint, subexpr1, port_y_taint, false, cell->get_src_attribute());
}
void add_imprecise_GLIFT_logic_2(const RTLIL::Cell *cell, RTLIL::SigSpec &port_a, RTLIL::SigSpec &port_a_taint, RTLIL::SigSpec &port_b, RTLIL::SigSpec &port_b_taint, RTLIL::SigSpec &port_y_taint) {
//AKA AN2_SH4 or OR2_SH4
bool is_and = cell->type.in(ID($_AND_), ID($_NAND_));
RTLIL::SigSpec n_port_b = module->LogicNot(cell->name.str() + "_t_3_1", port_b, false, cell->get_src_attribute());
auto subexpr1 = module->And(cell->name.str() + "_t_3_2", is_and? port_a : n_port_b, is_and? port_b_taint : port_a_taint, false, cell->get_src_attribute());
module->addOr(cell->name.str() + "_t_3_3", is_and? port_a_taint : port_b_taint, subexpr1, port_y_taint, false, cell->get_src_attribute());
}
void add_imprecise_GLIFT_logic_3(const RTLIL::Cell *cell, RTLIL::SigSpec &port_a_taint, RTLIL::SigSpec &port_b_taint, RTLIL::SigSpec &port_y_taint) {
//AKA AN2_SH5 or OR2_SH5 or XR2_SH2
module->addOr(cell->name.str() + "_t_4_1", port_a_taint, port_b_taint, port_y_taint, false, cell->get_src_attribute());
}
void add_imprecise_GLIFT_logic_4(RTLIL::SigSpec &port_a_taint, RTLIL::SigSpec &port_y_taint) {
module->connect(port_y_taint, port_a_taint);
}
void add_imprecise_GLIFT_logic_5(RTLIL::SigSpec &port_b_taint, RTLIL::SigSpec &port_y_taint) {
module->connect(port_y_taint, port_b_taint);
}
void add_imprecise_GLIFT_logic_6(RTLIL::SigSpec &port_y_taint) {
module->connect(port_y_taint, RTLIL::Const(1, 1));
}
void add_imprecise_GLIFT_logic_7(RTLIL::SigSpec &port_y_taint) {
module->connect(port_y_taint, RTLIL::Const(0, 1));
}
void add_precise_GLIFT_mux(const RTLIL::Cell *cell, RTLIL::SigSpec &port_a, RTLIL::SigSpec &port_a_taint, RTLIL::SigSpec &port_b, RTLIL::SigSpec &port_b_taint, RTLIL::SigSpec &port_s, RTLIL::SigSpec &port_s_taint, RTLIL::SigSpec &port_y_taint) {
//S&At | ~S&Bt | ~A&B&St | A&~B&St | At&St | Bt&St
RTLIL::SigSpec n_port_a = module->LogicNot(cell->name.str() + "_t_4_1", port_a, false, cell->get_src_attribute());
RTLIL::SigSpec n_port_b = module->LogicNot(cell->name.str() + "_t_4_2", port_b, false, cell->get_src_attribute());
RTLIL::SigSpec n_port_s = module->LogicNot(cell->name.str() + "_t_4_3", port_s, false, cell->get_src_attribute());
auto subexpr1 = module->And(cell->name.str() + "_t_4_4", port_s, port_a_taint, false, cell->get_src_attribute());
auto subexpr2 = module->And(cell->name.str() + "_t_4_5", n_port_s, port_b_taint, false, cell->get_src_attribute());
auto subexpr3 = module->And(cell->name.str() + "_t_4_6", n_port_a, port_b, false, cell->get_src_attribute());
auto subexpr4 = module->And(cell->name.str() + "_t_4_7", subexpr3, port_s_taint, false, cell->get_src_attribute());
auto subexpr5 = module->And(cell->name.str() + "_t_4_8", port_a, n_port_b, false, cell->get_src_attribute());
auto subexpr6 = module->And(cell->name.str() + "_t_4_9", subexpr5, port_s_taint, false, cell->get_src_attribute());
auto subexpr7 = module->And(cell->name.str() + "_t_4_10", port_a_taint, port_s_taint, false, cell->get_src_attribute());
auto subexpr8 = module->And(cell->name.str() + "_t_4_11", port_b_taint, port_s_taint, false, cell->get_src_attribute());
auto subexpr9 = module->Or(cell->name.str() + "_t_4_12", subexpr1, subexpr2, false, cell->get_src_attribute());
auto subexpr10 = module->Or(cell->name.str() + "_t_4_13", subexpr4, subexpr6, false, cell->get_src_attribute());
auto subexpr11 = module->Or(cell->name.str() + "_t_4_14", subexpr7, subexpr8, false, cell->get_src_attribute());
auto subexpr12 = module->Or(cell->name.str() + "_t_4_15", subexpr9, subexpr10, false, cell->get_src_attribute());
module->addOr(cell->name.str() + "_t_4_16", subexpr11, subexpr12, port_y_taint, false, cell->get_src_attribute());
}
RTLIL::SigSpec score_metamux_select(const RTLIL::SigSpec &metamux_select, const RTLIL::IdString celltype) {
log_assert(metamux_select.is_wire());
if (opt_simplecostmodel) {
//The complex model is an area model, so a lower score should mean smaller.
//In this case, a nonzero hole metamux select value means less logic.
//Thus we should invert the ReduceOr over the metamux_select signal.
RTLIL::SigSpec pmux_select = module->ReduceOr(metamux_select.as_wire()->name.str() + "_nonzero", metamux_select);
return module->Pmux(NEW_ID, RTLIL::Const(1), RTLIL::Const(0), pmux_select, metamux_select.as_wire()->get_src_attribute());
} else {
auto select_width = metamux_select.as_wire()->width;
std::vector<RTLIL::Const> costs;
if (celltype == ID($_AND_) || celltype == ID($_OR_)) {
costs = {5, 2, 2, 1, 0, 0, 0, 0};
log_assert(select_width == 2 || select_width == 3);
log_assert(opt_instrumentmore || select_width == 2);
log_assert(!opt_instrumentmore || select_width == 3);
}
else if (celltype == ID($_XOR_) || celltype == ID($_XNOR_)) {
costs = {1, 0, 0, 0};
log_assert(select_width == 2);
}
std::vector<RTLIL::SigSpec> next_pmux_y_ports, pmux_y_ports(costs.begin(), costs.begin() + exp2(select_width));
for (auto i = 0; pmux_y_ports.size() > 1; ++i) {
for (auto j = 0; j+1 < GetSize(pmux_y_ports); j += 2) {
next_pmux_y_ports.emplace_back(module->Pmux(stringf("%s_mux_%d_%d", metamux_select.as_wire()->name.c_str(), i, j), pmux_y_ports[j], pmux_y_ports[j+1], metamux_select[GetSize(metamux_select) - 1 - i], metamux_select.as_wire()->get_src_attribute()));
}
if (GetSize(pmux_y_ports) % 2 == 1)
next_pmux_y_ports.push_back(pmux_y_ports[GetSize(pmux_y_ports) - 1]);
pmux_y_ports.swap(next_pmux_y_ports);
next_pmux_y_ports.clear();
}
log_assert(pmux_y_ports.size() == 1);
return pmux_y_ports[0];
}
}
void create_glift_logic() {
if (module->get_bool_attribute(glift_attribute_name))
return;
std::vector<RTLIL::SigSig> connections(module->connections());
for(auto &cell : module->cells().to_vector()) {
if (!cell->type.in({ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_MUX_), ID($_NMUX_), ID($_NOT_), ID($anyconst), ID($allconst), ID($assume), ID($assert)}) && module->design->module(cell->type) == nullptr) {
log_cmd_error("Unsupported cell type \"%s\" found. Run `techmap` first.\n", cell->type.c_str());
}
if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_))) {
const unsigned int A = 0, B = 1, Y = 2;
const unsigned int NUM_PORTS = 3;
RTLIL::SigSpec ports[NUM_PORTS] = {cell->getPort(ID::A), cell->getPort(ID::B), cell->getPort(ID::Y)};
RTLIL::SigSpec port_taints[NUM_PORTS];
if (ports[A].size() != 1 || ports[B].size() != 1 || ports[Y].size() != 1)
log_cmd_error("Multi-bit signal found. Run `splitnets` first.\n");
for (unsigned int i = 0; i < NUM_PORTS; ++i)
port_taints[i] = get_corresponding_taint_signal(ports[i]);
if (opt_create_precise_model)
add_precise_GLIFT_logic(cell, ports[A], port_taints[A], ports[B], port_taints[B], port_taints[Y]);
else if (opt_create_imprecise_model)
add_imprecise_GLIFT_logic_3(cell, port_taints[A], port_taints[B], port_taints[Y]);
else if (opt_create_instrumented_model) {
std::vector<RTLIL::SigSpec> taint_version;
int num_versions = opt_instrumentmore? 8 : 4;
for (auto i = 1; i <= num_versions; ++i)
taint_version.emplace_back(RTLIL::SigSpec(module->addWire(stringf("%s_y%d", cell->name.c_str(), i), 1)));
for (auto i = 0; i < num_versions; ++i) {
switch(i) {
case 0: add_precise_GLIFT_logic(cell, ports[A], port_taints[A], ports[B], port_taints[B], taint_version[i]);
break;
case 1: add_imprecise_GLIFT_logic_1(cell, ports[A], port_taints[A], ports[B], port_taints[B], taint_version[i]);
break;
case 2: add_imprecise_GLIFT_logic_2(cell, ports[A], port_taints[A], ports[B], port_taints[B], taint_version[i]);
break;
case 3: add_imprecise_GLIFT_logic_3(cell, port_taints[A], port_taints[B], taint_version[i]);
break;
case 4: add_imprecise_GLIFT_logic_4(port_taints[A], taint_version[i]);
break;
case 5: add_imprecise_GLIFT_logic_5(port_taints[B], taint_version[i]);
break;
case 6: add_imprecise_GLIFT_logic_6(taint_version[i]);
break;
case 7: add_imprecise_GLIFT_logic_7(taint_version[i]);
break;
default: log_assert(false);
}
}
auto select_width = log2(num_versions);
log_assert(exp2(select_width) == num_versions);
RTLIL::SigSpec meta_mux_select(module->addWire(cell->name.str() + "_sel", select_width));
meta_mux_selects.push_back(make_pair(meta_mux_select, cell->type));
module->connect(meta_mux_select, module->Anyconst(cell->name.str() + "_hole", select_width, cell->get_src_attribute()));
std::vector<RTLIL::SigSpec> next_meta_mux_y_ports, meta_mux_y_ports(taint_version);
for (auto i = 0; meta_mux_y_ports.size() > 1; ++i) {
for (auto j = 0; j+1 < GetSize(meta_mux_y_ports); j += 2) {
next_meta_mux_y_ports.emplace_back(module->Mux(stringf("%s_mux_%d_%d", cell->name.c_str(), i, j), meta_mux_y_ports[j], meta_mux_y_ports[j+1], meta_mux_select[GetSize(meta_mux_select) - 1 - i]));
}
if (GetSize(meta_mux_y_ports) % 2 == 1)
next_meta_mux_y_ports.push_back(meta_mux_y_ports[GetSize(meta_mux_y_ports) - 1]);
meta_mux_y_ports.swap(next_meta_mux_y_ports);
next_meta_mux_y_ports.clear();
}
log_assert(meta_mux_y_ports.size() == 1);
module->connect(port_taints[Y], meta_mux_y_ports[0]);
}
else log_cmd_error("This is a bug (1).\n");
}
else if (cell->type.in(ID($_XOR_), ID($_XNOR_))) {
const unsigned int A = 0, B = 1, Y = 2;
const unsigned int NUM_PORTS = 3;
RTLIL::SigSpec ports[NUM_PORTS] = {cell->getPort(ID::A), cell->getPort(ID::B), cell->getPort(ID::Y)};
RTLIL::SigSpec port_taints[NUM_PORTS];
if (ports[A].size() != 1 || ports[B].size() != 1 || ports[Y].size() != 1)
log_cmd_error("Multi-bit signal found. Run `splitnets` first.\n");
for (unsigned int i = 0; i < NUM_PORTS; ++i)
port_taints[i] = get_corresponding_taint_signal(ports[i]);
if (opt_create_precise_model || opt_create_imprecise_model)
add_imprecise_GLIFT_logic_3(cell, port_taints[A], port_taints[B], port_taints[Y]);
else if (opt_create_instrumented_model) {
std::vector<RTLIL::SigSpec> taint_version;
int num_versions = 4;
auto select_width = log2(num_versions);
log_assert(exp2(select_width) == num_versions);
for (auto i = 1; i <= num_versions; ++i)
taint_version.emplace_back(RTLIL::SigSpec(module->addWire(stringf("%s_y%d", cell->name.c_str(), i), 1)));
for (auto i = 0; i < num_versions; ++i) {
switch(i) {
case 0: add_imprecise_GLIFT_logic_3(cell, port_taints[A], port_taints[B], taint_version[i]);
break;
case 1: add_imprecise_GLIFT_logic_4(port_taints[A], taint_version[i]);
break;
case 2: add_imprecise_GLIFT_logic_5(port_taints[B], taint_version[i]);
break;
case 3: add_imprecise_GLIFT_logic_6(taint_version[i]);
break;
default: log_assert(false);
}
}
RTLIL::SigSpec meta_mux_select(module->addWire(cell->name.str() + "_sel", select_width));
meta_mux_selects.push_back(make_pair(meta_mux_select, cell->type));
module->connect(meta_mux_select, module->Anyconst(cell->name.str() + "_hole", select_width, cell->get_src_attribute()));
std::vector<RTLIL::SigSpec> next_meta_mux_y_ports, meta_mux_y_ports(taint_version);
for (auto i = 0; meta_mux_y_ports.size() > 1; ++i) {
for (auto j = 0; j+1 < GetSize(meta_mux_y_ports); j += 2) {
next_meta_mux_y_ports.emplace_back(module->Mux(stringf("%s_mux_%d_%d", cell->name.c_str(), i, j), meta_mux_y_ports[j], meta_mux_y_ports[j+1], meta_mux_select[GetSize(meta_mux_select) - 1 - i]));
}
if (GetSize(meta_mux_y_ports) % 2 == 1)
next_meta_mux_y_ports.push_back(meta_mux_y_ports[GetSize(meta_mux_y_ports) - 1]);
meta_mux_y_ports.swap(next_meta_mux_y_ports);
next_meta_mux_y_ports.clear();
}
log_assert(meta_mux_y_ports.size() == 1);
module->connect(port_taints[Y], meta_mux_y_ports[0]);
}
else log_cmd_error("This is a bug (2).\n");
}
else if (cell->type.in(ID($_MUX_), ID($_NMUX_))) {
const unsigned int A = 0, B = 1, S = 2, Y = 3;
const unsigned int NUM_PORTS = 4;
RTLIL::SigSpec ports[NUM_PORTS] = {cell->getPort(ID::A), cell->getPort(ID::B), cell->getPort(ID::S), cell->getPort(ID::Y)};
RTLIL::SigSpec port_taints[NUM_PORTS];
if (ports[A].size() != 1 || ports[B].size() != 1 || ports[S].size() != 1 || ports[Y].size() != 1)
log_cmd_error("Multi-bit signal found. Run `splitnets` first.\n");
for (unsigned int i = 0; i < NUM_PORTS; ++i)
port_taints[i] = get_corresponding_taint_signal(ports[i]);
add_precise_GLIFT_mux(cell, ports[A], port_taints[A], ports[B], port_taints[B], ports[S], port_taints[S], port_taints[Y]);
}
else if (cell->type.in(ID($_NOT_))) {
const unsigned int A = 0, Y = 1;
const unsigned int NUM_PORTS = 2;
RTLIL::SigSpec ports[NUM_PORTS] = {cell->getPort(ID::A), cell->getPort(ID::Y)};
RTLIL::SigSpec port_taints[NUM_PORTS];
if (ports[A].size() != 1 || ports[Y].size() != 1)
log_cmd_error("Multi-bit signal found. Run `splitnets` first.\n");
for (unsigned int i = 0; i < NUM_PORTS; ++i)
port_taints[i] = get_corresponding_taint_signal(ports[i]);
if (cell->type == ID($_NOT_)) {
module->connect(port_taints[Y], port_taints[A]);
}
else log_cmd_error("This is a bug (3).\n");
}
else if (module->design->module(cell->type) != nullptr) {
//User cell type
//This function is called on modules according to topological order, so we do not need to
//recurse to GLIFT model the child module. However, we need to augment the ports list
//with taint signals and connect the new ports to the corresponding taint signals.
RTLIL::Module *cell_module_def = module->design->module(cell->type);
dict<RTLIL::IdString, RTLIL::SigSpec> orig_ports = cell->connections();
log("Adding cell %s\n", cell_module_def->name.c_str());
for (auto &it : orig_ports) {
RTLIL::SigSpec port = it.second;
RTLIL::SigSpec port_taint = get_corresponding_taint_signal(port);
log_assert(port_taint.is_wire());
log_assert(std::find(cell_module_def->ports.begin(), cell_module_def->ports.end(), port_taint.as_wire()->name) != cell_module_def->ports.end());
cell->setPort(port_taint.as_wire()->name, port_taint);
}
}
else log_cmd_error("This is a bug (4).\n");
} //end foreach cell in cells
for (auto &conn : connections) {
RTLIL::SigSpec first = get_corresponding_taint_signal(conn.first);
RTLIL::SigSpec second = get_corresponding_taint_signal(conn.second);
module->connect(first, second);
if(conn.second.is_wire() && conn.second.as_wire()->port_input)
second.as_wire()->port_input = true;
if(conn.first.is_wire() && conn.first.as_wire()->port_output)
new_taint_outputs.push_back(first.as_wire());
} //end foreach conn in connections
//Create a rough model of area by summing the (potentially simplified) "weight" score of each meta-mux select:
if (!opt_nocostmodel) {
std::vector<RTLIL::SigSpec> meta_mux_select_sums;
std::vector<RTLIL::SigSpec> meta_mux_select_sums_buf;
for (auto &it : meta_mux_selects) {
meta_mux_select_sums.emplace_back(score_metamux_select(it.first, it.second));
}
for (unsigned int i = 0; meta_mux_select_sums.size() > 1; ) {
meta_mux_select_sums_buf.clear();
for (i = 0; i + 1 < meta_mux_select_sums.size(); i += 2) {
meta_mux_select_sums_buf.push_back(module->Add(meta_mux_select_sums[i].as_wire()->name.str() + "_add", meta_mux_select_sums[i], meta_mux_select_sums[i+1], false));
}
if (meta_mux_select_sums.size() % 2 == 1)
meta_mux_select_sums_buf.push_back(meta_mux_select_sums[meta_mux_select_sums.size()-1]);
meta_mux_select_sums.swap(meta_mux_select_sums_buf);
}
if (meta_mux_select_sums.size() > 0) {
meta_mux_select_sums[0].as_wire()->set_bool_attribute("\\minimize");
meta_mux_select_sums[0].as_wire()->set_bool_attribute("\\keep");
module->rename(meta_mux_select_sums[0].as_wire(), cost_model_wire_name);
}
}
//Mark new module outputs:
for (auto &port_name : module->ports) {
RTLIL::Wire *port = module->wire(port_name);
log_assert(port != nullptr);
if (is_top_module && port->port_output && !opt_keepoutputs)
port->port_output = false;
}
for (auto &output : new_taint_outputs)
output->port_output = true;
module->fixup_ports(); //we have some new taint signals in the module interface
module->set_bool_attribute(glift_attribute_name, true);
}
public:
GliftWorker(RTLIL::Module *_module, bool _is_top_module, bool _opt_create_precise_model, bool _opt_create_imprecise_model, bool _opt_create_instrumented_model, bool _opt_taintconstants, bool _opt_keepoutputs, bool _opt_simplecostmodel, bool _opt_nocostmodel, bool _opt_instrumentmore) {
module = _module;
is_top_module = _is_top_module;
opt_create_precise_model = _opt_create_precise_model;
opt_create_imprecise_model = _opt_create_imprecise_model;
opt_create_instrumented_model = _opt_create_instrumented_model;
opt_taintconstants = _opt_taintconstants;
opt_keepoutputs = _opt_keepoutputs;
opt_simplecostmodel = _opt_simplecostmodel;
opt_nocostmodel = _opt_nocostmodel;
opt_instrumentmore = _opt_instrumentmore;
create_glift_logic();
}
};
struct GliftPass : public Pass {
GliftPass() : Pass("glift", "create GLIFT models and optimization problems") {}
void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" glift <command> [options] [selection]\n");
log("\n");
log("Augments the current or specified module with gate-level information flow tracking\n");
log("(GLIFT) logic using the \"constructive mapping\" approach. Also can set up QBF-SAT\n");
log("optimization problems in order to optimize GLIFT models or trade off precision and\n");
log("complexity.\n");
log("\n");
log("\n");
log("Commands:\n");
log("\n");
log(" -create-precise-model\n");
log(" Replaces the current or specified module with one that has corresponding \"taint\"\n");
log(" inputs, outputs, and internal nets along with precise taint tracking logic.\n");
log(" For example, precise taint tracking logic for an AND gate is:\n");
log("\n");
log(" y_t = a & b_t | b & a_t | a_t & b_t\n");
log("\n");
log("\n");
log(" -create-imprecise-model\n");
log(" Replaces the current or specified module with one that has corresponding \"taint\"\n");
log(" inputs, outputs, and internal nets along with imprecise \"All OR\" taint tracking\n");
log(" logic:\n");
log("\n");
log(" y_t = a_t | b_t\n");
log("\n");
log("\n");
log(" -create-instrumented-model\n");
log(" Replaces the current or specified module with one that has corresponding \"taint\"\n");
log(" inputs, outputs, and internal nets along with 4 varying-precision versions of taint\n");
log(" tracking logic. Which version of taint tracking logic is used for a given gate is\n");
log(" determined by a MUX selected by an $anyconst cell. By default, unless the\n");
log(" `-no-cost-model` option is provided, an additional wire named `__glift_weight` with\n");
log(" the `keep` and `minimize` attributes is added to the module along with pmuxes and\n");
log(" adders to calculate a rough estimate of the number of logic gates in the GLIFT model\n");
log(" given an assignment for the $anyconst cells. The four versions of taint tracking logic\n");
log(" for an AND gate are:");
log("\n");
log(" y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`)\n");
log(" y_t = a_t | a & b_t\n");
log(" y_t = b_t | b & a_t\n");
log(" y_t = a_t | b_t (like `-create-imprecise-model`)\n");
log("\n");
log("\n");
log("Options:\n");
log("\n");
log(" -taint-constants\n");
log(" Constant values in the design are labeled as tainted.\n");
log(" (default: label constants as un-tainted)\n");
log("\n");
log(" -keep-outputs\n");
log(" Do not remove module outputs. Taint tracking outputs will appear in the module ports\n");
log(" alongside the orignal outputs.\n");
log(" (default: original module outputs are removed)\n");
log("\n");
log(" -simple-cost-model\n");
log(" Do not model logic area. Instead model the number of non-zero assignments to $anyconsts.\n");
log(" Taint tracking logic versions vary in their size, but all reduced-precision versions are\n");
log(" significantly smaller than the fully-precise version. A non-zero $anyconst assignment means\n");
log(" that reduced-precision taint tracking logic was chosen for some gate.\n");
log(" Only applicable in combination with `-create-instrumented-model`.\n");
log(" (default: use a complex model and give that wire the \"keep\" and \"minimize\" attributes)\n");
log("\n");
log(" -no-cost-model\n");
log(" Do not model taint tracking logic area and do not create a `__glift_weight` wire.\n");
log(" Only applicable in combination with `-create-instrumented-model`.\n");
log(" (default: model area and give that wire the \"keep\" and \"minimize\" attributes)\n");
log("\n");
log(" -instrument-more\n");
log(" Allow choice from more versions of (even simpler) taint tracking logic. A total\n");
log(" of 8 versions of taint tracking logic will be added per gate, including the 4\n");
log(" versions from `-create-instrumented-model` and these additional versions:\n");
log("\n");
log(" y_t = a_t\n");
log(" y_t = b_t\n");
log(" y_t = 1\n");
log(" y_t = 0\n");
log("\n");
log(" Only applicable in combination with `-create-instrumented-model`.\n");
log(" (default: do not add more versions of taint tracking logic.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool opt_create_precise_model = false, opt_create_imprecise_model = false, opt_create_instrumented_model = false;
bool opt_taintconstants = false, opt_keepoutputs = false, opt_simplecostmodel = false, opt_nocostmodel = false;
bool opt_instrumentmore = false;
log_header(design, "Executing GLIFT pass (creating and manipulating GLIFT models).\n");
std::vector<std::string>::size_type argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-create-precise-model") {
opt_create_precise_model = true;
continue;
}
if (args[argidx] == "-create-imprecise-model") {
opt_create_imprecise_model = true;
continue;
}
if (args[argidx] == "-create-instrumented-model") {
opt_create_instrumented_model = true;
continue;
}
if (args[argidx] == "-taint-constants") {
opt_taintconstants = true;
continue;
}
if (args[argidx] == "-keep-outputs") {
opt_keepoutputs = true;
continue;
}
if (args[argidx] == "-simple-cost-model") {
opt_simplecostmodel = true;
continue;
}
if (args[argidx] == "-no-cost-model") {
opt_nocostmodel = true;
continue;
}
if (args[argidx] == "-instrument-more") {
opt_instrumentmore = true;
continue;
}
break;
}
if(!opt_create_precise_model && !opt_create_imprecise_model && !opt_create_instrumented_model)
log_cmd_error("No command provided. See help for usage.\n");
if(static_cast<int>(opt_create_precise_model) + static_cast<int>(opt_create_imprecise_model) + static_cast<int>(opt_create_instrumented_model) != 1)
log_cmd_error("Only one command may be specified. See help for usage.\n");
if(opt_simplecostmodel && opt_nocostmodel)
log_cmd_error("Only one of `-simple-cost-model` and `-no-cost-model` may be specified. See help for usage.\n");
if((opt_simplecostmodel || opt_nocostmodel) && !opt_create_instrumented_model)
log_cmd_error("Options `-simple-cost-model` and `-no-cost-model` may only be used with `-create-instrumented-model`. See help for usage.\n");
extra_args(args, argidx, design);
if (GetSize(design->selected_modules()) == 0)
log_cmd_error("Can't operate on an empty selection!\n");
TopoSort<RTLIL::Module*, IdString::compare_ptr_by_name<RTLIL::Module>> topo_modules; //cribbed from passes/techmap/flatten.cc
auto worklist = design->selected_modules();
pool<RTLIL::IdString> non_top_modules;
while (!worklist.empty()) {
RTLIL::Module *module = *(worklist.begin());
worklist.erase(worklist.begin());
topo_modules.node(module);
for (auto cell : module->selected_cells()) {
RTLIL::Module *tpl = design->module(cell->type);
if (tpl != nullptr) {
if (topo_modules.database.count(tpl) == 0)
worklist.push_back(tpl);
topo_modules.edge(tpl, module);
non_top_modules.insert(cell->type);
}
}
}
if (!topo_modules.sort())
log_cmd_error("Cannot handle recursive module instantiations.\n");
for (auto i = 0; i < GetSize(topo_modules.sorted); ++i) {
RTLIL::Module *module = topo_modules.sorted[i];
GliftWorker(module, !non_top_modules[module->name], opt_create_precise_model, opt_create_imprecise_model, opt_create_instrumented_model, opt_taintconstants, opt_keepoutputs, opt_simplecostmodel, opt_nocostmodel, opt_instrumentmore);
}
}
} GliftPass;
PRIVATE_NAMESPACE_END