mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-26 10:38:47 +00:00
Code Activity

Remove trailing whitespaces

Browse source
This commit is contained in:
Miodrag Milanovic 2026-06-23 07:24:59 +02:00
parent 48a3dcc02a
commit a689342207
317 changed files with 3136 additions and 3136 deletions
Download patch file Download diff file Expand all files Collapse all files

6
examples/intel/asicworld_lfsr/lfsr_updown.v
View file

@ -10,7 +10,7 @@ overflow // Overflow output
input clk;
input reset;
input enable;
input enable;
input up_down;
output [7 : 0] count;
@ -18,11 +18,11 @@ overflow // Overflow output
reg [7 : 0] count;
assign overflow = (up_down) ? (count == {{7{1'b0}}, 1'b1}) :
assign overflow = (up_down) ? (count == {{7{1'b0}}, 1'b1}) :
(count == {1'b1, {7{1'b0}}}) ;
always @(posedge clk)
if (reset)
if (reset)
count <= {7{1'b0}};
else if (enable) begin
if (up_down) begin

2
examples/intel/asicworld_lfsr/lfsr_updown_tb.v
View file

@ -31,4 +31,4 @@ lfsr_updown U(
.overflow ( overflow )
);
endmodule
endmodule

838
examples/smtbmc/glift/C7552.v
View file

@ -1,428 +1,428 @@
module C7552_lev2(pi000, pi001, pi002, pi003, pi004, pi005, pi006, pi007, pi008, pi009,
pi010, pi011, pi012, pi013, pi014, pi015, pi016, pi017, pi018, pi019,
pi020, pi021, pi022, pi023, pi024, pi025, pi026, pi027, pi028, pi029,
pi030, pi031, pi032, pi033, pi034, pi035, pi036, pi037, pi038, pi039,
pi040, pi041, pi042, pi043, pi044, pi045, pi046, pi047, pi048, pi049,
pi050, pi051, pi052, pi053, pi054, pi055, pi056, pi057, pi058, pi059,
pi060, pi061, pi062, pi063, pi064, pi065, pi066, pi067, pi068, pi069,
pi070, pi071, pi072, pi073, pi074, pi075, pi076, pi077, pi078, pi079,
pi080, pi081, pi082, pi083, pi084, pi085, pi086, pi087, pi088, pi089,
pi090, pi091, pi092, pi093, pi094, pi095, pi096, pi097, pi098, pi099,
pi100, pi101, pi102, pi103, pi104, pi105, pi106, pi107, pi108, pi109,
pi110, pi111, pi112, pi113, pi114, pi115, pi116, pi117, pi118, pi119,
pi120, pi121, pi122, pi123, pi124, pi125, pi126, pi127, pi128, pi129,
pi130, pi131, pi132, pi133, pi134, pi135, pi136, pi137, pi138, pi139,
pi140, pi141, pi142, pi143, pi144, pi145, pi146, pi147, pi148, pi149,
pi150, pi151, pi152, pi153, pi154, pi155, pi156, pi157, pi158, pi159,
pi160, pi161, pi162, pi163, pi164, pi165, pi166, pi167, pi168, pi169,
pi170, pi171, pi172, pi173, pi174, pi175, pi176, pi177, pi178, pi179,
pi180, pi181, pi182, pi183, pi184, pi185, pi186, pi187, pi188, pi189,
pi190, pi191, pi192, pi193, pi194, pi195, pi196, pi197, pi198, pi199,
pi200, pi201, pi202, pi203, pi204, pi205, pi206, po000, po001, po002,
po003, po004, po005, po006, po007, po008, po009, po010, po011, po012,
po013, po014, po015, po016, po017, po018, po019, po020, po021, po022,
po023, po024, po025, po026, po027, po028, po029, po030, po031, po032,
po033, po034, po035, po036, po037, po038, po039, po040, po041, po042,
po043, po044, po045, po046, po047, po048, po049, po050, po051, po052,
po053, po054, po055, po056, po057, po058, po059, po060, po061, po062,
po063, po064, po065, po066, po067, po068, po069, po070, po071, po072,
po073, po074, po075, po076, po077, po078, po079, po080, po081, po082,
po083, po084, po085, po086, po087, po088, po089, po090, po091, po092,
po093, po094, po095, po096, po097, po098, po099, po100, po101, po102,
module C7552_lev2(pi000, pi001, pi002, pi003, pi004, pi005, pi006, pi007, pi008, pi009,
pi010, pi011, pi012, pi013, pi014, pi015, pi016, pi017, pi018, pi019,
pi020, pi021, pi022, pi023, pi024, pi025, pi026, pi027, pi028, pi029,
pi030, pi031, pi032, pi033, pi034, pi035, pi036, pi037, pi038, pi039,
pi040, pi041, pi042, pi043, pi044, pi045, pi046, pi047, pi048, pi049,
pi050, pi051, pi052, pi053, pi054, pi055, pi056, pi057, pi058, pi059,
pi060, pi061, pi062, pi063, pi064, pi065, pi066, pi067, pi068, pi069,
pi070, pi071, pi072, pi073, pi074, pi075, pi076, pi077, pi078, pi079,
pi080, pi081, pi082, pi083, pi084, pi085, pi086, pi087, pi088, pi089,
pi090, pi091, pi092, pi093, pi094, pi095, pi096, pi097, pi098, pi099,
pi100, pi101, pi102, pi103, pi104, pi105, pi106, pi107, pi108, pi109,
pi110, pi111, pi112, pi113, pi114, pi115, pi116, pi117, pi118, pi119,
pi120, pi121, pi122, pi123, pi124, pi125, pi126, pi127, pi128, pi129,
pi130, pi131, pi132, pi133, pi134, pi135, pi136, pi137, pi138, pi139,
pi140, pi141, pi142, pi143, pi144, pi145, pi146, pi147, pi148, pi149,
pi150, pi151, pi152, pi153, pi154, pi155, pi156, pi157, pi158, pi159,
pi160, pi161, pi162, pi163, pi164, pi165, pi166, pi167, pi168, pi169,
pi170, pi171, pi172, pi173, pi174, pi175, pi176, pi177, pi178, pi179,
pi180, pi181, pi182, pi183, pi184, pi185, pi186, pi187, pi188, pi189,
pi190, pi191, pi192, pi193, pi194, pi195, pi196, pi197, pi198, pi199,
pi200, pi201, pi202, pi203, pi204, pi205, pi206, po000, po001, po002,
po003, po004, po005, po006, po007, po008, po009, po010, po011, po012,
po013, po014, po015, po016, po017, po018, po019, po020, po021, po022,
po023, po024, po025, po026, po027, po028, po029, po030, po031, po032,
po033, po034, po035, po036, po037, po038, po039, po040, po041, po042,
po043, po044, po045, po046, po047, po048, po049, po050, po051, po052,
po053, po054, po055, po056, po057, po058, po059, po060, po061, po062,
po063, po064, po065, po066, po067, po068, po069, po070, po071, po072,
po073, po074, po075, po076, po077, po078, po079, po080, po081, po082,
po083, po084, po085, po086, po087, po088, po089, po090, po091, po092,
po093, po094, po095, po096, po097, po098, po099, po100, po101, po102,
po103, po104, po105, po106, po107);
input pi000, pi001, pi002, pi003, pi004, pi005, pi006, pi007, pi008, pi009,
pi010, pi011, pi012, pi013, pi014, pi015, pi016, pi017, pi018, pi019,
pi020, pi021, pi022, pi023, pi024, pi025, pi026, pi027, pi028, pi029,
pi030, pi031, pi032, pi033, pi034, pi035, pi036, pi037, pi038, pi039,
pi040, pi041, pi042, pi043, pi044, pi045, pi046, pi047, pi048, pi049,
pi050, pi051, pi052, pi053, pi054, pi055, pi056, pi057, pi058, pi059,
pi060, pi061, pi062, pi063, pi064, pi065, pi066, pi067, pi068, pi069,
pi070, pi071, pi072, pi073, pi074, pi075, pi076, pi077, pi078, pi079,
pi080, pi081, pi082, pi083, pi084, pi085, pi086, pi087, pi088, pi089,
pi090, pi091, pi092, pi093, pi094, pi095, pi096, pi097, pi098, pi099,
pi100, pi101, pi102, pi103, pi104, pi105, pi106, pi107, pi108, pi109,
pi110, pi111, pi112, pi113, pi114, pi115, pi116, pi117, pi118, pi119,
pi120, pi121, pi122, pi123, pi124, pi125, pi126, pi127, pi128, pi129,
pi130, pi131, pi132, pi133, pi134, pi135, pi136, pi137, pi138, pi139,
pi140, pi141, pi142, pi143, pi144, pi145, pi146, pi147, pi148, pi149,
pi150, pi151, pi152, pi153, pi154, pi155, pi156, pi157, pi158, pi159,
pi160, pi161, pi162, pi163, pi164, pi165, pi166, pi167, pi168, pi169,
pi170, pi171, pi172, pi173, pi174, pi175, pi176, pi177, pi178, pi179,
pi180, pi181, pi182, pi183, pi184, pi185, pi186, pi187, pi188, pi189,
pi190, pi191, pi192, pi193, pi194, pi195, pi196, pi197, pi198, pi199,
input pi000, pi001, pi002, pi003, pi004, pi005, pi006, pi007, pi008, pi009,
pi010, pi011, pi012, pi013, pi014, pi015, pi016, pi017, pi018, pi019,
pi020, pi021, pi022, pi023, pi024, pi025, pi026, pi027, pi028, pi029,
pi030, pi031, pi032, pi033, pi034, pi035, pi036, pi037, pi038, pi039,
pi040, pi041, pi042, pi043, pi044, pi045, pi046, pi047, pi048, pi049,
pi050, pi051, pi052, pi053, pi054, pi055, pi056, pi057, pi058, pi059,
pi060, pi061, pi062, pi063, pi064, pi065, pi066, pi067, pi068, pi069,
pi070, pi071, pi072, pi073, pi074, pi075, pi076, pi077, pi078, pi079,
pi080, pi081, pi082, pi083, pi084, pi085, pi086, pi087, pi088, pi089,
pi090, pi091, pi092, pi093, pi094, pi095, pi096, pi097, pi098, pi099,
pi100, pi101, pi102, pi103, pi104, pi105, pi106, pi107, pi108, pi109,
pi110, pi111, pi112, pi113, pi114, pi115, pi116, pi117, pi118, pi119,
pi120, pi121, pi122, pi123, pi124, pi125, pi126, pi127, pi128, pi129,
pi130, pi131, pi132, pi133, pi134, pi135, pi136, pi137, pi138, pi139,
pi140, pi141, pi142, pi143, pi144, pi145, pi146, pi147, pi148, pi149,
pi150, pi151, pi152, pi153, pi154, pi155, pi156, pi157, pi158, pi159,
pi160, pi161, pi162, pi163, pi164, pi165, pi166, pi167, pi168, pi169,
pi170, pi171, pi172, pi173, pi174, pi175, pi176, pi177, pi178, pi179,
pi180, pi181, pi182, pi183, pi184, pi185, pi186, pi187, pi188, pi189,
pi190, pi191, pi192, pi193, pi194, pi195, pi196, pi197, pi198, pi199,
pi200, pi201, pi202, pi203, pi204, pi205, pi206;
output po000, po001, po002, po003, po004, po005, po006, po007, po008, po009,
po010, po011, po012, po013, po014, po015, po016, po017, po018, po019,
po020, po021, po022, po023, po024, po025, po026, po027, po028, po029,
po030, po031, po032, po033, po034, po035, po036, po037, po038, po039,
po040, po041, po042, po043, po044, po045, po046, po047, po048, po049,
po050, po051, po052, po053, po054, po055, po056, po057, po058, po059,
po060, po061, po062, po063, po064, po065, po066, po067, po068, po069,
po070, po071, po072, po073, po074, po075, po076, po077, po078, po079,
po080, po081, po082, po083, po084, po085, po086, po087, po088, po089,
po090, po091, po092, po093, po094, po095, po096, po097, po098, po099,
output po000, po001, po002, po003, po004, po005, po006, po007, po008, po009,
po010, po011, po012, po013, po014, po015, po016, po017, po018, po019,
po020, po021, po022, po023, po024, po025, po026, po027, po028, po029,
po030, po031, po032, po033, po034, po035, po036, po037, po038, po039,
po040, po041, po042, po043, po044, po045, po046, po047, po048, po049,
po050, po051, po052, po053, po054, po055, po056, po057, po058, po059,
po060, po061, po062, po063, po064, po065, po066, po067, po068, po069,
po070, po071, po072, po073, po074, po075, po076, po077, po078, po079,
po080, po081, po082, po083, po084, po085, po086, po087, po088, po089,
po090, po091, po092, po093, po094, po095, po096, po097, po098, po099,
po100, po101, po102, po103, po104, po105, po106, po107;
wire n2822, n2823, n2824, n2825, n2826, n2827, n2828, n2829, n2830, n2831,
n2832, n2833, n2834, n2835, n2836, n2837, n2838, n2839, n2840, n2841,
n2842, n2843, n2844, n2845, n2846, n2847, n2848, n2849, n2850, n2851,
n2852, n2853, n2854, n2855, n2856, n2857, n2858, n2859, n2860, n2861,
n2862, n2863, n2864, n2865, n2866, n2867, n2868, n2869, n2870, n2871,
n2872, n2873, n2874, n2875, n2876, n2877, n2878, n2879, n2880, n2881,
n2882, n2883, n2884, n2885, n2886, n2887, n2888, n2889, n2890, n2891,
n2892, n2893, n2894, n2895, n2896, n2897, n2898, n2899, n2900, n2901,
n2902, n2903, n2904, n2905, n2906, n2907, n2908, n2909, n2910, n2911,
n2912, n2913, n2914, n2915, n2916, n2917, n2918, n2919, n2920, n2921,
n2922, n2923, n2924, n2925, n2926, n2927, n2928, n2929, n2930, n2931,
n2932, n2933, n2934, n2935, n2936, n2937, n2938, n2939, n2940, n2941,
n2942, n2943, n2944, n2945, n2946, n2947, n2948, n2949, n2950, n2951,
n2952, n2953, n2954, n2955, n2956, n2957, n2958, n2959, n2960, n2961,
n2962, n2963, n2964, n2965, n2966, n2967, n2968, n2969, n2970, n2971,
n2972, n2973, n2974, n2975, n2976, n2977, n2978, n2979, n2980, n2981,
n2982, n2983, n2984, n2985, n2986, n2987, n2988, n2989, n2990, n2991,
n2992, n2993, n2994, n2995, n2996, n2997, n2998, n2999, n3000, n3001,
n3002, n3003, n3004, n3005, n3006, n3007, n3008, n3009, n3010, n3011,
n3012, n3013, n3014, n3015, n3016, n3017, n3018, n3019, n3020, n3021,
n3022, n3023, n3024, n3025, n3026, n3027, n3028, n3029, n3030, n3031,
n3032, n3033, n3034, n3035, n3036, n3037, n3038, n3039, n3040, n3041,
n3042, n3043, n3044, n3045, n3046, n3047, n3048, n3049, n3050, n3051,
n3052, n3053, n3054, n3055, n3056, n3057, n3058, n3059, n3060, n3061,
n3062, n3063, n3064, n3065, n3066, n3067, n3068, n3069, n3070, n3071,
n3072, n3073, n3074, n3075, n3076, n3077, n3078, n3079, n3080, n3081,
n3082, n3083, n3084, n3085, n3086, n3087, n3088, n3089, n3090, n3091,
n3092, n3093, n3094, n3095, n3096, n3097, n3098, n3099, n3100, n3101,
n3102, n3103, n3104, n3105, n3106, n3107, n3108, n3109, n3110, n3111,
n3112, n3113, n3114, n3115, n3116, n3117, n3118, n3119, n3120, n3121,
n3122, n3123, n3124, n3125, n3126, n3127, n3128, n3129, n3130, n3131,
n3132, n3133, n3134, n3135, n3136, n3137, n3138, n3139, n3140, n3141,
n3142, n3143, n3144, n3145, n3146, n3147, n3148, n3149, n3150, n3151,
n3152, n3153, n3154, n3155, n3156, n3157, n3158, n3159, n3160, n3161,
n3162, n3163, n3164, n3165, n3166, n3167, n3168, n3169, n3170, n3171,
n3172, n3173, n3174, n3175, n3176, n3177, n3178, n3179, n3180, n3181,
n3182, n3183, n3184, n3185, n3186, n3187, n3188, n3189, n3190, n3191,
n3192, n3193, n3194, n3195, n3196, n3197, n3198, n3199, n3200, n3201,
n3202, n3203, n3204, n3205, n3206, n3207, n3208, n3209, n3210, n3211,
n3212, n3213, n3214, n3215, n3216, n3217, n3218, n3219, n3220, n3221,
n3222, n3223, n3224, n3225, n3226, n3227, n3228, n3229, n3230, n3231,
n3232, n3233, n3234, n3235, n3236, n3237, n3238, n3239, n3240, n3241,
n3242, n3243, n3244, n3245, n3246, n3247, n3248, n3249, n3250, n3251,
n3252, n3253, n3254, n3255, n3256, n3257, n3258, n3259, n3260, n3261,
n3262, n3263, n3264, n3265, n3266, n3267, n3268, n3269, n3270, n3271,
n3272, n3273, n3274, n3275, n3276, n3277, n3278, n3279, n3280, n3281,
n3282, n3283, n3284, n3285, n3286, n3287, n3288, n3289, n3290, n3291,
n3292, n3293, n3294, n3295, n3296, n3297, n3298, n3299, n3300, n3301,
n3302, n3303, n3304, n3305, n3306, n3307, n3308, n3309, n3310, n3311,
n3312, n3313, n3314, n3315, n3316, n3317, n3318, n3319, n3320, n3321,
n3322, n3323, n3324, n3325, n3326, n3327, n3328, n3329, n3330, n3331,
n3332, n3333, n3334, n3335, n3336, n3337, n3338, n3339, n3340, n3341,
n3342, n3343, n3344, n3345, n3346, n3347, n3348, n3349, n3350, n3351,
n3352, n3353, n3354, n3355, n3356, n3357, n3358, n3359, n3360, n3361,
n3362, n3363, n3364, n3365, n3366, n3367, n3368, n3369, n3370, n3371,
n3372, n3373, n3374, n3375, n3376, n3377, n3378, n3379, n3380, n3381,
n3382, n3383, n3384, n3385, n3386, n3387, n3388, n3389, n3390, n3391,
n3392, n3393, n3394, n3395, n3396, n3397, n3398, n3399, n3400, n3401,
n3402, n3403, n3404, n3405, n3406, n3407, n3408, n3409, n3410, n3411,
n3412, n3413, n3414, n3415, n3416, n3417, n3418, n3419, n3420, n3421,
n3422, n3423, n3424, n3425, n3426, n3427, n3428, n3429, n3430, n3431,
n3432, n3433, n3434, n3435, n3436, n3437, n3438, n3439, n3440, n3441,
n3442, n3443, n3444, n3445, n3446, n3447, n3448, n3449, n3450, n3451,
n3452, n3453, n3454, n3455, n3456, n3457, n3458, n3459, n3460, n3461,
n3462, n3463, n3464, n3465, n3466, n3467, n3468, n3469, n3470, n3471,
n3472, n3473, n3474, n3475, n3476, n3477, n3478, n3479, n3480, n3481,
n3482, n3483, n3484, n3485, n3486, n3487, n3488, n3489, n3490, n3491,
n3492, n3493, n3494, n3495, n3496, n3497, n3498, n3499, n3500, n3501,
n3502, n3503, n3504, n3505, n3506, n3507, n3508, n3509, n3510, n3511,
n3512, n3513, n3514, n3515, n3516, n3517, n3518, n3519, n3520, n3521,
n3522, n3523, n3524, n3525, n3526, n3527, n3528, n3529, n3530, n3531,
n3532, n3533, n3534, n3535, n3536, n3537, n3538, n3539, n3540, n3541,
n3542, n3543, n3544, n3545, n3546, n3547, n3548, n3549, n3550, n3551,
n3552, n3553, n3554, n3555, n3556, n3557, n3558, n3559, n3560, n3561,
n3562, n3563, n3564, n3565, n3566, n3567, n3568, n3569, n3570, n3571,
n3572, n3573, n3574, n3575, n3576, n3577, n3578, n3579, n3580, n3581,
n3582, n3583, n3584, n3585, n3586, n3587, n3588, n3589, n3590, n3591,
n3592, n3593, n3594, n3595, n3596, n3597, n3598, n3599, n3600, n3601,
n3602, n3603, n3604, n3605, n3606, n3607, n3608, n3609, n3610, n3611,
n3612, n3613, n3614, n3615, n3616, n3617, n3618, n3619, n3620, n3621,
n3622, n3623, n3624, n3625, n3626, n3627, n3628, n3629, n3630, n3631,
n3632, n3633, n3634, n3635, n3636, n3637, n3638, n3639, n3640, n3641,
n3642, n3643, n3644, n3645, n3646, n3647, n3648, n3649, n3650, n3651,
n3652, n3653, n3654, n3655, n3656, n3657, n3658, n3659, n3660, n3661,
n3662, n3663, n3664, n3665, n3666, n3667, n3668, n3669, n3670, n3671,
n3672, n3673, n3674, n3675, n3676, n3677, n3678, n3679, n3680, n3681,
n3682, n3683, n3684, n3685, n3686, n3687, n3688, n3689, n3690, n3691,
n3692, n3693, n3694, n3695, n3696, n3697, n3698, n3699, n3700, n3701,
n3702, n3703, n3704, n3705, n3706, n3707, n3708, n3709, n3710, n3711,
n3712, n3713, n3714, n3715, n3716, n3717, n3718, n3719, n3720, n3721,
n3722, n3723, n3724, n3725, n3726, n3727, n3728, n3729, n3730, n3731,
n3732, n3733, n3734, n3735, n3736, n3737, n3738, n3739, n3740, n3741,
n3742, n3743, n3744, n3745, n3746, n3747, n3748, n3749, n3750, n3751,
n3752, n3753, n3754, n3755, n3756, n3757, n3758, n3759, n3760, n3761,
n3762, n3763, n3764, n3765, n3766, n3767, n3768, n3769, n3770, n3771,
n3772, n3773, n3774, n3775, n3776, n3777, n3778, n3779, n3780, n3781,
n3782, n3783, n3784, n3785, n3786, n3787, n3788, n3789, n3790, n3791,
n3792, n3793, n3794, n3795, n3796, n3797, n3798, n3799, n3800, n3801,
n3802, n3803, n3804, n3805, n3806, n3807, n3808, n3809, n3810, n3811,
n3812, n3813, n3814, n3815, n3816, n3817, n3818, n3819, n3820, n3821,
n3822, n3823, n3824, n3825, n3826, n3827, n3828, n3829, n3830, n3831,
n3832, n3833, n3834, n3835, n3836, n3837, n3838, n3839, n3840, n3841,
n3842, n3843, n3844, n3845, n3846, n3847, n3848, n3849, n3850, n3851,
n3852, n3853, n3854, n3855, n3856, n3857, n3858, n3859, n3860, n3861,
n3862, n3863, n3864, n3865, n3866, n3867, n3868, n3869, n3870, n3871,
n3872, n3873, n3874, n3875, n3876, n3877, n3878, n3879, n3880, n3881,
n3882, n3883, n3884, n3885, n3886, n3887, n3888, n3889, n3890, n3891,
n3892, n3893, n3894, n3895, n3896, n3897, n3898, n3899, n3900, n3901,
n3902, n3903, n3904, n3905, n3906, n3907, n3908, n3909, n3910, n3911,
n3912, n3913, n3914, n3915, n3916, n3917, n3918, n3919, n3920, n3921,
n3922, n3923, n3924, n3925, n3926, n3927, n3928, n3929, n3930, n3931,
n3932, n3933, n3934, n3935, n3936, n3937, n3938, n3939, n3940, n3941,
n3942, n3943, n3944, n3945, n3946, n3947, n3948, n3949, n3950, n3951,
n3952, n3953, n3954, n3955, n3956, n3957, n3958, n3959, n3960, n3961,
n3962, n3963, n3964, n3965, n3966, n3967, n3968, n3969, n3970, n3971,
n3972, n3973, n3974, n3975, n3976, n3977, n3978, n3979, n3980, n3981,
n3982, n3983, n3984, n3985, n3986, n3987, n3988, n3989, n3990, n3991,
n3992, n3993, n3994, n3995, n3996, n3997, n3998, n3999, n4000, n4001,
n4002, n4003, n4004, n4005, n4006, n4007, n4008, n4009, n4010, n4011,
n4012, n4013, n4014, n4015, n4016, n4017, n4018, n4019, n4020, n4021,
n4022, n4023, n4024, n4025, n4026, n4027, n4028, n4029, n4030, n4031,
n4032, n4033, n4034, n4035, n4036, n4037, n4038, n4039, n4040, n4041,
n4042, n4043, n4044, n4045, n4046, n4047, n4048, n4049, n4050, n4051,
n4052, n4053, n4054, n4055, n4056, n4057, n4058, n4059, n4060, n4061,
n4062, n4063, n4064, n4065, n4066, n4067, n4068, n4069, n4070, n4071,
n4072, n4073, n4074, n4075, n4076, n4077, n4078, n4079, n4080, n4081,
n4082, n4083, n4084, n4085, n4086, n4087, n4088, n4089, n4090, n4091,
n4092, n4093, n4094, n4095, n4096, n4097, n4098, n4099, n4100, n4101,
n4102, n4103, n4104, n4105, n4106, n4107, n4108, n4109, n4110, n4111,
n4112, n4113, n4114, n4115, n4116, n4117, n4118, n4119, n4120, n4121,
n4122, n4123, n4124, n4125, n4126, n4127, n4128, n4129, n4130, n4131,
n4132, n4133, n4134, n4135, n4136, n4137, n4138, n4139, n4140, n4141,
n4142, n4143, n4144, n4145, n4146, n4147, n4148, n4149, n4150, n4151,
n4152, n4153, n4154, n4155, n4156, n4157, n4158, n4159, n4160, n4161,
n4162, n4163, n4164, n4165, n4166, n4167, n4168, n4169, n4170, n4171,
n4172, n4173, n4174, n4175, n4176, n4177, n4178, n4179, n4180, n4181,
n4182, n4183, n4184, n4185, n4186, n4187, n4188, n4189, n4190, n4191,
n4192, n4193, n4194, n4195, n4196, n4197, n4198, n4199, n4200, n4201,
n4202, n4203, n4204, n4205, n4206, n4207, n4208, n4209, n4210, n4211,
n4212, n4213, n4214, n4215, n4216, n4217, n4218, n4219, n4220, n4221,
n4222, n4223, n4224, n4225, n4226, n4227, n4228, n4229, n4230, n4231,
n4232, n4233, n4234, n4235, n4236, n4237, n4238, n4239, n4240, n4241,
n4242, n4243, n4244, n4245, n4246, n4247, n4248, n4249, n4250, n4251,
n4252, n4253, n4254, n4255, n4256, n4257, n4258, n4259, n4260, n4261,
n4262, n4263, n4264, n4265, n4266, n4267, n4268, n4269, n4270, n4271,
n4272, n4273, n4274, n4275, n4276, n4277, n4278, n4279, n4280, n4281,
n4282, n4283, n4284, n4285, n4286, n4287, n4288, n4289, n4290, n4291,
n4292, n4293, n4294, n4295, n4296, n4297, n4298, n4299, n4300, n4301,
n4302, n4303, n4304, n4305, n4306, n4307, n4308, n4309, n4310, n4311,
n4312, n4313, n4314, n4315, n4316, n4317, n4318, n4319, n4320, n4321,
n4322, n4323, n4324, n4325, n4326, n4327, n4328, n4329, n4330, n4331,
n4332, n4333, n4334, n4335, n4336, n4337, n4338, n4339, n4340, n4341,
n4342, n4343, n4344, n4345, n4346, n4347, n4348, n4349, n4350, n4351,
n4352, n4353, n4354, n4355, n4356, n4357, n4358, n4359, n4360, n4361,
n4362, n4363, n4364, n4365, n4366, n4367, n4368, n4369, n4370, n4371,
n4372, n4373, n4374, n4375, n4376, n4377, n4378, n4379, n4380, n4381,
n4382, n4383, n4384, n4385, n4386, n4387, n4388, n4389, n4390, n4391,
n4392, n4393, n4394, n4395, n4396, n4397, n4398, n4399, n4400, n4401,
n4402, n4403, n4404, n4405, n4406, n4407, n4408, n4409, n4410, n4411,
n4412, n4413, n4414, n4415, n4416, n4417, n4418, n4419, n4420, n4421,
n4422, n4423, n4424, n4425, n4426, n4427, n4428, n4429, n4430, n4431,
n4432, n4433, n4434, n4435, n4436, n4437, n4438, n4439, n4440, n4441,
n4442, n4443, n4444, n4445, n4446, n4447, n4448, n4449, n4450, n4451,
n4452, n4453, n4454, n4455, n4456, n4457, n4458, n4459, n4460, n4461,
n4462, n4463, n4464, n4465, n4466, n4467, n4468, n4469, n4470, n4471,
n4472, n4473, n4474, n4475, n4476, n4477, n4478, n4479, n4480, n4481,
n4482, n4483, n4484, n4485, n4486, n4487, n4488, n4489, n4490, n4491,
n4492, n4493, n4494, n4495, n4496, n4497, n4498, n4499, n4500, n4501,
n4502, n4503, n4504, n4505, n4506, n4507, n4508, n4509, n4510, n4511,
n4512, n4513, n4514, n4515, n4516, n4517, n4518, n4519, n4520, n4521,
n4522, n4523, n4524, n4525, n4526, n4527, n4528, n4529, n4530, n4531,
n4532, n4533, n4534, n4535, n4536, n4537, n4538, n4539, n4540, n4541,
n4542, n4543, n4544, n4545, n4546, n4547, n4548, n4549, n4550, n4551,
n4552, n4553, n4554, n4555, n4556, n4557, n4558, n4559, n4560, n4561,
n4562, n4563, n4564, n4565, n4566, n4567, n4568, n4569, n4570, n4571,
n4572, n4573, n4574, n4575, n4576, n4577, n4578, n4579, n4580, n4581,
n4582, n4583, n4584, n4585, n4586, n4587, n4588, n4589, n4590, n4591,
n4592, n4593, n4594, n4595, n4596, n4597, n4598, n4599, n4600, n4601,
n4602, n4603, n4604, n4605, n4606, n4607, n4608, n4609, n4610, n4611,
n4612, n4613, n4614, n4615, n4616, n4617, n4618, n4619, n4620, n4621,
n4622, n4623, n4624, n4625, n4626, n4627, n4628, n4629, n4630, n4631,
n4632, n4633, n4634, n4635, n4636, n4637, n4638, n4639, n4640, n4641,
n4642, n4643, n4644, n4645, n4646, n4647, n4648, n4649, n4650, n4651,
n4652, n4653, n4654, n4655, n4656, n4657, n4658, n4659, n4660, n4661,
n4662, n4663, n4664, n4665, n4666, n4667, n4668, n4669, n4670, n4671,
n4672, n4673, n4674, n4675, n4676, n4677, n4678, n4679, n4680, n4681,
n4682, n4683, n4684, n4685, n4686, n4687, n4688, n4689, n4690, n4691,
n4692, n4693, n4694, n4695, n4696, n4697, n4698, n4699, n4700, n4701,
n4702, n4703, n4704, n4705, n4706, n4707, n4708, n4709, n4710, n4711,
n4712, n4713, n4714, n4715, n4716, n4717, n4718, n4719, n4720, n4721,
n4722, n4723, n4724, n4725, n4726, n4727, n4728, n4729, n4730, n4731,
n4732, n4733, n4734, n4735, n4736, n4737, n4738, n4739, n4740, n4741,
n4742, n4743, n4744, n4745, n4746, n4747, n4748, n4749, n4750, n4751,
n4752, n4753, n4754, n4755, n4756, n4757, n4758, n4759, n4760, n4761,
n4762, n4763, n4764, n4765, n4766, n4767, n4768, n4769, n4770, n4771,
n4772, n4773, n4774, n4775, n4776, n4777, n4778, n4779, n4780, n4781,
n4782, n4783, n4784, n4785, n4786, n4787, n4788, n4789, n4790, n4791,
n4792, n4793, n4794, n4795, n4796, n4797, n4798, n4799, n4800, n4801,
n4802, n4803, n4804, n4805, n4806, n4807, n4808, n4809, n4810, n4811,
n4812, n4813, n4814, n4815, n4816, n4817, n4818, n4819, n4820, n4821,
n4822, n4823, n4824, n4825, n4826, n4827, n4828, n4829, n4830, n4831,
n4832, n4833, n4834, n4835, n4836, n4837, n4838, n4839, n4840, n4841,
n4842, n4843, n4844, n4845, n4846, n4847, n4848, n4849, n4850, n4851,
n4852, n4853, n4854, n4855, n4856, n4857, n4858, n4859, n4860, n4861,
n4862, n4863, n4864, n4865, n4866, n4867, n4868, n4869, n4870, n4871,
n4872, n4873, n4874, n4875, n4876, n4877, n4878, n4879, n4880, n4881,
n4882, n4883, n4884, n4885, n4886, n4887, n4888, n4889, n4890, n4891,
n4892, n4893, n4894, n4895, n4896, n4897, n4898, n4899, n4900, n4901,
n4902, n4903, n4904, n4905, n4906, n4907, n4908, n4909, n4910, n4911,
n4912, n4913, n4914, n4915, n4916, n4917, n4918, n4919, n4920, n4921,
n4922, n4923, n4924, n4925, n4926, n4927, n4928, n4929, n4930, n4931,
n4932, n4933, n4934, n4935, n4936, n4937, n4938, n4939, n4940, n4941,
n4942, n4943, n4944, n4945, n4946, n4947, n4948, n4949, n4950, n4951,
n4952, n4953, n4954, n4955, n4956, n4957, n4958, n4959, n4960, n4961,
n4962, n4963, n4964, n4965, n4966, n4967, n4968, n4969, n4970, n4971,
n4972, n4973, n4974, n4975, n4976, n4977, n4978, n4979, n4980, n4981,
n4982, n4983, n4984, n4985, n4986, n4987, n4988, n4989, n4990, n4991,
n4992, n4993, n4994, n4995, n4996, n4997, n4998, n4999, n5000, n5001,
n5002, n5003, n5004, n5005, n5006, n5007, n5008, n5009, n5010, n5011,
n5012, n5013, n5014, n5015, n5016, n5017, n5018, n5019, n5020, n5021,
n5022, n5023, n5024, n5025, n5026, n5027, n5028, n5029, n5030, n5031,
n5032, n5033, n5034, n5035, n5036, n5037, n5038, n5039, n5040, n5041,
n5042, n5043, n5044, n5045, n5046, n5047, n5048, n5049, n5050, n5051,
n5052, n5053, n5054, n5055, n5056, n5057, n5058, n5059, n5060, n5061,
n5062, n5063, n5064, n5065, n5066, n5067, n5068, n5069, n5070, n5071,
n5072, n5073, n5074, n5075, n5076, n5077, n5078, n5079, n5080, n5081,
n5082, n5083, n5084, n5085, n5086, n5087, n5088, n5089, n5090, n5091,
n5092, n5093, n5094, n5095, n5096, n5097, n5098, n5099, n5100, n5101,
n5102, n5103, n5104, n5105, n5106, n5107, n5108, n5109, n5110, n5111,
n5112, n5113, n5114, n5115, n5116, n5117, n5118, n5119, n5120, n5121,
n5122, n5123, n5124, n5125, n5126, n5127, n5128, n5129, n5130, n5131,
n5132, n5133, n5134, n5135, n5136, n5137, n5138, n5139, n5140, n5141,
n5142, n5143, n5144, n5145, n5146, n5147, n5148, n5149, n5150, n5151,
n5152, n5153, n5154, n5155, n5156, n5157, n5158, n5159, n5160, n5161,
n5162, n5163, n5164, n5165, n5166, n5167, n5168, n5169, n5170, n5171,
n5172, n5173, n5174, n5175, n5176, n5177, n5178, n5179, n5180, n5181,
n5182, n5183, n5184, n5185, n5186, n5187, n5188, n5189, n5190, n5191,
n5192, n5193, n5194, n5195, n5196, n5197, n5198, n5199, n5200, n5201,
n5202, n5203, n5204, n5205, n5206, n5207, n5208, n5209, n5210, n5211,
n5212, n5213, n5214, n5215, n5216, n5217, n5218, n5219, n5220, n5221,
n5222, n5223, n5224, n5225, n5226, n5227, n5228, n5229, n5230, n5231,
n5232, n5233, n5234, n5235, n5236, n5237, n5238, n5239, n5240, n5241,
n5242, n5243, n5244, n5245, n5246, n5247, n5248, n5249, n5250, n5251,
n5252, n5253, n5254, n5255, n5256, n5257, n5258, n5259, n5260, n5261,
n5262, n5263, n5264, n5265, n5266, n5267, n5268, n5269, n5270, n5271,
n5272, n5273, n5274, n5275, n5276, n5277, n5278, n5279, n5280, n5281,
n5282, n5283, n5284, n5285, n5286, n5287, n5288, n5289, n5290, n5291,
n5292, n5293, n5294, n5295, n5296, n5297, n5298, n5299, n5300, n5301,
n5302, n5303, n5304, n5305, n5306, n5307, n5308, n5309, n5310, n5311,
n5312, n5313, n5314, n5315, n5316, n5317, n5318, n5319, n5320, n5321,
n5322, n5323, n5324, n5325, n5326, n5327, n5328, n5329, n5330, n5331,
n5332, n5333, n5334, n5335, n5336, n5337, n5338, n5339, n5340, n5341,
n5342, n5343, n5344, n5345, n5346, n5347, n5348, n5349, n5350, n5351,
n5352, n5353, n5354, n5355, n5356, n5357, n5358, n5359, n5360, n5361,
n5362, n5363, n5364, n5365, n5366, n5367, n5368, n5369, n5370, n5371,
n5372, n5373, n5374, n5375, n5376, n5377, n5378, n5379, n5380, n5381,
n5382, n5383, n5384, n5385, n5386, n5387, n5388, n5389, n5390, n5391,
n5392, n5393, n5394, n5395, n5396, n5397, n5398, n5399, n5400, n5401,
n5402, n5403, n5404, n5405, n5406, n5407, n5408, n5409, n5410, n5411,
n5412, n5413, n5414, n5415, n5416, n5417, n5418, n5419, n5420, n5421,
n5422, n5423, n5424, n5425, n5426, n5427, n5428, n5429, n5430, n5431,
n5432, n5433, n5434, n5435, n5436, n5437, n5438, n5439, n5440, n5441,
n5442, n5443, n5444, n5445, n5446, n5447, n5448, n5449, n5450, n5451,
n5452, n5453, n5454, n5455, n5456, n5457, n5458, n5459, n5460, n5461,
n5462, n5463, n5464, n5465, n5466, n5467, n5468, n5469, n5470, n5471,
n5472, n5473, n5474, n5475, n5476, n5477, n5478, n5479, n5480, n5481,
n5482, n5483, n5484, n5485, n5486, n5487, n5488, n5489, n5490, n5491,
n5492, n5493, n5494, n5495, n5496, n5497, n5498, n5499, n5500, n5501,
n5502, n5503, n5504, n5505, n5506, n5507, n5508, n5509, n5510, n5511,
n5512, n5513, n5514, n5515, n5516, n5517, n5518, n5519, n5520, n5521,
n5522, n5523, n5524, n5525, n5526, n5527, n5528, n5529, n5530, n5531,
n5532, n5533, n5534, n5535, n5536, n5537, n5538, n5539, n5540, n5541,
n5542, n5543, n5544, n5545, n5546, n5547, n5548, n5549, n5550, n5551,
n5552, n5553, n5554, n5555, n5556, n5557, n5558, n5559, n5560, n5561,
n5562, n5563, n5564, n5565, n5566, n5567, n5568, n5569, n5570, n5571,
n5572, n5573, n5574, n5575, n5576, n5577, n5578, n5579, n5580, n5581,
n5582, n5583, n5584, n5585, n5586, n5587, n5588, n5589, n5590, n5591,
n5592, n5593, n5594, n5595, n5596, n5597, n5598, n5599, n5600, n5601,
n5602, n5603, n5604, n5605, n5606, n5607, n5608, n5609, n5610, n5611,
n5612, n5613, n5614, n5615, n5616, n5617, n5618, n5619, n5620, n5621,
n5622, n5623, n5624, n5625, n5626, n5627, n5628, n5629, n5630, n5631,
n5632, n5633, n5634, n5635, n5636, n5637, n5638, n5639, n5640, n5641,
n5642, n5643, n5644, n5645, n5646, n5647, n5648, n5649, n5650, n5651,
n5652, n5653, n5654, n5655, n5656, n5657, n5658, n5659, n5660, n5661,
n5662, n5663, n5664, n5665, n5666, n5667, n5668, n5669, n5670, n5671,
n5672, n5673, n5674, n5675, n5676, n5677, n5678, n5679, n5680, n5681,
n5682, n5683, n5684, n5685, n5686, n5687, n5688, n5689, n5690, n5691,
n5692, n5693, n5694, n5695, n5696, n5697, n5698, n5699, n5700, n5701,
n5702, n5703, n5704, n5705, n5706, n5707, n5708, n5709, n5710, n5711,
n5712, n5713, n5714, n5715, n5716, n5717, n5718, n5719, n5720, n5721,
n5722, n5723, n5724, n5725, n5726, n5727, n5728, n5729, n5730, n5731,
n5732, n5733, n5734, n5735, n5736, n5737, n5738, n5739, n5740, n5741,
n5742, n5743, n5744, n5745, n5746, n5747, n5748, n5749, n5750, n5751,
n5752, n5753, n5754, n5755, n5756, n5757, n5758, n5759, n5760, n5761,
n5762, n5763, n5764, n5765, n5766, n5767, n5768, n5769, n5770, n5771,
n5772, n5773, n5774, n5775, n5776, n5777, n5778, n5779, n5780, n5781,
n5782, n5783, n5784, n5785, n5786, n5787, n5788, n5789, n5790, n5791,
n5792, n5793, n5794, n5795, n5796, n5797, n5798, n5799, n5800, n5801,
n5802, n5803, n5804, n5805, n5806, n5807, n5808, n5809, n5810, n5811,
n5812, n5813, n5814, n5815, n5816, n5817, n5818, n5819, n5820, n5821,
n5822, n5823, n5824, n5825, n5826, n5827, n5828, n5829, n5830, n5831,
n5832, n5833, n5834, n5835, n5836, n5837, n5838, n5839, n5840, n5841,
n5842, n5843, n5844, n5845, n5846, n5847, n5848, n5849, n5850, n5851,
n5852, n5853, n5854, n5855, n5856, n5857, n5858, n5859, n5860, n5861,
n5862, n5863, n5864, n5865, n5866, n5867, n5868, n5869, n5870, n5871,
n5872, n5873, n5874, n5875, n5876, n5877, n5878, n5879, n5880, n5881,
n5882, n5883, n5884, n5885, n5886, n5887, n5888, n5889, n5890, n5891,
n5892, n5893, n5894, n5895, n5896, n5897, n5898, n5899, n5900, n5901,
n5902, n5903, n5904, n5905, n5906, n5907, n5908, n5909, n5910, n5911,
n5912, n5913, n5914, n5915, n5916, n5917, n5918, n5919, n5920, n5921,
n5922, n5923, n5924, n5925, n5926, n5927, n5928, n5929, n5930, n5931,
n5932, n5933, n5934, n5935, n5936, n5937, n5938, n5939, n5940, n5941,
n5942, n5943, n5944, n5945, n5946, n5947, n5948, n5949, n5950, n5951,
n5952, n5953, n5954, n5955, n5956, n5957, n5958, n5959, n5960, n5961,
n5962, n5963, n5964, n5965, n5966, n5967, n5968, n5969, n5970, n5971,
n5972, n5973, n5974, n5975, n5976, n5977, n5978, n5979, n5980, n5981,
n5982, n5983, n5984, n5985, n5986, n5987, n5988, n5989, n5990, n5991,
n5992, n5993, n5994, n5995, n5996, n5997, n5998, n5999, n6000, n6001,
n6002, n6003, n6004, n6005, n6006, n6007, n6008, n6009, n6010, n6011,
n6012, n6013, n6014, n6015, n6016, n6017, n6018, n6019, n6020, n6021,
n6022, n6023, n6024, n6025, n6026, n6027, n6028, n6029, n6030, n6031,
n6032, n6033, n6034, n6035, n6036, n6037, n6038, n6039, n6040, n6041,
n6042, n6043, n6044, n6045, n6046, n6047, n6048, n6049, n6050, n6051,
n6052, n6053, n6054, n6055, n6056, n6057, n6058, n6059, n6060, n6061,
n6062, n6063, n6064, n6065, n6066, n6067, n6068, n6069, n6070, n6071,
n6072, n6073, n6074, n6075, n6076, n6077, n6078, n6079, n6080, n6081,
n6082, n6083, n6084, n6085, n6086, n6087, n6088, n6089, n6090, n6091,
n6092, n6093, n6094, n6095, n6096, n6097, n6098, n6099, n6100, n6101,
n6102, n6103, n6104, n6105, n6106, n6107, n6108, n6109, n6110, n6111,
n6112, n6113, n6114, n6115, n6116, n6117, n6118, n6119, n6120, n6121,
n6122, n6123, n6124, n6125, n6126, n6127, n6128, n6129, n6130, n6131,
n6132, n6133, n6134, n6135, n6136, n6137, n6138, n6139, n6140, n6141,
n6142, n6143, n6144, n6145, n6146, n6147, n6148, n6149, n6150, n6151,
n6152, n6153, n6154, n6155, n6156, n6157, n6158, n6159, n6160, n6161,
n6162, n6163, n6164, n6165, n6166, n6167, n6168, n6169, n6170, n6171,
n6172, n6173, n6174, n6175, n6176, n6177, n6178, n6179, n6180, n6181,
n6182, n6183, n6184, n6185, n6186, n6187, n6188, n6189, n6190, n6191,
n6192, n6193, n6194, n6195, n6196, n6197, n6198, n6199, n6200, n6201,
n6202, n6203, n6204, n6205, n6206, n6207, n6208, n6209, n6210, n6211,
n6212, n6213, n6214, n6215, n6216, n6217, n6218, n6219, n6220, n6221,
n6222, n6223, n6224, n6225, n6226, n6227, n6228, n6229, n6230, n6231,
n6232, n6233, n6234, n6235, n6236, n6237, n6238, n6239, n6240, n6241,
n6242, n6243, n6244, n6245, n6246, n6247, n6248, n6249, n6250, n6251,
n6252, n6253, n6254, n6255, n6256, n6257, n6258, n6259, n6260, n6261,
n6262, n6263, n6264, n6265, n6266, n6267, n6268, n6269, n6270, n6271,
n6272, n6273, n6274, n6275, n6276, n6277, n6278, n6279, n6280, n6281,
n6282, n6283, n6284, n6285, n6286, n6287, n6288, n6289, n6290, n6291,
n6292, n6293, n6294, n6295, n6296, n6297, n6298, n6299, n6300, n6301,
n6302, n6303, n6304, n6305, n6306, n6307, n6308, n6309, n6310, n6311,
n6312, n6313, n6314, n6315, n6316, n6317, n6318, n6319, n6320, n6321,
n6322, n6323, n6324, n6325, n6326, n6327, n6328, n6329, n6330, n6331,
n6332, n6333, n6334, n6335, n6336, n6337, n6338, n6339, n6340, n6341,
n6342, n6343, n6344, n6345, n6346, n6347, n6348, n6349, n6350, n6351,
n6352, n6353, n6354, n6355, n6356, n6357, n6358, n6359, n6360, n6361,
n6362, n6363, n6364, n6365, n6366, n6367, n6368, n6369, n6370, n6371,
n6372, n6373, n6374, n6375, n6376, n6377, n6378, n6379, n6380, n6381,
n6382, n6383, n6384, n6385, n6386, n6387, n6388, n6389, n6390, n6391,
n6392, n6393, n6394, n6395, n6396, n6397, n6398, n6399, n6400, n6401,
wire n2822, n2823, n2824, n2825, n2826, n2827, n2828, n2829, n2830, n2831,
n2832, n2833, n2834, n2835, n2836, n2837, n2838, n2839, n2840, n2841,
n2842, n2843, n2844, n2845, n2846, n2847, n2848, n2849, n2850, n2851,
n2852, n2853, n2854, n2855, n2856, n2857, n2858, n2859, n2860, n2861,
n2862, n2863, n2864, n2865, n2866, n2867, n2868, n2869, n2870, n2871,
n2872, n2873, n2874, n2875, n2876, n2877, n2878, n2879, n2880, n2881,
n2882, n2883, n2884, n2885, n2886, n2887, n2888, n2889, n2890, n2891,
n2892, n2893, n2894, n2895, n2896, n2897, n2898, n2899, n2900, n2901,
n2902, n2903, n2904, n2905, n2906, n2907, n2908, n2909, n2910, n2911,
n2912, n2913, n2914, n2915, n2916, n2917, n2918, n2919, n2920, n2921,
n2922, n2923, n2924, n2925, n2926, n2927, n2928, n2929, n2930, n2931,
n2932, n2933, n2934, n2935, n2936, n2937, n2938, n2939, n2940, n2941,
n2942, n2943, n2944, n2945, n2946, n2947, n2948, n2949, n2950, n2951,
n2952, n2953, n2954, n2955, n2956, n2957, n2958, n2959, n2960, n2961,
n2962, n2963, n2964, n2965, n2966, n2967, n2968, n2969, n2970, n2971,
n2972, n2973, n2974, n2975, n2976, n2977, n2978, n2979, n2980, n2981,
n2982, n2983, n2984, n2985, n2986, n2987, n2988, n2989, n2990, n2991,
n2992, n2993, n2994, n2995, n2996, n2997, n2998, n2999, n3000, n3001,
n3002, n3003, n3004, n3005, n3006, n3007, n3008, n3009, n3010, n3011,
n3012, n3013, n3014, n3015, n3016, n3017, n3018, n3019, n3020, n3021,
n3022, n3023, n3024, n3025, n3026, n3027, n3028, n3029, n3030, n3031,
n3032, n3033, n3034, n3035, n3036, n3037, n3038, n3039, n3040, n3041,
n3042, n3043, n3044, n3045, n3046, n3047, n3048, n3049, n3050, n3051,
n3052, n3053, n3054, n3055, n3056, n3057, n3058, n3059, n3060, n3061,
n3062, n3063, n3064, n3065, n3066, n3067, n3068, n3069, n3070, n3071,
n3072, n3073, n3074, n3075, n3076, n3077, n3078, n3079, n3080, n3081,
n3082, n3083, n3084, n3085, n3086, n3087, n3088, n3089, n3090, n3091,
n3092, n3093, n3094, n3095, n3096, n3097, n3098, n3099, n3100, n3101,
n3102, n3103, n3104, n3105, n3106, n3107, n3108, n3109, n3110, n3111,
n3112, n3113, n3114, n3115, n3116, n3117, n3118, n3119, n3120, n3121,
n3122, n3123, n3124, n3125, n3126, n3127, n3128, n3129, n3130, n3131,
n3132, n3133, n3134, n3135, n3136, n3137, n3138, n3139, n3140, n3141,
n3142, n3143, n3144, n3145, n3146, n3147, n3148, n3149, n3150, n3151,
n3152, n3153, n3154, n3155, n3156, n3157, n3158, n3159, n3160, n3161,
n3162, n3163, n3164, n3165, n3166, n3167, n3168, n3169, n3170, n3171,
n3172, n3173, n3174, n3175, n3176, n3177, n3178, n3179, n3180, n3181,
n3182, n3183, n3184, n3185, n3186, n3187, n3188, n3189, n3190, n3191,
n3192, n3193, n3194, n3195, n3196, n3197, n3198, n3199, n3200, n3201,
n3202, n3203, n3204, n3205, n3206, n3207, n3208, n3209, n3210, n3211,
n3212, n3213, n3214, n3215, n3216, n3217, n3218, n3219, n3220, n3221,
n3222, n3223, n3224, n3225, n3226, n3227, n3228, n3229, n3230, n3231,
n3232, n3233, n3234, n3235, n3236, n3237, n3238, n3239, n3240, n3241,
n3242, n3243, n3244, n3245, n3246, n3247, n3248, n3249, n3250, n3251,
n3252, n3253, n3254, n3255, n3256, n3257, n3258, n3259, n3260, n3261,
n3262, n3263, n3264, n3265, n3266, n3267, n3268, n3269, n3270, n3271,
n3272, n3273, n3274, n3275, n3276, n3277, n3278, n3279, n3280, n3281,
n3282, n3283, n3284, n3285, n3286, n3287, n3288, n3289, n3290, n3291,
n3292, n3293, n3294, n3295, n3296, n3297, n3298, n3299, n3300, n3301,
n3302, n3303, n3304, n3305, n3306, n3307, n3308, n3309, n3310, n3311,
n3312, n3313, n3314, n3315, n3316, n3317, n3318, n3319, n3320, n3321,
n3322, n3323, n3324, n3325, n3326, n3327, n3328, n3329, n3330, n3331,
n3332, n3333, n3334, n3335, n3336, n3337, n3338, n3339, n3340, n3341,
n3342, n3343, n3344, n3345, n3346, n3347, n3348, n3349, n3350, n3351,
n3352, n3353, n3354, n3355, n3356, n3357, n3358, n3359, n3360, n3361,
n3362, n3363, n3364, n3365, n3366, n3367, n3368, n3369, n3370, n3371,
n3372, n3373, n3374, n3375, n3376, n3377, n3378, n3379, n3380, n3381,
n3382, n3383, n3384, n3385, n3386, n3387, n3388, n3389, n3390, n3391,
n3392, n3393, n3394, n3395, n3396, n3397, n3398, n3399, n3400, n3401,
n3402, n3403, n3404, n3405, n3406, n3407, n3408, n3409, n3410, n3411,
n3412, n3413, n3414, n3415, n3416, n3417, n3418, n3419, n3420, n3421,
n3422, n3423, n3424, n3425, n3426, n3427, n3428, n3429, n3430, n3431,
n3432, n3433, n3434, n3435, n3436, n3437, n3438, n3439, n3440, n3441,
n3442, n3443, n3444, n3445, n3446, n3447, n3448, n3449, n3450, n3451,
n3452, n3453, n3454, n3455, n3456, n3457, n3458, n3459, n3460, n3461,
n3462, n3463, n3464, n3465, n3466, n3467, n3468, n3469, n3470, n3471,
n3472, n3473, n3474, n3475, n3476, n3477, n3478, n3479, n3480, n3481,
n3482, n3483, n3484, n3485, n3486, n3487, n3488, n3489, n3490, n3491,
n3492, n3493, n3494, n3495, n3496, n3497, n3498, n3499, n3500, n3501,
n3502, n3503, n3504, n3505, n3506, n3507, n3508, n3509, n3510, n3511,
n3512, n3513, n3514, n3515, n3516, n3517, n3518, n3519, n3520, n3521,
n3522, n3523, n3524, n3525, n3526, n3527, n3528, n3529, n3530, n3531,
n3532, n3533, n3534, n3535, n3536, n3537, n3538, n3539, n3540, n3541,
n3542, n3543, n3544, n3545, n3546, n3547, n3548, n3549, n3550, n3551,
n3552, n3553, n3554, n3555, n3556, n3557, n3558, n3559, n3560, n3561,
n3562, n3563, n3564, n3565, n3566, n3567, n3568, n3569, n3570, n3571,
n3572, n3573, n3574, n3575, n3576, n3577, n3578, n3579, n3580, n3581,
n3582, n3583, n3584, n3585, n3586, n3587, n3588, n3589, n3590, n3591,
n3592, n3593, n3594, n3595, n3596, n3597, n3598, n3599, n3600, n3601,
n3602, n3603, n3604, n3605, n3606, n3607, n3608, n3609, n3610, n3611,
n3612, n3613, n3614, n3615, n3616, n3617, n3618, n3619, n3620, n3621,
n3622, n3623, n3624, n3625, n3626, n3627, n3628, n3629, n3630, n3631,
n3632, n3633, n3634, n3635, n3636, n3637, n3638, n3639, n3640, n3641,
n3642, n3643, n3644, n3645, n3646, n3647, n3648, n3649, n3650, n3651,
n3652, n3653, n3654, n3655, n3656, n3657, n3658, n3659, n3660, n3661,
n3662, n3663, n3664, n3665, n3666, n3667, n3668, n3669, n3670, n3671,
n3672, n3673, n3674, n3675, n3676, n3677, n3678, n3679, n3680, n3681,
n3682, n3683, n3684, n3685, n3686, n3687, n3688, n3689, n3690, n3691,
n3692, n3693, n3694, n3695, n3696, n3697, n3698, n3699, n3700, n3701,
n3702, n3703, n3704, n3705, n3706, n3707, n3708, n3709, n3710, n3711,
n3712, n3713, n3714, n3715, n3716, n3717, n3718, n3719, n3720, n3721,
n3722, n3723, n3724, n3725, n3726, n3727, n3728, n3729, n3730, n3731,
n3732, n3733, n3734, n3735, n3736, n3737, n3738, n3739, n3740, n3741,
n3742, n3743, n3744, n3745, n3746, n3747, n3748, n3749, n3750, n3751,
n3752, n3753, n3754, n3755, n3756, n3757, n3758, n3759, n3760, n3761,
n3762, n3763, n3764, n3765, n3766, n3767, n3768, n3769, n3770, n3771,
n3772, n3773, n3774, n3775, n3776, n3777, n3778, n3779, n3780, n3781,
n3782, n3783, n3784, n3785, n3786, n3787, n3788, n3789, n3790, n3791,
n3792, n3793, n3794, n3795, n3796, n3797, n3798, n3799, n3800, n3801,
n3802, n3803, n3804, n3805, n3806, n3807, n3808, n3809, n3810, n3811,
n3812, n3813, n3814, n3815, n3816, n3817, n3818, n3819, n3820, n3821,
n3822, n3823, n3824, n3825, n3826, n3827, n3828, n3829, n3830, n3831,
n3832, n3833, n3834, n3835, n3836, n3837, n3838, n3839, n3840, n3841,
n3842, n3843, n3844, n3845, n3846, n3847, n3848, n3849, n3850, n3851,
n3852, n3853, n3854, n3855, n3856, n3857, n3858, n3859, n3860, n3861,
n3862, n3863, n3864, n3865, n3866, n3867, n3868, n3869, n3870, n3871,
n3872, n3873, n3874, n3875, n3876, n3877, n3878, n3879, n3880, n3881,
n3882, n3883, n3884, n3885, n3886, n3887, n3888, n3889, n3890, n3891,
n3892, n3893, n3894, n3895, n3896, n3897, n3898, n3899, n3900, n3901,
n3902, n3903, n3904, n3905, n3906, n3907, n3908, n3909, n3910, n3911,
n3912, n3913, n3914, n3915, n3916, n3917, n3918, n3919, n3920, n3921,
n3922, n3923, n3924, n3925, n3926, n3927, n3928, n3929, n3930, n3931,
n3932, n3933, n3934, n3935, n3936, n3937, n3938, n3939, n3940, n3941,
n3942, n3943, n3944, n3945, n3946, n3947, n3948, n3949, n3950, n3951,
n3952, n3953, n3954, n3955, n3956, n3957, n3958, n3959, n3960, n3961,
n3962, n3963, n3964, n3965, n3966, n3967, n3968, n3969, n3970, n3971,
n3972, n3973, n3974, n3975, n3976, n3977, n3978, n3979, n3980, n3981,
n3982, n3983, n3984, n3985, n3986, n3987, n3988, n3989, n3990, n3991,
n3992, n3993, n3994, n3995, n3996, n3997, n3998, n3999, n4000, n4001,
n4002, n4003, n4004, n4005, n4006, n4007, n4008, n4009, n4010, n4011,
n4012, n4013, n4014, n4015, n4016, n4017, n4018, n4019, n4020, n4021,
n4022, n4023, n4024, n4025, n4026, n4027, n4028, n4029, n4030, n4031,
n4032, n4033, n4034, n4035, n4036, n4037, n4038, n4039, n4040, n4041,
n4042, n4043, n4044, n4045, n4046, n4047, n4048, n4049, n4050, n4051,
n4052, n4053, n4054, n4055, n4056, n4057, n4058, n4059, n4060, n4061,
n4062, n4063, n4064, n4065, n4066, n4067, n4068, n4069, n4070, n4071,
n4072, n4073, n4074, n4075, n4076, n4077, n4078, n4079, n4080, n4081,
n4082, n4083, n4084, n4085, n4086, n4087, n4088, n4089, n4090, n4091,
n4092, n4093, n4094, n4095, n4096, n4097, n4098, n4099, n4100, n4101,
n4102, n4103, n4104, n4105, n4106, n4107, n4108, n4109, n4110, n4111,
n4112, n4113, n4114, n4115, n4116, n4117, n4118, n4119, n4120, n4121,
n4122, n4123, n4124, n4125, n4126, n4127, n4128, n4129, n4130, n4131,
n4132, n4133, n4134, n4135, n4136, n4137, n4138, n4139, n4140, n4141,
n4142, n4143, n4144, n4145, n4146, n4147, n4148, n4149, n4150, n4151,
n4152, n4153, n4154, n4155, n4156, n4157, n4158, n4159, n4160, n4161,
n4162, n4163, n4164, n4165, n4166, n4167, n4168, n4169, n4170, n4171,
n4172, n4173, n4174, n4175, n4176, n4177, n4178, n4179, n4180, n4181,
n4182, n4183, n4184, n4185, n4186, n4187, n4188, n4189, n4190, n4191,
n4192, n4193, n4194, n4195, n4196, n4197, n4198, n4199, n4200, n4201,
n4202, n4203, n4204, n4205, n4206, n4207, n4208, n4209, n4210, n4211,
n4212, n4213, n4214, n4215, n4216, n4217, n4218, n4219, n4220, n4221,
n4222, n4223, n4224, n4225, n4226, n4227, n4228, n4229, n4230, n4231,
n4232, n4233, n4234, n4235, n4236, n4237, n4238, n4239, n4240, n4241,
n4242, n4243, n4244, n4245, n4246, n4247, n4248, n4249, n4250, n4251,
n4252, n4253, n4254, n4255, n4256, n4257, n4258, n4259, n4260, n4261,
n4262, n4263, n4264, n4265, n4266, n4267, n4268, n4269, n4270, n4271,
n4272, n4273, n4274, n4275, n4276, n4277, n4278, n4279, n4280, n4281,
n4282, n4283, n4284, n4285, n4286, n4287, n4288, n4289, n4290, n4291,
n4292, n4293, n4294, n4295, n4296, n4297, n4298, n4299, n4300, n4301,
n4302, n4303, n4304, n4305, n4306, n4307, n4308, n4309, n4310, n4311,
n4312, n4313, n4314, n4315, n4316, n4317, n4318, n4319, n4320, n4321,
n4322, n4323, n4324, n4325, n4326, n4327, n4328, n4329, n4330, n4331,
n4332, n4333, n4334, n4335, n4336, n4337, n4338, n4339, n4340, n4341,
n4342, n4343, n4344, n4345, n4346, n4347, n4348, n4349, n4350, n4351,
n4352, n4353, n4354, n4355, n4356, n4357, n4358, n4359, n4360, n4361,
n4362, n4363, n4364, n4365, n4366, n4367, n4368, n4369, n4370, n4371,
n4372, n4373, n4374, n4375, n4376, n4377, n4378, n4379, n4380, n4381,
n4382, n4383, n4384, n4385, n4386, n4387, n4388, n4389, n4390, n4391,
n4392, n4393, n4394, n4395, n4396, n4397, n4398, n4399, n4400, n4401,
n4402, n4403, n4404, n4405, n4406, n4407, n4408, n4409, n4410, n4411,
n4412, n4413, n4414, n4415, n4416, n4417, n4418, n4419, n4420, n4421,
n4422, n4423, n4424, n4425, n4426, n4427, n4428, n4429, n4430, n4431,
n4432, n4433, n4434, n4435, n4436, n4437, n4438, n4439, n4440, n4441,
n4442, n4443, n4444, n4445, n4446, n4447, n4448, n4449, n4450, n4451,
n4452, n4453, n4454, n4455, n4456, n4457, n4458, n4459, n4460, n4461,
n4462, n4463, n4464, n4465, n4466, n4467, n4468, n4469, n4470, n4471,
n4472, n4473, n4474, n4475, n4476, n4477, n4478, n4479, n4480, n4481,
n4482, n4483, n4484, n4485, n4486, n4487, n4488, n4489, n4490, n4491,
n4492, n4493, n4494, n4495, n4496, n4497, n4498, n4499, n4500, n4501,
n4502, n4503, n4504, n4505, n4506, n4507, n4508, n4509, n4510, n4511,
n4512, n4513, n4514, n4515, n4516, n4517, n4518, n4519, n4520, n4521,
n4522, n4523, n4524, n4525, n4526, n4527, n4528, n4529, n4530, n4531,
n4532, n4533, n4534, n4535, n4536, n4537, n4538, n4539, n4540, n4541,
n4542, n4543, n4544, n4545, n4546, n4547, n4548, n4549, n4550, n4551,
n4552, n4553, n4554, n4555, n4556, n4557, n4558, n4559, n4560, n4561,
n4562, n4563, n4564, n4565, n4566, n4567, n4568, n4569, n4570, n4571,
n4572, n4573, n4574, n4575, n4576, n4577, n4578, n4579, n4580, n4581,
n4582, n4583, n4584, n4585, n4586, n4587, n4588, n4589, n4590, n4591,
n4592, n4593, n4594, n4595, n4596, n4597, n4598, n4599, n4600, n4601,
n4602, n4603, n4604, n4605, n4606, n4607, n4608, n4609, n4610, n4611,
n4612, n4613, n4614, n4615, n4616, n4617, n4618, n4619, n4620, n4621,
n4622, n4623, n4624, n4625, n4626, n4627, n4628, n4629, n4630, n4631,
n4632, n4633, n4634, n4635, n4636, n4637, n4638, n4639, n4640, n4641,
n4642, n4643, n4644, n4645, n4646, n4647, n4648, n4649, n4650, n4651,
n4652, n4653, n4654, n4655, n4656, n4657, n4658, n4659, n4660, n4661,
n4662, n4663, n4664, n4665, n4666, n4667, n4668, n4669, n4670, n4671,
n4672, n4673, n4674, n4675, n4676, n4677, n4678, n4679, n4680, n4681,
n4682, n4683, n4684, n4685, n4686, n4687, n4688, n4689, n4690, n4691,
n4692, n4693, n4694, n4695, n4696, n4697, n4698, n4699, n4700, n4701,
n4702, n4703, n4704, n4705, n4706, n4707, n4708, n4709, n4710, n4711,
n4712, n4713, n4714, n4715, n4716, n4717, n4718, n4719, n4720, n4721,
n4722, n4723, n4724, n4725, n4726, n4727, n4728, n4729, n4730, n4731,
n4732, n4733, n4734, n4735, n4736, n4737, n4738, n4739, n4740, n4741,
n4742, n4743, n4744, n4745, n4746, n4747, n4748, n4749, n4750, n4751,
n4752, n4753, n4754, n4755, n4756, n4757, n4758, n4759, n4760, n4761,
n4762, n4763, n4764, n4765, n4766, n4767, n4768, n4769, n4770, n4771,
n4772, n4773, n4774, n4775, n4776, n4777, n4778, n4779, n4780, n4781,
n4782, n4783, n4784, n4785, n4786, n4787, n4788, n4789, n4790, n4791,
n4792, n4793, n4794, n4795, n4796, n4797, n4798, n4799, n4800, n4801,
n4802, n4803, n4804, n4805, n4806, n4807, n4808, n4809, n4810, n4811,
n4812, n4813, n4814, n4815, n4816, n4817, n4818, n4819, n4820, n4821,
n4822, n4823, n4824, n4825, n4826, n4827, n4828, n4829, n4830, n4831,
n4832, n4833, n4834, n4835, n4836, n4837, n4838, n4839, n4840, n4841,
n4842, n4843, n4844, n4845, n4846, n4847, n4848, n4849, n4850, n4851,
n4852, n4853, n4854, n4855, n4856, n4857, n4858, n4859, n4860, n4861,
n4862, n4863, n4864, n4865, n4866, n4867, n4868, n4869, n4870, n4871,
n4872, n4873, n4874, n4875, n4876, n4877, n4878, n4879, n4880, n4881,
n4882, n4883, n4884, n4885, n4886, n4887, n4888, n4889, n4890, n4891,
n4892, n4893, n4894, n4895, n4896, n4897, n4898, n4899, n4900, n4901,
n4902, n4903, n4904, n4905, n4906, n4907, n4908, n4909, n4910, n4911,
n4912, n4913, n4914, n4915, n4916, n4917, n4918, n4919, n4920, n4921,
n4922, n4923, n4924, n4925, n4926, n4927, n4928, n4929, n4930, n4931,
n4932, n4933, n4934, n4935, n4936, n4937, n4938, n4939, n4940, n4941,
n4942, n4943, n4944, n4945, n4946, n4947, n4948, n4949, n4950, n4951,
n4952, n4953, n4954, n4955, n4956, n4957, n4958, n4959, n4960, n4961,
n4962, n4963, n4964, n4965, n4966, n4967, n4968, n4969, n4970, n4971,
n4972, n4973, n4974, n4975, n4976, n4977, n4978, n4979, n4980, n4981,
n4982, n4983, n4984, n4985, n4986, n4987, n4988, n4989, n4990, n4991,
n4992, n4993, n4994, n4995, n4996, n4997, n4998, n4999, n5000, n5001,
n5002, n5003, n5004, n5005, n5006, n5007, n5008, n5009, n5010, n5011,
n5012, n5013, n5014, n5015, n5016, n5017, n5018, n5019, n5020, n5021,
n5022, n5023, n5024, n5025, n5026, n5027, n5028, n5029, n5030, n5031,
n5032, n5033, n5034, n5035, n5036, n5037, n5038, n5039, n5040, n5041,
n5042, n5043, n5044, n5045, n5046, n5047, n5048, n5049, n5050, n5051,
n5052, n5053, n5054, n5055, n5056, n5057, n5058, n5059, n5060, n5061,
n5062, n5063, n5064, n5065, n5066, n5067, n5068, n5069, n5070, n5071,
n5072, n5073, n5074, n5075, n5076, n5077, n5078, n5079, n5080, n5081,
n5082, n5083, n5084, n5085, n5086, n5087, n5088, n5089, n5090, n5091,
n5092, n5093, n5094, n5095, n5096, n5097, n5098, n5099, n5100, n5101,
n5102, n5103, n5104, n5105, n5106, n5107, n5108, n5109, n5110, n5111,
n5112, n5113, n5114, n5115, n5116, n5117, n5118, n5119, n5120, n5121,
n5122, n5123, n5124, n5125, n5126, n5127, n5128, n5129, n5130, n5131,
n5132, n5133, n5134, n5135, n5136, n5137, n5138, n5139, n5140, n5141,
n5142, n5143, n5144, n5145, n5146, n5147, n5148, n5149, n5150, n5151,
n5152, n5153, n5154, n5155, n5156, n5157, n5158, n5159, n5160, n5161,
n5162, n5163, n5164, n5165, n5166, n5167, n5168, n5169, n5170, n5171,
n5172, n5173, n5174, n5175, n5176, n5177, n5178, n5179, n5180, n5181,
n5182, n5183, n5184, n5185, n5186, n5187, n5188, n5189, n5190, n5191,
n5192, n5193, n5194, n5195, n5196, n5197, n5198, n5199, n5200, n5201,
n5202, n5203, n5204, n5205, n5206, n5207, n5208, n5209, n5210, n5211,
n5212, n5213, n5214, n5215, n5216, n5217, n5218, n5219, n5220, n5221,
n5222, n5223, n5224, n5225, n5226, n5227, n5228, n5229, n5230, n5231,
n5232, n5233, n5234, n5235, n5236, n5237, n5238, n5239, n5240, n5241,
n5242, n5243, n5244, n5245, n5246, n5247, n5248, n5249, n5250, n5251,
n5252, n5253, n5254, n5255, n5256, n5257, n5258, n5259, n5260, n5261,
n5262, n5263, n5264, n5265, n5266, n5267, n5268, n5269, n5270, n5271,
n5272, n5273, n5274, n5275, n5276, n5277, n5278, n5279, n5280, n5281,
n5282, n5283, n5284, n5285, n5286, n5287, n5288, n5289, n5290, n5291,
n5292, n5293, n5294, n5295, n5296, n5297, n5298, n5299, n5300, n5301,
n5302, n5303, n5304, n5305, n5306, n5307, n5308, n5309, n5310, n5311,
n5312, n5313, n5314, n5315, n5316, n5317, n5318, n5319, n5320, n5321,
n5322, n5323, n5324, n5325, n5326, n5327, n5328, n5329, n5330, n5331,
n5332, n5333, n5334, n5335, n5336, n5337, n5338, n5339, n5340, n5341,
n5342, n5343, n5344, n5345, n5346, n5347, n5348, n5349, n5350, n5351,
n5352, n5353, n5354, n5355, n5356, n5357, n5358, n5359, n5360, n5361,
n5362, n5363, n5364, n5365, n5366, n5367, n5368, n5369, n5370, n5371,
n5372, n5373, n5374, n5375, n5376, n5377, n5378, n5379, n5380, n5381,
n5382, n5383, n5384, n5385, n5386, n5387, n5388, n5389, n5390, n5391,
n5392, n5393, n5394, n5395, n5396, n5397, n5398, n5399, n5400, n5401,
n5402, n5403, n5404, n5405, n5406, n5407, n5408, n5409, n5410, n5411,
n5412, n5413, n5414, n5415, n5416, n5417, n5418, n5419, n5420, n5421,
n5422, n5423, n5424, n5425, n5426, n5427, n5428, n5429, n5430, n5431,
n5432, n5433, n5434, n5435, n5436, n5437, n5438, n5439, n5440, n5441,
n5442, n5443, n5444, n5445, n5446, n5447, n5448, n5449, n5450, n5451,
n5452, n5453, n5454, n5455, n5456, n5457, n5458, n5459, n5460, n5461,
n5462, n5463, n5464, n5465, n5466, n5467, n5468, n5469, n5470, n5471,
n5472, n5473, n5474, n5475, n5476, n5477, n5478, n5479, n5480, n5481,
n5482, n5483, n5484, n5485, n5486, n5487, n5488, n5489, n5490, n5491,
n5492, n5493, n5494, n5495, n5496, n5497, n5498, n5499, n5500, n5501,
n5502, n5503, n5504, n5505, n5506, n5507, n5508, n5509, n5510, n5511,
n5512, n5513, n5514, n5515, n5516, n5517, n5518, n5519, n5520, n5521,
n5522, n5523, n5524, n5525, n5526, n5527, n5528, n5529, n5530, n5531,
n5532, n5533, n5534, n5535, n5536, n5537, n5538, n5539, n5540, n5541,
n5542, n5543, n5544, n5545, n5546, n5547, n5548, n5549, n5550, n5551,
n5552, n5553, n5554, n5555, n5556, n5557, n5558, n5559, n5560, n5561,
n5562, n5563, n5564, n5565, n5566, n5567, n5568, n5569, n5570, n5571,
n5572, n5573, n5574, n5575, n5576, n5577, n5578, n5579, n5580, n5581,
n5582, n5583, n5584, n5585, n5586, n5587, n5588, n5589, n5590, n5591,
n5592, n5593, n5594, n5595, n5596, n5597, n5598, n5599, n5600, n5601,
n5602, n5603, n5604, n5605, n5606, n5607, n5608, n5609, n5610, n5611,
n5612, n5613, n5614, n5615, n5616, n5617, n5618, n5619, n5620, n5621,
n5622, n5623, n5624, n5625, n5626, n5627, n5628, n5629, n5630, n5631,
n5632, n5633, n5634, n5635, n5636, n5637, n5638, n5639, n5640, n5641,
n5642, n5643, n5644, n5645, n5646, n5647, n5648, n5649, n5650, n5651,
n5652, n5653, n5654, n5655, n5656, n5657, n5658, n5659, n5660, n5661,
n5662, n5663, n5664, n5665, n5666, n5667, n5668, n5669, n5670, n5671,
n5672, n5673, n5674, n5675, n5676, n5677, n5678, n5679, n5680, n5681,
n5682, n5683, n5684, n5685, n5686, n5687, n5688, n5689, n5690, n5691,
n5692, n5693, n5694, n5695, n5696, n5697, n5698, n5699, n5700, n5701,
n5702, n5703, n5704, n5705, n5706, n5707, n5708, n5709, n5710, n5711,
n5712, n5713, n5714, n5715, n5716, n5717, n5718, n5719, n5720, n5721,
n5722, n5723, n5724, n5725, n5726, n5727, n5728, n5729, n5730, n5731,
n5732, n5733, n5734, n5735, n5736, n5737, n5738, n5739, n5740, n5741,
n5742, n5743, n5744, n5745, n5746, n5747, n5748, n5749, n5750, n5751,
n5752, n5753, n5754, n5755, n5756, n5757, n5758, n5759, n5760, n5761,
n5762, n5763, n5764, n5765, n5766, n5767, n5768, n5769, n5770, n5771,
n5772, n5773, n5774, n5775, n5776, n5777, n5778, n5779, n5780, n5781,
n5782, n5783, n5784, n5785, n5786, n5787, n5788, n5789, n5790, n5791,
n5792, n5793, n5794, n5795, n5796, n5797, n5798, n5799, n5800, n5801,
n5802, n5803, n5804, n5805, n5806, n5807, n5808, n5809, n5810, n5811,
n5812, n5813, n5814, n5815, n5816, n5817, n5818, n5819, n5820, n5821,
n5822, n5823, n5824, n5825, n5826, n5827, n5828, n5829, n5830, n5831,
n5832, n5833, n5834, n5835, n5836, n5837, n5838, n5839, n5840, n5841,
n5842, n5843, n5844, n5845, n5846, n5847, n5848, n5849, n5850, n5851,
n5852, n5853, n5854, n5855, n5856, n5857, n5858, n5859, n5860, n5861,
n5862, n5863, n5864, n5865, n5866, n5867, n5868, n5869, n5870, n5871,
n5872, n5873, n5874, n5875, n5876, n5877, n5878, n5879, n5880, n5881,
n5882, n5883, n5884, n5885, n5886, n5887, n5888, n5889, n5890, n5891,
n5892, n5893, n5894, n5895, n5896, n5897, n5898, n5899, n5900, n5901,
n5902, n5903, n5904, n5905, n5906, n5907, n5908, n5909, n5910, n5911,
n5912, n5913, n5914, n5915, n5916, n5917, n5918, n5919, n5920, n5921,
n5922, n5923, n5924, n5925, n5926, n5927, n5928, n5929, n5930, n5931,
n5932, n5933, n5934, n5935, n5936, n5937, n5938, n5939, n5940, n5941,
n5942, n5943, n5944, n5945, n5946, n5947, n5948, n5949, n5950, n5951,
n5952, n5953, n5954, n5955, n5956, n5957, n5958, n5959, n5960, n5961,
n5962, n5963, n5964, n5965, n5966, n5967, n5968, n5969, n5970, n5971,
n5972, n5973, n5974, n5975, n5976, n5977, n5978, n5979, n5980, n5981,
n5982, n5983, n5984, n5985, n5986, n5987, n5988, n5989, n5990, n5991,
n5992, n5993, n5994, n5995, n5996, n5997, n5998, n5999, n6000, n6001,
n6002, n6003, n6004, n6005, n6006, n6007, n6008, n6009, n6010, n6011,
n6012, n6013, n6014, n6015, n6016, n6017, n6018, n6019, n6020, n6021,
n6022, n6023, n6024, n6025, n6026, n6027, n6028, n6029, n6030, n6031,
n6032, n6033, n6034, n6035, n6036, n6037, n6038, n6039, n6040, n6041,
n6042, n6043, n6044, n6045, n6046, n6047, n6048, n6049, n6050, n6051,
n6052, n6053, n6054, n6055, n6056, n6057, n6058, n6059, n6060, n6061,
n6062, n6063, n6064, n6065, n6066, n6067, n6068, n6069, n6070, n6071,
n6072, n6073, n6074, n6075, n6076, n6077, n6078, n6079, n6080, n6081,
n6082, n6083, n6084, n6085, n6086, n6087, n6088, n6089, n6090, n6091,
n6092, n6093, n6094, n6095, n6096, n6097, n6098, n6099, n6100, n6101,
n6102, n6103, n6104, n6105, n6106, n6107, n6108, n6109, n6110, n6111,
n6112, n6113, n6114, n6115, n6116, n6117, n6118, n6119, n6120, n6121,
n6122, n6123, n6124, n6125, n6126, n6127, n6128, n6129, n6130, n6131,
n6132, n6133, n6134, n6135, n6136, n6137, n6138, n6139, n6140, n6141,
n6142, n6143, n6144, n6145, n6146, n6147, n6148, n6149, n6150, n6151,
n6152, n6153, n6154, n6155, n6156, n6157, n6158, n6159, n6160, n6161,
n6162, n6163, n6164, n6165, n6166, n6167, n6168, n6169, n6170, n6171,
n6172, n6173, n6174, n6175, n6176, n6177, n6178, n6179, n6180, n6181,
n6182, n6183, n6184, n6185, n6186, n6187, n6188, n6189, n6190, n6191,
n6192, n6193, n6194, n6195, n6196, n6197, n6198, n6199, n6200, n6201,
n6202, n6203, n6204, n6205, n6206, n6207, n6208, n6209, n6210, n6211,
n6212, n6213, n6214, n6215, n6216, n6217, n6218, n6219, n6220, n6221,
n6222, n6223, n6224, n6225, n6226, n6227, n6228, n6229, n6230, n6231,
n6232, n6233, n6234, n6235, n6236, n6237, n6238, n6239, n6240, n6241,
n6242, n6243, n6244, n6245, n6246, n6247, n6248, n6249, n6250, n6251,
n6252, n6253, n6254, n6255, n6256, n6257, n6258, n6259, n6260, n6261,
n6262, n6263, n6264, n6265, n6266, n6267, n6268, n6269, n6270, n6271,
n6272, n6273, n6274, n6275, n6276, n6277, n6278, n6279, n6280, n6281,
n6282, n6283, n6284, n6285, n6286, n6287, n6288, n6289, n6290, n6291,
n6292, n6293, n6294, n6295, n6296, n6297, n6298, n6299, n6300, n6301,
n6302, n6303, n6304, n6305, n6306, n6307, n6308, n6309, n6310, n6311,
n6312, n6313, n6314, n6315, n6316, n6317, n6318, n6319, n6320, n6321,
n6322, n6323, n6324, n6325, n6326, n6327, n6328, n6329, n6330, n6331,
n6332, n6333, n6334, n6335, n6336, n6337, n6338, n6339, n6340, n6341,
n6342, n6343, n6344, n6345, n6346, n6347, n6348, n6349, n6350, n6351,
n6352, n6353, n6354, n6355, n6356, n6357, n6358, n6359, n6360, n6361,
n6362, n6363, n6364, n6365, n6366, n6367, n6368, n6369, n6370, n6371,
n6372, n6373, n6374, n6375, n6376, n6377, n6378, n6379, n6380, n6381,
n6382, n6383, n6384, n6385, n6386, n6387, n6388, n6389, n6390, n6391,
n6392, n6393, n6394, n6395, n6396, n6397, n6398, n6399, n6400, n6401,
n6402, n6403, n6404, n6405;
assign po001 = pi187;

2
examples/smtbmc/glift/C7552.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell

98
examples/smtbmc/glift/C880.v
View file

@ -1,58 +1,58 @@
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,
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,
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,
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,
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;

2
examples/smtbmc/glift/C880.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell

66
examples/smtbmc/glift/alu2.v
View file

@ -1,42 +1,42 @@
module alu2_lev2(pi0, pi1, pi2, pi3, pi4, pi5, pi6, pi7, pi8, pi9,
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,
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));

2
examples/smtbmc/glift/alu2.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell

142
examples/smtbmc/glift/alu4.v
View file

@ -1,80 +1,80 @@
module alu4_lev2(pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09,
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,
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,
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));

2
examples/smtbmc/glift/alu4.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell

12
examples/smtbmc/glift/t481.v
View file

@ -1,15 +1,15 @@
module t481_lev2(pi00, pi01, pi02, pi03, pi04, pi05, pi06, pi07, pi08, pi09,
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,
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,
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));

2
examples/smtbmc/glift/t481.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell

68
examples/smtbmc/glift/too_large.v
View file

@ -1,43 +1,43 @@
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,
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,
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,
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));

2
examples/smtbmc/glift/too_large.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell

44
examples/smtbmc/glift/ttt2.v
View file

@ -1,31 +1,31 @@
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,
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,
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,
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,
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));

2
examples/smtbmc/glift/ttt2.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell

86
examples/smtbmc/glift/x1.v
View file

@ -1,52 +1,52 @@
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,
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,
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,
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,
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;

2
examples/smtbmc/glift/x1.ys
View file

@ -36,6 +36,6 @@ opt solved
miter -equiv spec solved satmiter
flatten
sat -prove trigger 0 satmiter
delete satmiter
delete satmiter
stat
shell