# CrackMeEXE
ta nhận được file exe đã bị pack bằng UPX:
vào hàm main:
ta thấy chương trình gọi rất nhiều kỹ thuật anti-debug.
ta có thể patch nhảy qua check chieeuf kiện như sau:
ta có thể thấy chương trình gọi shellcode
vào hàm `v16`:
chương trình thực hiện mã hóa xor input với `'flag'` và kiểm tra với `v4`.
script solve:

v4=[0x11, 0x0F, 0x15, 0x01, 0x1D, 0x2D, 0x0F, 0x09, 0x56, 0x15, 0x52, 0x03, 0x39, 0x35, 0x52, 0x13, 0x59, 0x11]  
j=b'flag'
flag=''
for i in range(len(v4)):flag+=(chr(v4[17-i]^j[(17-i)%4]))
print(flag[::-1])

Flag: `wctf{Ann0y3d_Y3t?}`
# Lockdown
bài cho 1 file `synth.v`
<details>
<summary>synth.v</summary>

/* Generated by Yosys 0.50+107 (git sha1 6462cd216, x86_64-w64-mingw32-g++ 13.2.1 -O3) */
`include "structs.sv"

(* top =  1  *)
(* src = "add.sv:1.1-10.10" *)
module add(a, b, password, c);
  wire _000_;
  wire _001_;
  wire _002_;
  wire _003_;
  wire _004_;
  wire _005_;
  wire _006_;
  wire _007_;
  wire _008_;
  wire _009_;
  wire _010_;
  wire _011_;
  wire _012_;
  wire _013_;
  wire _014_;
  wire _015_;
  wire _016_;
  wire _017_;
  wire _018_;
  wire _019_;
  wire _020_;
  wire _021_;
  wire _022_;
  wire _023_;
  wire _024_;
  wire _025_;
  wire _026_;
  wire _027_;
  wire _028_;
  wire _029_;
  wire _030_;
  wire _031_;
  wire _032_;
  wire _033_;
  wire _034_;
  wire _035_;
  wire _036_;
  wire _037_;
  wire _038_;
  wire _039_;
  wire _040_;
  wire _041_;
  wire _042_;
  wire _043_;
  wire _044_;
  wire _045_;
  wire _046_;
  wire _047_;
  wire _048_;
  wire _049_;
  wire _050_;
  wire _051_;
  wire _052_;
  wire _053_;
  wire _054_;
  wire _055_;
  wire _056_;
  wire _057_;
  wire _058_;
  wire _059_;
  wire _060_;
  wire _061_;
  wire _062_;
  wire _063_;
  wire _064_;
  wire _065_;
  wire _066_;
  wire _067_;
  wire _068_;
  wire _069_;
  wire _070_;
  wire _071_;
  wire _072_;
  wire _073_;
  wire _074_;
  wire _075_;
  wire _076_;
  wire _077_;
  wire _078_;
  wire _079_;
  wire _080_;
  wire _081_;
  wire _082_;
  wire _083_;
  wire _084_;
  wire _085_;
  wire _086_;
  wire _087_;
  wire _088_;
  wire _089_;
  wire _090_;
  wire _091_;
  wire _092_;
  wire _093_;
  wire _094_;
  wire _095_;
  wire _096_;
  wire _097_;
  wire _098_;
  wire _099_;
  wire _100_;
  wire _101_;
  wire _102_;
  wire _103_;
  wire _104_;
  wire _105_;
  wire _106_;
  wire _107_;
  wire _108_;
  wire _109_;
  wire _110_;
  wire _111_;
  wire _112_;
  wire _113_;
  wire _114_;
  wire _115_;
  wire _116_;
  wire _117_;
  wire _118_;
  wire _119_;
  wire _120_;
  wire _121_;
  wire _122_;
  wire _123_;
  wire _124_;
  wire _125_;
  wire _126_;
  wire _127_;
  wire _128_;
  wire _129_;
  wire _130_;
  wire _131_;
  wire _132_;

  wire _l0_;
  wire _l1_;
  wire _l2_;
  wire _l3_;
  wire _l4_;
  wire _l5_;
  wire _l6_;
  wire _l7_;
  wire _l8_;
  wire _l9_;
  wire _l10_;
  wire _l11_;
  wire _l12_;
  wire _l13_;
  wire _l14_;
  wire _l15_;
  wire _l16_;
  wire _l17_;
  wire _l18_;
  wire _l19_;
  wire _l20_;
  wire _l21_;
  wire _l22_;
  wire _l23_;
  wire _l24_;
  wire _l25_;
  wire _l26_;
  wire _l27_;
  wire _l28_;
  wire _l29_;
  wire _l30_;
  wire _l31_;
  wire _l32_;
  wire _l33_;
  wire _l34_;
  wire _l35_;
  wire _l36_;
  wire _l37_;
  wire _l38_;
  wire _l39_;
  wire _l40_;
  wire _l41_;
  wire _l42_;
  wire _l43_;
  wire _l44_;
  wire _l45_;
  wire _l46_;
  wire _l47_;

  (* src = "add.sv:2.25-2.26" *)
  input [31:0] a;
  wire [31:0] a;
  (* src = "add.sv:3.25-3.26" *)
  input [31:0] b;
  wire [31:0] b;
  (* src = "add.sv:5.25-5.26" *)
  output [31:0] c;
  wire [31:0] c;
  (* src = "add.sv:4.25-4.33" *)
  input [47:0] password;
  wire [47:0] password;
  
  
NAND _133_ (
    .A(a[12]),
    .B(b[12]),
    .Y(_130_)
);

XOR _134_ (
    .A(a[12]),
    .B(b[12]),
    .Y(_131_)
);

NAND _135_ (
    .A(a[11]),
    .B(b[11]),
    .Y(_l16_)
);

NOR _136_ (
    .A(a[11]),
    .B(b[11]),
    .Y(_l20_)
);

NAND _137_ (
    .A(a[10]),
    .B(b[10]),
    .Y(_001_)
);

XOR _138_ (
    .A(a[10]),
    .B(b[10]),
    .Y(_002_)
);

NAND _139_ (
    .A(a[9]),
    .B(b[9]),
    .Y(_003_)
);

NOR _140_ (
    .A(a[9]),
    .B(b[9]),
    .Y(_l33_)
);

AND _141_ (
    .A(a[8]),
    .B(b[8]),
    .Y(_l38_)
);

XOR _142_ (
    .A(a[8]),
    .B(b[8]),
    .Y(_006_)
);

NAND _143_ (
    .A(a[7]),
    .B(b[7]),
    .Y(_007_)
);

OR _144_ (
    .A(a[7]),
    .B(b[7]),
    .Y(_008_)
);

AND _145_ (
    .A(a[6]),
    .B(b[6]),
    .Y(_l21_)
);

XOR _146_ (
    .A(a[6]),
    .B(b[6]),
    .Y(_l24_)
);

NAND _147_ (
    .A(a[5]),
    .B(b[5]),
    .Y(_011_)
);

NAND _148_ (
    .A(a[4]),
    .B(b[4]),
    .Y(_012_)
);

NAND _149_ (
    .A(a[3]),
    .B(b[3]),
    .Y(_013_)
);

NAND _150_ (
    .A(a[2]),
    .B(b[2]),
    .Y(_014_)
);

NAND _151_ (
    .A(a[1]),
    .B(b[1]),
    .Y(_015_)
);

AND _152_ (
    .A(a[0]),
    .B(b[0]),
    .Y(_016_)
);

XOR _153_ (
    .A(a[1]),
    .B(b[1]),
    .Y(_017_)
);

NAND _154_ (
    .A(_016_),
    .B(_017_),
    .Y(_018_)
);

NAND _155_ (
    .A(_015_),
    .B(_018_),
    .Y(_019_)
);

XOR _156_ (
    .A(a[2]),
    .B(b[2]),
    .Y(_020_)
);

NAND _157_ (
    .A(_019_),
    .B(_020_),
    .Y(_021_)
);

NAND _158_ (
    .A(_014_),
    .B(_021_),
    .Y(_022_)
);

XOR _159_ (
    .A(a[3]),
    .B(b[3]),
    .Y(_023_)
);

NAND _160_ (
    .A(_022_),
    .B(_023_),
    .Y(_024_)
);

NAND _161_ (
    .A(_013_),
    .B(_024_),
    .Y(_025_)
);

XNOR _162_ (
    .A(a[4]),
    .B(b[4]),
    .Y(_l0_)
);

AND _163_ (
    .A(_025_),
    .B(_026_),
    .Y(_l46_)
);

AND _164_ (
    .A(_012_),
    .B(_027_),
    .Y(_l27_)
);

XOR _165_ (
    .A(a[5]),
    .B(b[5]),
    .Y(_l5_)
);

NAND _166_ (
    .A(_028_),
    .B(_029_),
    .Y(_030_)
);

NAND _167_ (
    .A(_011_),
    .B(_030_),
    .Y(_031_)
);

NAND _168_ (
    .A(_010_),
    .B(_031_),
    .Y(_032_)
);

NAND _169_ (
    .A(_009_),
    .B(_032_),
    .Y(_033_)
);

NAND _170_ (
    .A(_008_),
    .B(_033_),
    .Y(_034_)
);

AND _171_ (
    .A(_007_),
    .B(_034_),
    .Y(_l6_)
);

NAND _172_ (
    .A(_006_),
    .B(_035_),
    .Y(_036_)
);

AND _173_ (
    .A(_005_),
    .B(_036_),
    .Y(_l42_)
);

NAND _174_ (
    .A(_004_),
    .B(_037_),
    .Y(_038_)
);

NAND _175_ (
    .A(_003_),
    .B(_038_),
    .Y(_039_)
);

NAND _176_ (
    .A(_002_),
    .B(_039_),
    .Y(_040_)
);

NAND _177_ (
    .A(_001_),
    .B(_040_),
    .Y(_041_)
);

NAND _178_ (
    .A(_000_),
    .B(_041_),
    .Y(_042_)
);

NAND _179_ (
    .A(_132_),
    .B(_042_),
    .Y(_l15_)
);

AND _180_ (
    .A(_131_),
    .B(_043_),
    .Y(_l26_)
);

AND _181_ (
    .A(_130_),
    .B(_044_),
    .Y(_045_)
);

NAND _182_ (
    .A(a[13]),
    .B(b[13]),
    .Y(_l18_)
);

OR _183_ (
    .A(a[13]),
    .B(b[13]),
    .Y(_047_)
);

XOR _184_ (
    .A(a[13]),
    .B(b[13]),
    .Y(_048_)
);

XNOR _185_ (
    .A(_045_),
    .B(_048_),
    .Y(_l22_)
);

AND _186_ (
    .A(a[14]),
    .B(b[14]),
    .Y(_l9_)
);

XOR _187_ (
    .A(a[14]),
    .B(b[14]),
    .Y(_050_)
);

NAND _188_ (
    .A(_045_),
    .B(_046_),
    .Y(_l28_)
);

AND _189_ (
    .A(_047_),
    .B(_051_),
    .Y(_052_)
);

AND _190_ (
    .A(_050_),
    .B(_052_),
    .Y(_l37_)
);

XOR _191_ (
    .A(_050_),
    .B(_052_),
    .Y(c[14])
);

AND _192_ (
    .A(_049_),
    .B(_053_),
    .Y(_054_)
);

NAND _193_ (
    .A(a[15]),
    .B(b[15]),
    .Y(_055_)
);

OR _194_ (
    .A(a[15]),
    .B(b[15]),
    .Y(_l39_)
);

XOR _195_ (
    .A(a[15]),
    .B(b[15]),
    .Y(_057_)
);

XNOR _196_ (
    .A(_054_),
    .B(_057_),
    .Y(c[15])
);

NAND _197_ (
    .A(a[16]),
    .B(b[16]),
    .Y(_l4_)
);

XNOR _198_ (
    .A(a[16]),
    .B(b[16]),
    .Y(_l35_)
);

NAND _199_ (
    .A(_054_),
    .B(_055_),
    .Y(_060_)
);

AND _200_ (
    .A(_056_),
    .B(_060_),
    .Y(_l47_)
);

NAND _201_ (
    .A(_059_),
    .B(_061_),
    .Y(_062_)
);

XOR _202_ (
    .A(_059_),
    .B(_061_),
    .Y(c[16])
);

AND _203_ (
    .A(_058_),
    .B(_062_),
    .Y(_063_)
);

NAND _204_ (
    .A(a[17]),
    .B(b[17]),
    .Y(_064_)
);

OR _205_ (
    .A(a[17]),
    .B(b[17]),
    .Y(_l36_)
);

XOR _206_ (
    .A(a[17]),
    .B(b[17]),
    .Y(_066_)
);

XNOR _207_ (
    .A(_063_),
    .B(_066_),
    .Y(c[17])
);

NAND _208_ (
    .A(a[18]),
    .B(b[18]),
    .Y(_067_)
);

XOR _209_ (
    .A(a[18]),
    .B(b[18]),
    .Y(_068_)
);

NAND _210_ (
    .A(_063_),
    .B(_064_),
    .Y(_069_)
);

AND _211_ (
    .A(_065_),
    .B(_069_),
    .Y(_070_)
);

NAND _212_ (
    .A(_068_),
    .B(_070_),
    .Y(_071_)
);

XOR _213_ (
    .A(_068_),
    .B(_070_),
    .Y(c[18])
);

AND _214_ (
    .A(_067_),
    .B(_071_),
    .Y(_072_)
);

NAND _215_ (
    .A(a[19]),
    .B(b[19]),
    .Y(_073_)
);

NOR _216_ (
    .A(a[19]),
    .B(b[19]),
    .Y(_l3_)
);

XOR _217_ (
    .A(a[19]),
    .B(b[19]),
    .Y(_075_)
);

XOR _218_ (
    .A(_072_),
    .B(_075_),
    .Y(_l45_)
);

NAND _219_ (
    .A(a[20]),
    .B(b[20]),
    .Y(_076_)
);

XOR _220_ (
    .A(a[20]),
    .B(b[20]),
    .Y(_077_)
);

NAND _221_ (
    .A(_072_),
    .B(_073_),
    .Y(_078_)
);

AND _222_ (
    .A(_074_),
    .B(_078_),
    .Y(_079_)
);

AND _223_ (
    .A(_077_),
    .B(_079_),
    .Y(_l8_)
);

XOR _224_ (
    .A(_077_),
    .B(_079_),
    .Y(c[20])
);

AND _225_ (
    .A(_076_),
    .B(_080_),
    .Y(_081_)
);

NAND _226_ (
    .A(a[21]),
    .B(b[21]),
    .Y(_l2_)
);

OR _227_ (
    .A(a[21]),
    .B(b[21]),
    .Y(_083_)
);

XOR _228_ (
    .A(a[21]),
    .B(b[21]),
    .Y(_084_)
);

XNOR _229_ (
    .A(_081_),
    .B(_084_),
    .Y(c[21])
);

NAND _230_ (
    .A(a[22]),
    .B(b[22]),
    .Y(_085_)
);

XNOR _231_ (
    .A(a[22]),
    .B(b[22]),
    .Y(_l1_)
);

NAND _232_ (
    .A(_081_),
    .B(_082_),
    .Y(_087_)
);

AND _233_ (
    .A(_083_),
    .B(_087_),
    .Y(_088_)
);

NAND _234_ (
    .A(_086_),
    .B(_088_),
    .Y(_089_)
);

XOR _235_ (
    .A(_086_),
    .B(_088_),
    .Y(c[22])
);

AND _236_ (
    .A(_085_),
    .B(_089_),
    .Y(_090_)
);

AND _237_ (
    .A(a[23]),
    .B(b[23]),
    .Y(_l13_)
);

OR _238_ (
    .A(a[23]),
    .B(b[23]),
    .Y(_092_)
);

XOR _239_ (
    .A(a[23]),
    .B(b[23]),
    .Y(_l7_)
);

XNOR _240_ (
    .A(_090_),
    .B(_093_),
    .Y(c[23])
);

NAND _241_ (
    .A(a[24]),
    .B(b[24]),
    .Y(_094_)
);

XOR _242_ (
    .A(a[24]),
    .B(b[24]),
    .Y(_095_)
);

NAND _243_ (
    .A(_090_),
    .B(_091_),
    .Y(_l19_)
);

AND _244_ (
    .A(_092_),
    .B(_096_),
    .Y(_097_)
);

NAND _245_ (
    .A(_095_),
    .B(_097_),
    .Y(_098_)
);

XOR _246_ (
    .A(_095_),
    .B(_097_),
    .Y(c[24])
);

AND _247_ (
    .A(_094_),
    .B(_098_),
    .Y(_099_)
);

AND _248_ (
    .A(a[25]),
    .B(b[25]),
    .Y(_l14_)
);

OR _249_ (
    .A(a[25]),
    .B(b[25]),
    .Y(_101_)
);

XOR _250_ (
    .A(a[25]),
    .B(b[25]),
    .Y(_102_)
);

XNOR _251_ (
    .A(_099_),
    .B(_102_),
    .Y(c[25])
);

NAND _252_ (
    .A(a[26]),
    .B(b[26]),
    .Y(_103_)
);

XOR _253_ (
    .A(a[26]),
    .B(b[26]),
    .Y(_104_)
);

NAND _254_ (
    .A(_099_),
    .B(_100_),
    .Y(_105_)
);

NAND _255_ (
    .A(_101_),
    .B(_105_),
    .Y(_l44_)
);

NAND _256_ (
    .A(_104_),
    .B(_106_),
    .Y(_107_)
);

XOR _257_ (
    .A(_104_),
    .B(_106_),
    .Y(c[26])
);

AND _258_ (
    .A(_103_),
    .B(_107_),
    .Y(_108_)
);

NAND _259_ (
    .A(a[27]),
    .B(b[27]),
    .Y(_109_)
);

OR _260_ (
    .A(a[27]),
    .B(b[27]),
    .Y(_110_)
);

XOR _261_ (
    .A(a[27]),
    .B(b[27]),
    .Y(_l10_)
);

XNOR _262_ (
    .A(_108_),
    .B(_111_),
    .Y(c[27])
);

NAND _263_ (
    .A(a[28]),
    .B(b[28]),
    .Y(_112_)
);

XOR _264_ (
    .A(a[28]),
    .B(b[28]),
    .Y(_113_)
);

NAND _265_ (
    .A(_108_),
    .B(_109_),
    .Y(_l43_)
);

NAND _266_ (
    .A(_110_),
    .B(_114_),
    .Y(_l34_)
);

NAND _267_ (
    .A(_113_),
    .B(_115_),
    .Y(_116_)
);

XOR _268_ (
    .A(_113_),
    .B(_115_),
    .Y(c[28])
);

NAND _269_ (
    .A(_112_),
    .B(_116_),
    .Y(_117_)
);

NAND _270_ (
    .A(a[29]),
    .B(b[29]),
    .Y(_118_)
);

XNOR _271_ (
    .A(a[29]),
    .B(b[29]),
    .Y(_l30_)
);

NAND _272_ (
    .A(_117_),
    .B(_119_),
    .Y(_120_)
);

XOR _273_ (
    .A(_117_),
    .B(_119_),
    .Y(c[29])
);

NAND _274_ (
    .A(_118_),
    .B(_120_),
    .Y(_121_)
);

NAND _275_ (
    .A(a[30]),
    .B(b[30]),
    .Y(_l11_)
);

XOR _276_ (
    .A(a[30]),
    .B(b[30]),
    .Y(_123_)
);

NAND _277_ (
    .A(_121_),
    .B(_123_),
    .Y(_124_)
);

XNOR _278_ (
    .A(_121_),
    .B(_123_),
    .Y(_l40_)
);

NAND _279_ (
    .A(_122_),
    .B(_124_),
    .Y(_l23_)
);

XNOR _280_ (
    .A(a[31]),
    .B(b[31]),
    .Y(_l32_)
);

XNOR _281_ (
    .A(_125_),
    .B(_126_),
    .Y(c[31])
);

XOR _282_ (
    .A(a[0]),
    .B(b[0]),
    .Y(_l12_)
);

XOR _283_ (
    .A(_016_),
    .B(_017_),
    .Y(_l29_)
);

XOR _284_ (
    .A(_019_),
    .B(_020_),
    .Y(c[2])
);

XOR _285_ (
    .A(_022_),
    .B(_023_),
    .Y(c[3])
);

XOR _286_ (
    .A(_025_),
    .B(_026_),
    .Y(c[4])
);

XOR _287_ (
    .A(_028_),
    .B(_029_),
    .Y(c[5])
);

XOR _288_ (
    .A(_010_),
    .B(_031_),
    .Y(_l17_)
);

XNOR _289_ (
    .A(a[7]),
    .B(b[7]),
    .Y(_127_)
);

XNOR _290_ (
    .A(_033_),
    .B(_127_),
    .Y(c[7])
);

XOR _291_ (
    .A(_006_),
    .B(_035_),
    .Y(_l31_)
);

XNOR _292_ (
    .A(a[9]),
    .B(b[9]),
    .Y(_128_)
);

XNOR _293_ (
    .A(_037_),
    .B(_128_),
    .Y(_l41_)
);

XOR _294_ (
    .A(_002_),
    .B(_039_),
    .Y(c[10])
);

XNOR _295_ (
    .A(a[11]),
    .B(b[11]),
    .Y(_129_)
);

XNOR _296_ (
    .A(_041_),
    .B(_129_),
    .Y(c[11])
);

XOR _297_ (
    .A(_131_),
    .B(_043_),
    .Y(_l25_)
);

XOR _lock0_ (
    .A(_l0_),
    .B(password[0]),
    .Y(_026_)
);

XOR _lock1_ (
    .A(_l1_),
    .B(password[1]),
    .Y(_086_)
);

XOR _lock2_ (
    .A(_l2_),
    .B(password[2]),
    .Y(_082_)
);

XOR _lock3_ (
    .A(_l3_),
    .B(password[3]),
    .Y(_074_)
);

XOR _lock4_ (
    .A(_l4_),
    .B(password[4]),
    .Y(_058_)
);

XOR _lock5_ (
    .A(_l5_),
    .B(password[5]),
    .Y(_029_)
);

XOR _lock6_ (
    .A(_l6_),
    .B(password[6]),
    .Y(_035_)
);

XOR _lock7_ (
    .A(_l7_),
    .B(password[7]),
    .Y(_093_)
);

XOR _lock8_ (
    .A(_l8_),
    .B(password[8]),
    .Y(_080_)
);

XOR _lock9_ (
    .A(_l9_),
    .B(password[9]),
    .Y(_049_)
);

XOR _lock10_ (
    .A(_l10_),
    .B(password[10]),
    .Y(_111_)
);

XOR _lock11_ (
    .A(_l11_),
    .B(password[11]),
    .Y(_122_)
);

XOR _lock12_ (
    .A(_l12_),
    .B(password[12]),
    .Y(c[0])
);

XOR _lock13_ (
    .A(_l13_),
    .B(password[13]),
    .Y(_091_)
);

XOR _lock14_ (
    .A(_l14_),
    .B(password[14]),
    .Y(_100_)
);

XOR _lock15_ (
    .A(_l15_),
    .B(password[15]),
    .Y(_043_)
);

XOR _lock16_ (
    .A(_l16_),
    .B(password[16]),
    .Y(_132_)
);

XOR _lock17_ (
    .A(_l17_),
    .B(password[17]),
    .Y(c[6])
);

XOR _lock18_ (
    .A(_l18_),
    .B(password[18]),
    .Y(_046_)
);

XOR _lock19_ (
    .A(_l19_),
    .B(password[19]),
    .Y(_096_)
);

XOR _lock20_ (
    .A(_l20_),
    .B(password[20]),
    .Y(_000_)
);

XOR _lock21_ (
    .A(_l21_),
    .B(password[21]),
    .Y(_009_)
);

XOR _lock22_ (
    .A(_l22_),
    .B(password[22]),
    .Y(c[13])
);

XOR _lock23_ (
    .A(_l23_),
    .B(password[23]),
    .Y(_125_)
);

XOR _lock24_ (
    .A(_l24_),
    .B(password[24]),
    .Y(_010_)
);

XOR _lock25_ (
    .A(_l25_),
    .B(password[25]),
    .Y(c[12])
);

XOR _lock26_ (
    .A(_l26_),
    .B(password[26]),
    .Y(_044_)
);

XOR _lock27_ (
    .A(_l27_),
    .B(password[27]),
    .Y(_028_)
);

XOR _lock28_ (
    .A(_l28_),
    .B(password[28]),
    .Y(_051_)
);

XOR _lock29_ (
    .A(_l29_),
    .B(password[29]),
    .Y(c[1])
);

XOR _lock30_ (
    .A(_l30_),
    .B(password[30]),
    .Y(_119_)
);

XOR _lock31_ (
    .A(_l31_),
    .B(password[31]),
    .Y(c[8])
);

XOR _lock32_ (
    .A(_l32_),
    .B(password[32]),
    .Y(_126_)
);

XOR _lock33_ (
    .A(_l33_),
    .B(password[33]),
    .Y(_004_)
);

XOR _lock34_ (
    .A(_l34_),
    .B(password[34]),
    .Y(_115_)
);

XOR _lock35_ (
    .A(_l35_),
    .B(password[35]),
    .Y(_059_)
);

XOR _lock36_ (
    .A(_l36_),
    .B(password[36]),
    .Y(_065_)
);

XOR _lock37_ (
    .A(_l37_),
    .B(password[37]),
    .Y(_053_)
);

XOR _lock38_ (
    .A(_l38_),
    .B(password[38]),
    .Y(_005_)
);

XOR _lock39_ (
    .A(_l39_),
    .B(password[39]),
    .Y(_056_)
);

XOR _lock40_ (
    .A(_l40_),
    .B(password[40]),
    .Y(c[30])
);

XOR _lock41_ (
    .A(_l41_),
    .B(password[41]),
    .Y(c[9])
);

XOR _lock42_ (
    .A(_l42_),
    .B(password[42]),
    .Y(_037_)
);

XOR _lock43_ (
    .A(_l43_),
    .B(password[43]),
    .Y(_114_)
);

XOR _lock44_ (
    .A(_l44_),
    .B(password[44]),
    .Y(_106_)
);

XOR _lock45_ (
    .A(_l45_),
    .B(password[45]),
    .Y(c[19])
);

XOR _lock46_ (
    .A(_l46_),
    .B(password[46]),
    .Y(_027_)
);

XOR _lock47_ (
    .A(_l47_),
    .B(password[47]),
    .Y(_061_)
);
endmodule

</details>

ta dự đoán chương trình thực hiện a+b và mã hóa với key là password, nếu password đúng thì c==a+b
mô phỏng lại chương trình bằng C:

#include <stdio.h>
#include <stdint.h>

uint32_t add(uint32_t a, uint32_t b, uint64_t password) {
    // Khai báo tất cả các tín hiệu nội bộ (mỗi tín hiệu là 1 bit, dùng kiểu int)
    int _000_, _001_, _002_, _003_, _004_, _005_, _006_, _007_, _008_, _009_, _010_,
        _011_, _012_, _013_, _014_, _015_, _016_, _017_, _018_, _019_, _020_, _021_,
        _022_, _023_, _024_, _025_, _026_, _027_, _028_, _029_, _030_, _031_, _032_,
        _033_, _034_, _035_, _036_, _037_, _038_, _039_, _040_, _041_, _042_, _043_,
        _044_, _045_, _046_, _047_, _048_, _049_, _050_, _051_, _052_, _053_, _054_,
        _055_, _056_, _057_, _058_, _059_, _060_, _061_, _062_, _063_, _064_, _065_,
        _066_, _067_, _068_, _069_, _070_, _071_, _072_, _073_, _074_, _075_, _076_,
        _077_, _078_, _079_, _080_, _081_, _082_, _083_, _084_, _085_, _086_, _087_,
        _088_, _089_, _090_, _091_, _092_, _093_, _094_, _095_, _096_, _097_, _098_,
        _099_, _100_, _101_, _102_, _103_, _104_, _105_, _106_, _107_, _108_, _109_,
        _110_, _111_, _112_, _113_, _114_, _115_, _116_, _117_, _118_, _119_, _120_,
        _121_, _122_, _123_, _124_, _125_, _126_, _127_, _128_, _129_, _130_, _131_,
        _132_;

    // Các tín hiệu “l” (được tính từ a, b ban đầu)
    int _l0_, _l1_, _l2_, _l3_, _l4_, _l5_, _l6_, _l7_, _l8_, _l9_, _l10_, _l11_,
        _l12_, _l13_, _l14_, _l15_, _l16_, _l17_, _l18_, _l19_, _l20_, _l21_,
        _l22_, _l23_, _l24_, _l25_, _l26_, _l27_, _l28_, _l29_, _l30_, _l31_,
        _l32_, _l33_, _l34_, _l35_, _l36_, _l37_, _l38_, _l39_, _l40_, _l41_,
        _l42_, _l43_, _l44_, _l45_, _l46_, _l47_;

    // Các bit output riêng lẻ (c[0] tới c[31])
    int c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15,
        c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29,
        c30, c31;

    // --- Các cổng của mạch (theo thứ tự của netlist) ---

    // NAND _133_ (.A(a[12]), .B(b[12]), .Y(_130_));
    _130_ = !(((a >> 12) & 1) & ((b >> 12) & 1));
    // XOR _134_ (.A(a[12]), .B(b[12]), .Y(_131_));
    _131_ = (((a >> 12) & 1) ^ ((b >> 12) & 1));
    // NAND _135_ (.A(a[11]), .B(b[11]), .Y(_l16_));
    _l16_ = !(((a >> 11) & 1) & ((b >> 11) & 1));
    // NOR _136_ (.A(a[11]), .B(b[11]), .Y(_l20_));
    _l20_ = !(((a >> 11) & 1) | ((b >> 11) & 1));
    // NAND _137_ (.A(a[10]), .B(b[10]), .Y(_001_));
    _001_ = !(((a >> 10) & 1) & ((b >> 10) & 1));
    // XOR _138_ (.A(a[10]), .B(b[10]), .Y(_002_));
    _002_ = (((a >> 10) & 1) ^ ((b >> 10) & 1));
    // NAND _139_ (.A(a[9]), .B(b[9]), .Y(_003_));
    _003_ = !(((a >> 9) & 1) & ((b >> 9) & 1));
    // NOR _140_ (.A(a[9]), .B(b[9]), .Y(_l33_));
    _l33_ = !(((a >> 9) & 1) | ((b >> 9) & 1));
    // AND _141_ (.A(a[8]), .B(b[8]), .Y(_l38_));
    _l38_ = (((a >> 8) & 1) & ((b >> 8) & 1));
    // XOR _142_ (.A(a[8]), .B(b[8]), .Y(_006_));
    _006_ = (((a >> 8) & 1) ^ ((b >> 8) & 1));
    // NAND _143_ (.A(a[7]), .B(b[7]), .Y(_007_));
    _007_ = !(((a >> 7) & 1) & ((b >> 7) & 1));
    // OR _144_ (.A(a[7]), .B(b[7]), .Y(_008_));
    _008_ = (((a >> 7) & 1) | ((b >> 7) & 1));
    // AND _145_ (.A(a[6]), .B(b[6]), .Y(_l21_));
    _l21_ = (((a >> 6) & 1) & ((b >> 6) & 1));
    // XOR _146_ (.A(a[6]), .B(b[6]), .Y(_l24_));
    _l24_ = (((a >> 6) & 1) ^ ((b >> 6) & 1));
    // NAND _147_ (.A(a[5]), .B(b[5]), .Y(_011_));
    _011_ = !(((a >> 5) & 1) & ((b >> 5) & 1));
    // NAND _148_ (.A(a[4]), .B(b[4]), .Y(_012_));
    _012_ = !(((a >> 4) & 1) & ((b >> 4) & 1));
    // NAND _149_ (.A(a[3]), .B(b[3]), .Y(_013_));
    _013_ = !(((a >> 3) & 1) & ((b >> 3) & 1));
    // NAND _150_ (.A(a[2]), .B(b[2]), .Y(_014_));
    _014_ = !(((a >> 2) & 1) & ((b >> 2) & 1));
    // NAND _151_ (.A(a[1]), .B(b[1]), .Y(_015_));
    _015_ = !(((a >> 1) & 1) & ((b >> 1) & 1));
    // AND _152_ (.A(a[0]), .B(b[0]), .Y(_016_));
    _016_ = (((a >> 0) & 1) & ((b >> 0) & 1));
    // XOR _153_ (.A(a[1]), .B(b[1]), .Y(_017_));
    _017_ = (((a >> 1) & 1) ^ ((b >> 1) & 1));
    // NAND _154_ (.A(_016_), .B(_017_), .Y(_018_));
    _018_ = !(_016_ & _017_);
    // NAND _155_ (.A(_015_), .B(_018_), .Y(_019_));
    _019_ = !(_015_ & _018_);
    // XOR _156_ (.A(a[2]), .B(b[2]), .Y(_020_));
    _020_ = (((a >> 2) & 1) ^ ((b >> 2) & 1));
    // NAND _157_ (.A(_019_), .B(_020_), .Y(_021_));
    _021_ = !(_019_ & _020_);
    // NAND _158_ (.A(_014_), .B(_021_), .Y(_022_));
    _022_ = !(_014_ & _021_);
    // XOR _159_ (.A(a[3]), .B(b[3]), .Y(_023_));
    _023_ = (((a >> 3) & 1) ^ ((b >> 3) & 1));
    // NAND _160_ (.A(_022_), .B(_023_), .Y(_024_));
    _024_ = !(_022_ & _023_);
    // NAND _161_ (.A(_013_), .B(_024_), .Y(_025_));
    _025_ = !(_013_ & _024_);
    // XNOR _162_ (.A(a[4]), .B(b[4]), .Y(_l0_));
    _l0_ = !((((a >> 4) & 1) ^ ((b >> 4) & 1)));

    // --- Các tín hiệu lock được “tái gán” bằng XOR với các bit password.
    // _lock0_: _026_ = _l0_ XOR password[0]
    _026_ = _l0_ ^ ((password >> 0) & 1);
    // AND _163_ (.A(_025_), .B(_026_), .Y(_l46_));
    _l46_ = _025_ & _026_;
    // _lock46_: _027_ = _l46_ XOR password[46]
    _027_ = _l46_ ^ ((password >> 46) & 1);
    // AND _164_ (.A(_012_), .B(_027_), .Y(_l27_));
    _l27_ = _012_ & _027_;
    // XOR _165_ (.A(a[5]), .B(b[5]), .Y(_l5_));
    _l5_ = (((a >> 5) & 1) ^ ((b >> 5) & 1));
    // _lock5_: _029_ = _l5_ XOR password[5]
    _029_ = _l5_ ^ ((password >> 5) & 1);
    // _lock27_: _028_ = _l27_ XOR password[27]
    _028_ = _l27_ ^ ((password >> 27) & 1);
    // NAND _166_ (.A(_028_), .B(_029_), .Y(_030_));
    _030_ = !(_028_ & _029_);
    // NAND _167_ (.A(_011_), .B(_030_), .Y(_031_));
    _031_ = !(_011_ & _030_);
    // _lock24_: _010_ = _l24_ XOR password[24]
    _010_ = _l24_ ^ ((password >> 24) & 1);
    // NAND _168_ (.A(_010_), .B(_031_), .Y(_032_));
    _032_ = !(_010_ & _031_);
    // _lock21_: _009_ = _l21_ XOR password[21]
    _009_ = _l21_ ^ ((password >> 21) & 1);
    // NAND _169_ (.A(_009_), .B(_032_), .Y(_033_));
    _033_ = !(_009_ & _032_);
    // NAND _170_ (.A(_008_), .B(_033_), .Y(_034_));
    _034_ = !(_008_ & _033_);
    // AND _171_ (.A(_007_), .B(_034_), .Y(_l6_));
    _l6_ = _007_ & _034_;
    // _lock6_: _035_ = _l6_ XOR password[6]
    _035_ = _l6_ ^ ((password >> 6) & 1);
    // NAND _172_ (.A(_006_), .B(_035_), .Y(_036_));
    _036_ = !(_006_ & _035_);
    // _lock38_: _005_ = _l38_ XOR password[38]
    _005_ = _l38_ ^ ((password >> 38) & 1);
    // AND _173_ (.A(_005_), .B(_036_), .Y(_l42_));
    _l42_ = _005_ & _036_;
    // _lock33_: _004_ = _l33_ XOR password[33]
    _004_ = _l33_ ^ ((password >> 33) & 1);
    // _lock42_: _037_ = _l42_ XOR password[42]
    _037_ = _l42_ ^ ((password >> 42) & 1);
    // NAND _174_ (.A(_004_), .B(_037_), .Y(_038_));
    _038_ = !(_004_ & _037_);
    // NAND _175_ (.A(_003_), .B(_038_), .Y(_039_));
    _039_ = !(_003_ & _038_);
    // NAND _176_ (.A(_002_), .B(_039_), .Y(_040_));
    _040_ = !(_002_ & _039_);
    // NAND _177_ (.A(_001_), .B(_040_), .Y(_041_));
    _041_ = !(_001_ & _040_);
    // _lock20_: _000_ = _l20_ XOR password[20]
    _000_ = _l20_ ^ ((password >> 20) & 1);
    // NAND _178_ (.A(_000_), .B(_041_), .Y(_042_));
    _042_ = !(_000_ & _041_);
    // _lock16_: _132_ = _l16_ XOR password[16]
    _132_ = _l16_ ^ ((password >> 16) & 1);
    // NAND _179_ (.A(_132_), .B(_042_), .Y(_l15_));
    _l15_ = !(_132_ & _042_);
    // _lock15_: _043_ = _l15_ XOR password[15]
    _043_ = _l15_ ^ ((password >> 15) & 1);
    // AND _180_ (.A(_131_), .B(_043_), .Y(_l26_));
    _l26_ = _131_ & _043_;
    // _lock26_: _044_ = _l26_ XOR password[26]
    _044_ = _l26_ ^ ((password >> 26) & 1);
    // AND _181_ (.A(_130_), .B(_044_), .Y(_045_));
    _045_ = _130_ & _044_;
    // NAND _182_ (.A(a[13]), .B(b[13]), .Y(_l18_));
    _l18_ = !(((a >> 13) & 1) & ((b >> 13) & 1));
    // OR _183_ (.A(a[13]), .B(b[13]), .Y(_047_));
    _047_ = (((a >> 13) & 1) | ((b >> 13) & 1));
    // XOR _184_ (.A(a[13]), .B(b[13]), .Y(_048_));
    _048_ = (((a >> 13) & 1) ^ ((b >> 13) & 1));
    // XNOR _185_ (.A(_045_), .B(_048_), .Y(_l22_));
    _l22_ = !(_045_ ^ _048_);
    // AND _186_ (.A(a[14]), .B(b[14]), .Y(_l9_));
    _l9_ = (((a >> 14) & 1) & ((b >> 14) & 1));
    // XOR _187_ (.A(a[14]), .B(b[14]), .Y(_050_));
    _050_ = (((a >> 14) & 1) ^ ((b >> 14) & 1));
    // NAND _188_ (.A(_045_), .B(_046_), .Y(_l28_));
    // _lock18_: _046_ = _l18_ XOR password[18]
    _046_ = _l18_ ^ ((password >> 18) & 1);
    _l28_ = !(_045_ & _046_);
    // _lock28_: _051_ = _l28_ XOR password[28]
    _051_ = _l28_ ^ ((password >> 28) & 1);
    // AND _189_ (.A(_047_), .B(_051_), .Y(_052_));
    _052_ = _047_ & _051_;
    // AND _190_ (.A(_050_), .B(_052_), .Y(_l37_));
    _l37_ = _050_ & _052_;
    // XOR _191_ (.A(_050_), .B(_052_), .Y(c14));
    c14 = _050_ ^ _052_;
    // AND _192_ (.A(_049_), .B(_053_), .Y(_054_));
    // _lock9_: _049_ = _l9_ XOR password[9]
    _049_ = _l9_ ^ ((password >> 9) & 1);
    // _lock37_: _053_ = _l37_ XOR password[37]
    _053_ = _l37_ ^ ((password >> 37) & 1);
    _054_ = _049_ & _053_;
    // NAND _193_ (.A(a[15]), .B(b[15]), .Y(_055_));
    _055_ = !(((a >> 15) & 1) & ((b >> 15) & 1));
    // OR _194_ (.A(a[15]), .B(b[15]), .Y(_l39_));
    _l39_ = (((a >> 15) & 1) | ((b >> 15) & 1));
    // XOR _195_ (.A(a[15]), .B(b[15]), .Y(_057_));
    _057_ = (((a >> 15) & 1) ^ ((b >> 15) & 1));
    // XNOR _196_ (.A(_054_), .B(_057_), .Y(c15));
    c15 = !(_054_ ^ _057_);
    // NAND _197_ (.A(a[16]), .B(b[16]), .Y(_l4_));
    _l4_ = !(((a >> 16) & 1) & ((b >> 16) & 1));
    // XNOR _198_ (.A(a[16]), .B(b[16]), .Y(_l35_));
    _l35_ = !(((a >> 16) & 1) ^ ((b >> 16) & 1));
    // NAND _199_ (.A(_054_), .B(_055_), .Y(_060_));
    _060_ = !(_054_ & _055_);
    // _lock35_: _059_ = _l35_ XOR password[35]
    _059_ = _l35_ ^ ((password >> 35) & 1);
    // _lock39_: _056_ = _l39_ XOR password[39]
    _056_ = _l39_ ^ ((password >> 39) & 1);
    // AND _200_ (.A(_056_), .B(_060_), .Y(_l47_));
    _l47_ = _056_ & _060_;
    // NAND _201_ (.A(_059_), .B(_061_), .Y(_062_));
    // _lock47_: _061_ = _l47_ XOR password[47]
    _061_ = _l47_ ^ ((password >> 47) & 1);
    _062_ = !(_059_ & _061_);
    // XOR _202_ (.A(_059_), .B(_061_), .Y(c16));
    c16 = _059_ ^ _061_;
    // AND _203_ (.A(_058_), .B(_062_), .Y(_063_));
    // _lock4_: _058_ = _l4_ XOR password[4]
    _058_ = _l4_ ^ ((password >> 4) & 1);
    _063_ = _058_ & _062_;
    // NAND _204_ (.A(a[17]), .B(b[17]), .Y(_064_));
    _064_ = !(((a >> 17) & 1) & ((b >> 17) & 1));
    // OR _205_ (.A(a[17]), .B(b[17]), .Y(_l36_));
    _l36_ = (((a >> 17) & 1) | ((b >> 17) & 1));
    // XOR _206_ (.A(a[17]), .B(b[17]), .Y(_066_));
    _066_ = (((a >> 17) & 1) ^ ((b >> 17) & 1));
    // XNOR _207_ (.A(_063_), .B(_066_), .Y(c17));
    c17 = !(_063_ ^ _066_);
    // NAND _208_ (.A(a[18]), .B(b[18]), .Y(_067_));
    _067_ = !(((a >> 18) & 1) & ((b >> 18) & 1));
    // XOR _209_ (.A(a[18]), .B(b[18]), .Y(_068_));
    _068_ = (((a >> 18) & 1) ^ ((b >> 18) & 1));
    // NAND _210_ (.A(_063_), .B(_064_), .Y(_069_));
    _069_ = !(_063_ & _064_);
    // _lock36_: _065_ = _l36_ XOR password[36]
    _065_ = _l36_ ^ ((password >> 36) & 1);
    // AND _211_ (.A(_065_), .B(_069_), .Y(_070_));
    _070_ = _065_ & _069_;
    // NAND _212_ (.A(_068_), .B(_070_), .Y(_071_));
    _071_ = !(_068_ & _070_);
    // XOR _213_ (.A(_068_), .B(_070_), .Y(c18));
    c18 = _068_ ^ _070_;
    // AND _214_ (.A(_067_), .B(_071_), .Y(_072_));
    _072_ = _067_ & _071_;
    // NAND _215_ (.A(a[19]), .B(b[19]), .Y(_073_));
    _073_ = !(((a >> 19) & 1) & ((b >> 19) & 1));
    // NOR _216_ (.A(a[19]), .B(b[19]), .Y(_l3_));
    _l3_ = !(((a >> 19) & 1) | ((b >> 19) & 1));
    // XOR _217_ (.A(a[19]), .B(b[19]), .Y(_075_));
    _075_ = (((a >> 19) & 1) ^ ((b >> 19) & 1));
    // XOR _218_ (.A(_72_), .B(_075_), .Y(_l45_));
    _l45_ = _072_ ^ _075_;
    // NAND _219_ (.A(a[20]), .B(b[20]), .Y(_076_));
    _076_ = !(((a >> 20) & 1) & ((b >> 20) & 1));
    // XOR _220_ (.A(a[20]), .B(b[20]), .Y(_077_));
    _077_ = (((a >> 20) & 1) ^ ((b >> 20) & 1));
    // NAND _221_ (.A(_072_), .B(_073_), .Y(_078_));
    _078_ = !(_072_ & _073_);
    // _lock3_: _074_ = _l3_ XOR password[3]
    _074_ = _l3_ ^ ((password >> 3) & 1);
    // AND _222_ (.A(_074_), .B(_078_), .Y(_079_));
    _079_ = _074_ & _078_;
    // AND _223_ (.A(_077_), .B(_079_), .Y(_l8_));
    _l8_ = _077_ & _079_;
    // XOR _224_ (.A(_077_), .B(_079_), .Y(c20));
    c20 = _077_ ^ _079_;
    // AND _225_ (.A(_076_), .B(_080_), .Y(_081_));
    // _lock8_: _080_ = _l8_ XOR password[8]
    _080_ = _l8_ ^ ((password >> 8) & 1);
    _081_ = _076_ & _080_;
    // NAND _226_ (.A(a[21]), .B(b[21]), .Y(_l2_));
    _l2_ = !(((a >> 21) & 1) & ((b >> 21) & 1));
    // OR _227_ (.A(a[21]), .B(b[21]), .Y(_083_));
    _083_ = (((a >> 21) & 1) | ((b >> 21) & 1));
    // XOR _228_ (.A(a[21]), .B(b[21]), .Y(_084_));
    _084_ = (((a >> 21) & 1) ^ ((b >> 21) & 1));
    // XNOR _229_ (.A(_081_), .B(_084_), .Y(c21));
    c21 = !(_081_ ^ _084_);
    // NAND _230_ (.A(a[22]), .B(b[22]), .Y(_085_));
    _085_ = !(((a >> 22) & 1) & ((b >> 22) & 1));
    // XNOR _231_ (.A(a[22]), .B(b[22]), .Y(_l1_));
    _l1_ = !(((a >> 22) & 1) ^ ((b >> 22) & 1));
    // NAND _232_ (.A(_081_), .B(_082_), .Y(_087_));
    // _lock2_: _082_ = _l2_ XOR password[2]
    _082_ = _l2_ ^ ((password >> 2) & 1);
    _087_ = !(_081_ & _082_);
    // AND _233_ (.A(_083_), .B(_087_), .Y(_088_));
    _088_ = _083_ & _087_;
    // NAND _234_ (.A(_086_), .B(_088_), .Y(_089_));
    // _lock1_: _086_ = _l1_ XOR password[1]
    _086_ = _l1_ ^ ((password >> 1) & 1);
    _089_ = !(_086_ & _088_);
    // XOR _235_ (.A(_086_), .B(_088_), .Y(c22));
    c22 = _086_ ^ _088_;
    // AND _236_ (.A(_085_), .B(_089_), .Y(_090_));
    _090_ = _085_ & _089_;
    // AND _237_ (.A(a[23]), .B(b[23]), .Y(_l13_));
    _l13_ = (((a >> 23) & 1) & ((b >> 23) & 1));
    // OR _238_ (.A(a[23]), .B(b[23]), .Y(_092_));
    _092_ = (((a >> 23) & 1) | ((b >> 23) & 1));
    // XOR _239_ (.A(a[23]), .B(b[23]), .Y(_l7_));
    _l7_ = (((a >> 23) & 1) ^ ((b >> 23) & 1));
    // _lock7_: _093_ = _l7_ XOR password[7]  (đã tính ở trên)
    // XNOR _240_ (.A(_090_), .B(_093_), .Y(c23));
    c23 = !(_090_ ^ _093_);
    // NAND _241_ (.A(a[24]), .B(b[24]), .Y(_094_));
    _094_ = !(((a >> 24) & 1) & ((b >> 24) & 1));
    // XOR _242_ (.A(a[24]), .B(b[24]), .Y(_095_));
    _095_ = (((a >> 24) & 1) ^ ((b >> 24) & 1));
    // NAND _243_ (.A(_090_), .B(_091_), .Y(_l19_));
    // _lock13_: _091_ = _l13_ XOR password[13]
    _091_ = _l13_ ^ ((password >> 13) & 1);
    _l19_ = !(_090_ & _091_);
    // AND _244_ (.A(_092_), .B(_096_), .Y(_097_));
    // _lock19_: _096_ = _l19_ XOR password[19]
    _096_ = _l19_ ^ ((password >> 19) & 1);
    _097_ = _092_ & _096_;
    // NAND _245_ (.A(_095_), .B(_097_), .Y(_098_));
    _098_ = !(_095_ & _097_);
    // XOR _246_ (.A(_095_), .B(_097_), .Y(c24));
    c24 = _095_ ^ _097_;
    // AND _247_ (.A(_094_), .B(_098_), .Y(_099_));
    _099_ = _094_ & _098_;
    // AND _248_ (.A(a[25]), .B(b[25]), .Y(_l14_));
    _l14_ = (((a >> 25) & 1) & ((b >> 25) & 1));
    // OR _249_ (.A(a[25]), .B(b[25]), .Y(_101_));
    _101_ = (((a >> 25) & 1) | ((b >> 25) & 1));
    // XOR _250_ (.A(a[25]), .B(b[25]), .Y(_102_));
    _102_ = (((a >> 25) & 1) ^ ((b >> 25) & 1));
    // XNOR _251_ (.A(_099_), .B(_102_), .Y(c25));
    c25 = !(_099_ ^ _102_);
    // NAND _252_ (.A(a[26]), .B(b[26]), .Y(_103_));
    _103_ = !(((a >> 26) & 1) & ((b >> 26) & 1));
    // XOR _253_ (.A(a[26]), .B(b[26]), .Y(_104_));
    _104_ = (((a >> 26) & 1) ^ ((b >> 26) & 1));
    // NAND _254_ (.A(_099_), .B(_100_), .Y(_105_));
    // _lock14_: _100_ = _l14_ XOR password[14]
    _100_ = _l14_ ^ ((password >> 14) & 1);
    _105_ = !(_099_ & _100_);
    // NAND _255_ (.A(_101_), .B(_105_), .Y(_l44_));
    _l44_ = !(_101_ & _105_);
    // NAND _256_ (.A(_104_), .B(_106_), .Y(_107_));
    // _lock44_: _106_ = _l44_ XOR password[44]
    _106_ = _l44_ ^ ((password >> 44) & 1);
    _107_ = !(_104_ & _106_);
    // XOR _257_ (.A(_104_), .B(_106_), .Y(c26));
    c26 = _104_ ^ _106_;
    // AND _258_ (.A(_103_), .B(_107_), .Y(_108_));
    _108_ = _103_ & _107_;
    // NAND _259_ (.A(a[27]), .B(b[27]), .Y(_109_));
    _109_ = !(((a >> 27) & 1) & ((b >> 27) & 1));
    // OR _260_ (.A(a[27]), .B(b[27]), .Y(_110_));
    _110_ = (((a >> 27) & 1) | ((b >> 27) & 1));
    // XOR _261_ (.A(a[27]), .B(b[27]), .Y(_l10_));
    _l10_ = (((a >> 27) & 1) ^ ((b >> 27) & 1));
    // _lock10_: _111_ = _l10_ XOR password[10]
    _111_ = _l10_ ^ ((password >> 10) & 1);
    // XNOR _262_ (.A(_108_), .B(_111_), .Y(c27));
    c27 = !(_108_ ^ _111_);
    // NAND _263_ (.A(a[28]), .B(b[28]), .Y(_112_));
    _112_ = !(((a >> 28) & 1) & ((b >> 28) & 1));
    // XOR _264_ (.A(a[28]), .B(b[28]), .Y(_113_));
    _113_ = (((a >> 28) & 1) ^ ((b >> 28) & 1));
    // NAND _265_ (.A(_108_), .B(_109_), .Y(_l43_));
    _l43_ = !(_108_ & _109_);
    // NAND _266_ (.A(_110_), .B(_114_), .Y(_l34_));
    // _lock43_: _114_ = _l43_ XOR password[43]
    _114_ = _l43_ ^ ((password >> 43) & 1);
    _l34_ = !(_110_ & _114_);
    // NAND _267_ (.A(_113_), .B(_115_), .Y(_116_));
    // _lock34_: _115_ = _l34_ XOR password[34]
    _115_ = _l34_ ^ ((password >> 34) & 1);
    _116_ = !(_113_ & _115_);
    // XOR _268_ (.A(_113_), .B(_115_), .Y(c28));
    c28 = _113_ ^ _115_;
    // NAND _269_ (.A(_112_), .B(_116_), .Y(_117_));
    _117_ = !(_112_ & _116_);
    // NAND _270_ (.A(a[29]), .B(b[29]), .Y(_118_));
    _118_ = !(((a >> 29) & 1) & ((b >> 29) & 1));
    // XNOR _271_ (.A(a[29]), .B(b[29]), .Y(_l30_));
    _l30_ = !((((a >> 29) & 1) ^ ((b >> 29) & 1)));
    // _lock30_: _119_ = _l30_ XOR password[30]
    _119_ = _l30_ ^ ((password >> 30) & 1);
    // NAND _272_ (.A(_117_), .B(_119_), .Y(_120_));
    _120_ = !(_117_ & _119_);
    // XOR _273_ (.A(_117_), .B(_119_), .Y(c29));
    c29 = _117_ ^ _119_;
    // NAND _274_ (.A(_118_), .B(_120_), .Y(_121_));
    _121_ = !(_118_ & _120_);
    // NAND _275_ (.A(a[30]), .B(b[30]), .Y(_l11_));
    _l11_ = !(((a >> 30) & 1) & ((b >> 30) & 1));
    // XOR _276_ (.A(a[30]), .B(b[30]), .Y(_123_));
    _123_ = (((a >> 30) & 1) ^ ((b >> 30) & 1));
    // NAND _277_ (.A(_121_), .B(_123_), .Y(_124_));
    _124_ = !(_121_ & _123_);
    // XNOR _278_ (.A(_121_), .B(_123_), .Y(_l40_));
    _l40_ = !(_121_ ^ _123_);
    // _lock11_: _122_ = _l11_ XOR password[11]
    _122_ = _l11_ ^ ((password >> 11) & 1);
    // NAND _279_ (.A(_122_), .B(_124_), .Y(_l23_));
    _l23_ = !(_122_ & _124_);
    // XNOR _280_ (.A(a[31]), .B(b[31]), .Y(_l32_));
    _l32_ = !((((a >> 31) & 1) ^ ((b >> 31) & 1)));
    // _lock23_: _125_ = _l23_ XOR password[23]
    _125_ = _l23_ ^ ((password >> 23) & 1);
    // _lock32_: _126_ = _l32_ XOR password[32]
    _126_ = _l32_ ^ ((password >> 32) & 1);
    // XNOR _281_ (.A(_125_), .B(_126_), .Y(c31));
    c31 = !(_125_ ^ _126_);
    // XOR _282_ (.A(a[0]), .B(b[0]), .Y(_l12_));
    _l12_ = (((a >> 0) & 1) ^ ((b >> 0) & 1));
    // XOR _283_ (.A(_016_), .B(_017_), .Y(_l29_));
    _l29_ = _016_ ^ _017_;
    // XOR _284_ (.A(_019_), .B(_020_), .Y(c2));
    c2 = _019_ ^ _020_;
    // XOR _285_ (.A(_022_), .B(_023_), .Y(c3));
    c3 = _022_ ^ _023_;
    // XOR _286_ (.A(_025_), .B(_026_), .Y(c4));
    c4 = _025_ ^ _026_;
    // XOR _287_ (.A(_028_), .B(_029_), .Y(c5));
    c5 = _028_ ^ _029_;
    // Note: dòng _287_ dùng _028_ và _029_ đã tính ở trên.
    // XOR _288_ (.A(_010_), .B(_031_), .Y(_l17_));
    _l17_ = _010_ ^ _031_;
    // XNOR _289_ (.A(a[7]), .B(b[7]), .Y(_127_));
    _127_ = !((((a >> 7) & 1) ^ ((b >> 7) & 1)));
    // XNOR _290_ (.A(_033_), .B(_127_), .Y(c7));
    c7 = !(_033_ ^ _127_);
    // XOR _291_ (.A(_006_), .B(_035_), .Y(_l31_));
    _l31_ = _006_ ^ _035_;
    // XNOR _292_ (.A(a[9]), .B(b[9]), .Y(_128_));
    _128_ = !((((a >> 9) & 1) ^ ((b >> 9) & 1)));
    // XNOR _293_ (.A(_037_), .B(_128_), .Y(_l41_));
    _l41_ = !(_037_ ^ _128_);
    // XOR _294_ (.A(_002_), .B(_039_), .Y(c10));
    c10 = _002_ ^ _039_;
    // XNOR _295_ (.A(a[11]), .B(b[11]), .Y(_129_));
    _129_ = !((((a >> 11) & 1) ^ ((b >> 11) & 1)));
    // XNOR _296_ (.A(_041_), .B(_129_), .Y(c11));
    c11 = !(_041_ ^ _129_);
    // XOR _297_ (.A(_131_), .B(_043_), .Y(_l25_));
    _l25_ = _131_ ^ _043_;

    // --- Các dòng lock trực tiếp gán giá trị cho các bit c đã định nghĩa ---
    // _lock12_: c[0] = _l12_ XOR password[12]
    c0 = _l12_ ^ ((password >> 12) & 1);
    // _lock17_: c[6] = _l17_ XOR password[17]
    c6 = _l17_ ^ ((password >> 17) & 1);
    // _lock22_: c[13] = _l22_ XOR password[22]
    c13 = _l22_ ^ ((password >> 22) & 1);
    // _lock25_: c[12] = _l25_ XOR password[25]
    c12 = _l25_ ^ ((password >> 25) & 1);
    // _lock29_: c[1] = _l29_ XOR password[29]
    c1 = _l29_ ^ ((password >> 29) & 1);
    // _lock31_: c[8] = _l31_ XOR password[31]
    c8 = _l31_ ^ ((password >> 31) & 1);
    // _lock41_: c[9] = _l41_ XOR password[41]
    c9 = _l41_ ^ ((password >> 41) & 1);
    // _lock40_: c[30] = _l40_ XOR password[40]
    c30 = _l40_ ^ ((password >> 40) & 1);
    // _lock45_: c[19] = _l45_ XOR password[45]
    c19 = _l45_ ^ ((password >> 45) & 1);

    // Kết hợp các bit c[0..31] thành 1 số 32-bit
    uint32_t result = (c0 & 1) |
                      ((c1 & 1) << 1) |
                      ((c2 & 1) << 2) |
                      ((c3 & 1) << 3) |
                      ((c4 & 1) << 4) |
                      ((c5 & 1) << 5) |
                      ((c6 & 1) << 6) |
                      ((c7 & 1) << 7) |
                      ((c8 & 1) << 8) |
                      ((c9 & 1) << 9) |
                      ((c10 & 1) << 10) |
                      ((c11 & 1) << 11) |
                      ((c12 & 1) << 12) |
                      ((c13 & 1) << 13) |
                      ((c14 & 1) << 14) |
                      ((c15 & 1) << 15) |
                      ((c16 & 1) << 16) |
                      ((c17 & 1) << 17) |
                      ((c18 & 1) << 18) |
                      ((c19 & 1) << 19) |
                      ((c20 & 1) << 20) |
                      ((c21 & 1) << 21) |
                      ((c22 & 1) << 22) |
                      ((c23 & 1) << 23) |
                      ((c24 & 1) << 24) |
                      ((c25 & 1) << 25) |
                      ((c26 & 1) << 26) |
                      ((c27 & 1) << 27) |
                      ((c28 & 1) << 28) |
                      ((c29 & 1) << 29) |
                      ((c30 & 1) << 30) |
                      ((c31 & 1) << 31);

    return result;
}

int main(void) {
    // Ví dụ kiểm tra hàm add:
    uint32_t a = 1;
    uint32_t b = 100;
    // Sử dụng 48-bit password (đặt trong biến 64-bit)
    uint64_t password ;
    //scanf("%lld", &password);
    //printf("%lld\n",password);
    password=7; // Nhập mật khẩu dưới dạng số nguyên
    //printf("%lld\n",password);

    uint32_t c = add(a, b, password);
    printf("%u",c);
    return 0;
}

ta thử với a=1, b=100, password=7:
vậy kết quả khá lệch với a+b=101.
thực hiện giải chương trình bằng z3 (prompt lòi ỉa mới ra):

from z3 import *

# Định nghĩa các cổng logic
def NAND_gate(a, b):
    return Not(And(a, b))

def NOR_gate(a, b):
    return Not(Or(a, b))

def XOR_gate(a, b):
    return Xor(a, b)

def XNOR_gate(a, b):
    return Not(Xor(a, b))

def AND_gate(a, b):
    return And(a, b)

def OR_gate(a, b):
    return Or(a, b)

# Hàm add mô phỏng mạch (netlist) được trích xuất từ Verilog.
# a, b: số nguyên 32-bit (test case); P: danh sách 48 biến Bool ứng với các bit của password.
def add(a, b, P):
    # Tách các bit của a và b thành danh sách các giá trị Bool (hằng số)
    A = [BoolVal(((a >> i) & 1) == 1) for i in range(32)]
    B = [BoolVal(((b >> i) & 1) == 1) for i in range(32)]
    
    # --- Các tín hiệu theo netlist (đoạn trích từ Verilog) ---
    _130_ = NAND_gate(A[12], B[12])
    _131_ = XOR_gate(A[12], B[12])
    _l16_ = NAND_gate(A[11], B[11])
    _l20_ = NOR_gate(A[11], B[11])
    _001_ = NAND_gate(A[10], B[10])
    _002_ = XOR_gate(A[10], B[10])
    _003_ = NAND_gate(A[9], B[9])
    _l33_ = NOR_gate(A[9], B[9])
    _l38_ = AND_gate(A[8], B[8])
    _006_ = XOR_gate(A[8], B[8])
    _007_ = NAND_gate(A[7], B[7])
    _008_ = OR_gate(A[7], B[7])
    _l21_ = AND_gate(A[6], B[6])
    _l24_ = XOR_gate(A[6], B[6])
    _011_ = NAND_gate(A[5], B[5])
    _012_ = NAND_gate(A[4], B[4])
    _013_ = NAND_gate(A[3], B[3])
    _014_ = NAND_gate(A[2], B[2])
    _015_ = NAND_gate(A[1], B[1])
    _016_ = AND_gate(A[0], B[0])
    _017_ = XOR_gate(A[1], B[1])
    _018_ = NAND_gate(_016_, _017_)
    _019_ = NAND_gate(_015_, _018_)
    _020_ = XOR_gate(A[2], B[2])
    _021_ = NAND_gate(_019_, _020_)
    _022_ = NAND_gate(_014_, _021_)
    _023_ = XOR_gate(A[3], B[3])
    _024_ = NAND_gate(_022_, _023_)
    _025_ = NAND_gate(_013_, _024_)
    _l0_ = XNOR_gate(A[4], B[4])
    # --- lock0 ---
    _026_ = XOR_gate(_l0_, P[0])
    _l46_ = AND_gate(_025_, _026_)
    # --- lock46 ---
    _027_ = XOR_gate(_l46_, P[46])
    _l27_ = AND_gate(_012_, _027_)
    _l5_ = XOR_gate(A[5], B[5])
    # --- lock5 ---
    _029_ = XOR_gate(_l5_, P[5])
    # --- lock27 ---
    _028_ = XOR_gate(_l27_, P[27])
    _030_ = NAND_gate(_028_, _029_)
    # --- lock24 ---
    _010_ = XOR_gate(_l24_, P[24])
    _031_ = NAND_gate(_011_, _030_)
    _032_ = NAND_gate(_010_, _031_)
    # --- lock21 ---
    _009_ = XOR_gate(_l21_, P[21])
    _033_ = NAND_gate(_009_, _032_)
    _034_ = NAND_gate(_008_, _033_)
    _l6_ = AND_gate(_007_, _034_)
    # --- lock6 ---
    _035_ = XOR_gate(_l6_, P[6])
    _036_ = NAND_gate(_006_, _035_)
    # --- lock38 ---
    _005_ = XOR_gate(_l38_, P[38])
    _l42_ = AND_gate(_005_, _036_)
    # --- lock33 ---
    _004_ = XOR_gate(_l33_, P[33])
    # --- lock42 ---
    _037_ = XOR_gate(_l42_, P[42])
    _038_ = NAND_gate(_004_, _037_)
    _039_ = NAND_gate(_003_, _038_)
    _040_ = NAND_gate(_002_, _039_)
    _041_ = NAND_gate(_001_, _040_)
    # --- lock20 ---
    _000_ = XOR_gate(_l20_, P[20])
    _042_ = NAND_gate(_000_, _041_)
    # --- lock16 ---
    _132_ = XOR_gate(_l16_, P[16])
    _l15_ = NAND_gate(_132_, _042_)
    # --- lock15 ---
    _043_ = XOR_gate(_l15_, P[15])
    _l26_ = AND_gate(_131_, _043_)
    # --- lock26 ---
    _044_ = XOR_gate(_l26_, P[26])
    _045_ = AND_gate(_130_, _044_)
    # --- lock18 ---
    _l18_ = NAND_gate(A[13], B[13])
    _047_ = OR_gate(A[13], B[13])
    _048_ = XOR_gate(A[13], B[13])
    _l22_ = XNOR_gate(_045_, _048_)
    # --- lock4 ---
    _l4_ = NAND_gate(A[16], B[16])
    _l35_ = XNOR_gate(A[16], B[16])
    # --- lock18 (đã tính) ---
    _046_ = XOR_gate(_l18_, P[18])
    _l28_ = NAND_gate(_045_, _046_)
    # --- lock28 ---
    _051_ = XOR_gate(_l28_, P[28])
    _052_ = AND_gate(_047_, _051_)
    _l37_ = AND_gate(XOR_gate(A[14], B[14]), _052_)
    # c[14] = XOR( XOR(a[14], b[14]), _052_)
    c14 = XOR_gate(XOR_gate(A[14], B[14]), _052_)
    # --- lock9 ---
    _l9_ = AND_gate(A[14], B[14])
    _049_ = XOR_gate(_l9_, P[9])
    # --- lock37 ---
    _053_ = XOR_gate(_l37_, P[37])
    _054_ = AND_gate(_049_, _053_)
    _055_ = NAND_gate(A[15], B[15])
    _l39_ = OR_gate(A[15], B[15])
    _057_ = XOR_gate(A[15], B[15])
    c15 = XNOR_gate(_054_, _057_)
    _l11_ = NAND_gate(A[30], B[30])
    # --- lock35 ---
    _059_ = XOR_gate(_l35_, P[35])
    # --- lock39 & lock47 ---
    _056_ = XOR_gate(_l39_, P[39])
    _060_ = NAND_gate(_054_, _055_)
    _l47_ = AND_gate(_056_, _060_)
    _061_ = XOR_gate(_l47_, P[47])
    c16 = XOR_gate(_059_, _061_)
    # --- lock4 ---
    _058_ = XOR_gate(_l4_, P[4])
    _062_ = NAND_gate(_059_, _061_)
    _063_ = AND_gate(_058_, _062_)
    _064_ = NAND_gate(A[17], B[17])
    _l36_ = OR_gate(A[17], B[17])
    _066_ = XOR_gate(A[17], B[17])
    c17 = XNOR_gate(_063_, _066_)
    _067_ = NAND_gate(A[18], B[18])
    _068_ = XOR_gate(A[18], B[18])
    _069_ = NAND_gate(_063_, _064_)
    # --- lock36 ---
    _065_ = XOR_gate(_l36_, P[36])
    _070_ = AND_gate(_065_, _069_)
    _071_ = NAND_gate(_068_, _070_)
    c18 = XOR_gate(_068_, _070_)
    _072_ = AND_gate(_067_, _071_)
    _073_ = NAND_gate(A[19], B[19])
    _l3_ = NOR_gate(A[19], B[19])
    _075_ = XOR_gate(A[19], B[19])
    _l45_ = XOR_gate(_072_, _075_)
    _076_ = NAND_gate(A[20], B[20])
    _077_ = XOR_gate(A[20], B[20])
    # --- lock3 ---
    _074_ = XOR_gate(_l3_, P[3])
    _078_ = NAND_gate(_072_, _073_)
    _079_ = AND_gate(_074_, _078_)
    _l8_ = AND_gate(_077_, _079_)
    c20 = XOR_gate(_077_, _079_)
    # --- lock8 ---
    _080_ = XOR_gate(_l8_, P[8])
    _081_ = AND_gate(_076_, _080_)
    _l2_ = NAND_gate(A[21], B[21])
    _083_ = OR_gate(A[21], B[21])
    _084_ = XOR_gate(A[21], B[21])
    c21 = XNOR_gate(_081_, _084_)
    _085_ = NAND_gate(A[22], B[22])
    _l1_ = XNOR_gate(A[22], B[22])
    # --- lock2 ---
    _082_ = XOR_gate(_l2_, P[2])
    _087_ = NAND_gate(_081_, _082_)
    _088_ = AND_gate(_083_, _087_)
    # --- lock1 ---
    _086_ = XOR_gate(_l1_, P[1])
    _089_ = NAND_gate(_086_, _088_)
    c22 = XOR_gate(_086_, _088_)
    _090_ = AND_gate(_085_, _089_)
    _l13_ = AND_gate(A[23], B[23])
    _092_ = OR_gate(A[23], B[23])
    _l7_ = XOR_gate(A[23], B[23])
    # --- lock7 ---
    _093_ = XOR_gate(_l7_, P[7])
    c23 = XNOR_gate(_090_, _093_)
    _094_ = NAND_gate(A[24], B[24])
    _095_ = XOR_gate(A[24], B[24])
    # --- lock13 ---
    _091_ = XOR_gate(_l13_, P[13])
    _l19_ = NAND_gate(_090_, _091_)
    # --- lock19 ---
    _096_ = XOR_gate(_l19_, P[19])
    _097_ = AND_gate(_092_, _096_)
    _098_ = NAND_gate(_095_, _097_)
    c24 = XOR_gate(_095_, _097_)
    _099_ = AND_gate(_094_, _098_)
    _l14_ = AND_gate(A[25], B[25])
    _101_ = OR_gate(A[25], B[25])
    _102_ = XOR_gate(A[25], B[25])
    c25 = XNOR_gate(_099_, _102_)
    _103_ = NAND_gate(A[26], B[26])
    _104_ = XOR_gate(A[26], B[26])
    # --- lock14 ---
    _100_ = XOR_gate(_l14_, P[14])
    _105_ = NAND_gate(_099_, _100_)
    _l44_ = NAND_gate(_101_, _105_)
    # --- lock44 ---
    _106_ = XOR_gate(_l44_, P[44])
    _107_ = NAND_gate(_104_, _106_)
    c26 = XOR_gate(_104_, _106_)
    _108_ = AND_gate(_103_, _107_)
    _109_ = NAND_gate(A[27], B[27])
    _110_ = OR_gate(A[27], B[27])
    _l10_ = XOR_gate(A[27], B[27])
    # --- lock10 ---
    _111_ = XOR_gate(_l10_, P[10])
    c27 = XNOR_gate(_108_, _111_)
    _112_ = NAND_gate(A[28], B[28])
    _113_ = XOR_gate(A[28], B[28])
    _l43_ = NAND_gate(_108_, _109_)
    # --- lock43 ---
    _114_ = XOR_gate(_l43_, P[43])
    _l34_ = NAND_gate(_110_, _114_)
    # --- lock34 ---
    _115_ = XOR_gate(_l34_, P[34])
    _116_ = NAND_gate(_113_, _115_)
    c28 = XOR_gate(_113_, _115_)
    _117_ = NAND_gate(_112_, _116_)
    _118_ = NAND_gate(A[29], B[29])
    _l30_ = XNOR_gate(A[29], B[29])
    # --- lock30 ---
    _119_ = XOR_gate(_l30_, P[30])
    _120_ = NAND_gate(_117_, _119_)
    c29 = XOR_gate(_117_, _119_)
    _121_ = NAND_gate(_118_, _120_)
    _l11_ = NAND_gate(A[30], B[30])
    _123_ = XOR_gate(A[30], B[30])
    _124_ = NAND_gate(_121_, _123_)
    _l40_ = XNOR_gate(_121_, _123_)
    # --- lock11 ---
    _122_ = XOR_gate(_l11_, P[11])
    _l23_ = NAND_gate(_122_, _124_)
    _l32_ = XNOR_gate(A[31], B[31])
    # --- lock23 ---
    _125_ = XOR_gate(_l23_, P[23])
    # --- lock32 ---
    _126_ = XOR_gate(_l32_, P[32])
    c31 = XNOR_gate(_125_, _126_)
    _l12_ = XOR_gate(A[0], B[0])
    _l29_ = XOR_gate(_016_, _017_)
    c2  = XOR_gate(_019_, _020_)
    c3  = XOR_gate(_022_, _023_)
    c4  = XOR_gate(_025_, _026_)
    c5  = XOR_gate(_028_, _029_)
    _l17_ = XOR_gate(_010_, _031_)
    _127_ = XNOR_gate(A[7], B[7])
    c7  = XNOR_gate(_033_, _127_)
    _l31_ = XOR_gate(_006_, _035_)
    _128_ = XNOR_gate(A[9], B[9])
    _l41_ = XNOR_gate(_l42_, _128_)
    c10 = XOR_gate(_002_, _039_)
    _129_ = XNOR_gate(A[11], B[11])
    c11 = XNOR_gate(_041_, _129_)
    _l25_ = XOR_gate(_131_, _043_)
    # --- lock12 ---
    c0  = XOR_gate(_l12_, P[12])
    # --- lock17 ---
    c6  = XOR_gate(_l17_, P[17])
    # --- lock22 ---
    c13 = XOR_gate(_l22_, P[22])
    # --- lock25 ---
    c12 = XOR_gate(_l25_, P[25])
    # --- lock29 ---
    c1  = XOR_gate(_l29_, P[29])
    # --- lock31 ---
    c8  = XOR_gate(_l31_, P[31])
    # --- lock41 ---
    c9  = XOR_gate(_l41_, P[41])
    # --- lock40 ---
    c30 = XOR_gate(_l40_, P[40])
    # --- lock45 ---
    c19 = XOR_gate(_l45_, P[45])
    
    # Gom các bit kết quả thành số 32-bit.
    bits = [c0, c1, c2, c3, c4, c5, c6, c7, c8, c9,
            c10, c11, c12, c13, c14, c15, c16, c17, c18, c19,
            c20, c21, c22, c23, c24, c25, c26, c27, c28, c29,
            c30, c31]
    result = BitVecVal(0, 32)
    for i, bit in enumerate(bits):
        result = result | If(bit, BitVecVal(1 << i, 32), BitVecVal(0, 32))
    return result

# Khởi tạo solver và các biến password (48-bit dưới dạng danh sách các Bool)
solver = Solver()
P = [Bool(f"P_{i}") for i in range(48)]

# Thiết lập một số test case: (a, b) sao cho đầu ra của mạch bằng a+b modulo 2^32
import random

num_cases = int(input("so testcase: "))
max_val = int(input("max a,b : "))#2**31 - 1  # Giới hạn trên: a, b < 2**31

test_cases = [(random.randint(0, max_val), random.randint(0, max_val)) for _ in range(num_cases)]

for (a_val, b_val) in test_cases:
    circuit_out = add(a_val, b_val, P)
    expected = (a_val + b_val) & 0xFFFFFFFF
    solver.add(circuit_out == expected)

if solver.check() == sat:
    model = solver.model()
    password_val = 0
    # In ra chuỗi bit của password (bit 0 tới bit 47)
    for i in range(48):
        if is_true(model.evaluate(P[i])):
            password_val |= (1 << i)
            print('1', end='')
        else:
            print('0', end='')
    print('\n')
    print("Found password: 0x{:012X}".format(password_val))
else:
    print("No solution found")

if __name__ == "__main__":
    pass

ta thử với testcase=10 và max_val=1000:
thay password vào chương trình C:
ta thấy kết quả đã gần với a+b==101
tăng số lượng testcase và điều chỉnh max_val thích hợp + chút guessing ta được key:
`0x756E4C30634B`
thay vào chương trình C:
ta thấy kết quả đã chính xác.
Flag: `unL0cK`