aboutsummaryrefslogtreecommitdiffstats
path: root/examples/smtbmc/glift/ttt2.v
diff options
context:
space:
mode:
Diffstat (limited to 'examples/smtbmc/glift/ttt2.v')
-rwxr-xr-xexamples/smtbmc/glift/ttt2.v220
1 files changed, 220 insertions, 0 deletions
diff --git a/examples/smtbmc/glift/ttt2.v b/examples/smtbmc/glift/ttt2.v
new file mode 100755
index 000000000..47ca7684a
--- /dev/null
+++ b/examples/smtbmc/glift/ttt2.v
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-01 10:55:45 +0000