SemiMatrix / TOPICS / LOGIC EQUIVALENCE CHECKING (LEC)
FORMAL VERIFICATION — LOGIC EQUIVALENCE

Logic Equivalence Checking (LEC)
Synopsys Formality, Cadence Conformal & Gate-Level Proof

Synopsys Formality / Cadence Conformal BDD & SAT Solver Engines SVF Synthesis Guidance Functional ECO Verification

ในขั้นตอนการแปลงโค้ด RTL ไปเป็น Gate-Level Netlist ผ่านกระบวนการ Logic Synthesis, DFT Scan Insertion, Place & Route (P&R) และ Engineering Change Order (ECO) เครื่องมือสังเคราะห์จะทำการปรับแต่งวงจรนับล้านจุด Logic Equivalence Checking (LEC) คือระเบียบวิธีทางคณิตศาสตร์ที่พิสูจน์ว่าโครงสร้างเน็ตลิสต์หลังการปรับแต่ง ยังมีฟังก์ชันการทำงานเชิงตรรกะเหมือนกับ Golden RTL เดิม 100% โดยไม่ต้องรัน Gate-Level Simulation

📍 CAREER ROADMAP CONTEXT
STAGE 04 — SYNTHESIS & EQUIVALENCE: Logic Equivalence Signoff
รัน LEC เปรียบเทียบ RTL vs Synth Netlist, Synth vs Scan Netlist, และ PnR vs ECO Netlist ด้วย Synopsys Formality หรือ Cadence Conformal พร้อมวิเคราะห์ SVF/VSDC Guidance Files เพื่อรับประกันฟังก์ชันการทำงาน 100%
Industry Tools: Synopsys Formality, Cadence Conformal LEC, Siemens Questa Formal AutoCheck
Related: Logic Synthesis Flow · Formal Property Verification · Place & Route Flow · HDL Sandbox Lab
Role: ASIC Synthesis Engineer / Formal Verification Engineer / Physical Design Lead

01 ทำไมต้องใช้ LEC แทน Gate-Level Simulation?

ในอดีต เมื่อได้เน็ตลิสต์หลังการสังเคราะห์ วิศวกรจะรัน Gate-Level Simulation (GLS) ด้วยเวกเตอร์ทดสอบ แต่วิธีนี้มีข้อจำกัดร้ายแรง 3 ประการ:

  • ความเร็วช้ามาก: การจำลองเน็ตลิสต์ขนาด 100 ล้านเกตช้ากว่าการรัน RTL Simulation ถึง $100\times - 1,000\times$
  • ไม่ครอบคลุม 100%: เวกเตอร์ทดสอบไม่สามารถครอบคลุมทุก Corner-case logic transitions
  • X-Propagation Pessimism: การกระจายตัวของค่าที่ไม่ทราบสถานะ ('X') ในสเต็ปรีเซ็ตทำให้เกิด False Failures

LEC สามารถพิสูจน์ความสมมูลทางตรรกะแบบ Exhaustive 100% ได้ในเวลาเพียงไม่กี่นาทีถึงไม่กี่ชั่วโมง จึงกลายเป็นข้อบังคับในการทำ Signoff ของชิประดับโลก

02 คณิตศาสตร์ BDD, AIG & Boolean SAT Engines

เครื่องมือ LEC ใช้โครงสร้างข้อมูลทางคณิตศาสตร์ชั้นสูง:

MITER CIRCUIT FORMULA FOR EQUIVALENCE PROOF
\text{Miter Output } F_{\text{miter}}(X) = F_{\text{Golden}}(X) \oplus F_{\text{Revised}}(X)
เครื่องมือจะต่อวงจร Golden และ Revised เข้ากับอินพุตเดียวกัน $X$ แล้วนำเอาต์พุตของทั้งสองฝั่งมาผ่านเกต XOR (Miter Gate) จากนั้นสั่งให้ SAT Solver พิสูจน์ว่ามีอินพุต $X$ ใดที่ทำให้ $F_{\text{miter}} = 1$ หรือไม่ หากพิสูจน์ได้ว่า $F_{\text{miter}} \equiv 0$ สำหรับทุก $X$ แสดงว่าวงจรทั้งสอง Equivalent กัน 100%
เทคโนโลยี Solver โครงสร้างข้อมูล (Data Structure) จุดเด่นและการประยุกต์ใช้
Reduced Ordered BDD (ROBDD) กราฟแบบมีทิศทางไร้วงรอบที่มี Canonical Form เปรียบเทียบฟังก์ชันได้รวดเร็วระดับ $O(1)$ หลังสร้างกราฟเสร็จ แต่เสี่ยงต่อปัญหา BDD Memory Explosion ในวงจรคูณเลข (Multipliers)
And-Inverter Graph (AIG) + SAT กราฟที่ประกอบด้วยเกต AND 2 อินพุตและ Inverter เท่านั้น ประหยัดหน่วยความจำมหาศาล สามารถประมวลผลวงจรขนาดหลายร้อยล้านเกตได้อย่างมีประสิทธิภาพสูงสุด

03 สถาปัตยกรรม Compare Points & Logic Cones

อัลกอริทึม LEC จะแบ่งวงจรขนาดใหญ่ออกเป็นชิ้นส่วนย่อยๆ (Logic Cones) โดยกำหนด Compare Points ที่สอดคล้องกัน:

  • Primary Inputs (PI): ขาอินพุตของชิปและอินพุตจาก Black Boxes
  • State Elements: D-Flip-Flops, Latches, และ Memory Interfaces
  • Primary Outputs (PO): ขาเอาต์พุตของชิปและเอาต์พุตสู่ Black Boxes
  • Black Boxes: โมดูลที่ไม่อนุญาตให้สังเคราะห์ (เช่น Hard IP, Analog Blocks, Embedded SRAM Arrays)

04 โฟลว์การตรวจ Golden vs Revised Netlists

กระบวนการรัน Formality / Conformal มี 4 สเต็ปหลัก:

1
Read Designs & Library Setup
โหลดไฟล์ Golden Design (เช่น RTL SystemVerilog), Revised Design (เช่น Gate-Level Netlist .v), และ Target Technology Library (.db / .lib)
2
Load Guidance File (SVF / VSDC)
โหลดไฟล์บันทึกการแปลงของ Synthesis Tool เช่น การเปลี่ยนชื่อรีจิสเตอร์, การยุบสถานะ FSM, หรือการตัดเซลล์ที่ไม่มีโหลด
3
Match & Compare Points Alignment
จับคู่ Compare Points ระหว่าง Golden และ Revised (Matched Points > 99.9%) และรายงานจุด Unmapped Points
4
Verify & Equivalence Proof
รัน Solver Engine เพื่อยืนยันสถานะ SUCCEEDED / EQUIVALENT ในทุก Compare Point

05 การใช้ SVF / Guidance Files ในกระบวนการ Synthesis

ในระหว่างที่ Synopsys Design Compiler หรือ Cadence Genus ทำการสังเคราะห์วงจร มันจะบันทึกการเปลี่ยนแปลงทั้งหมดลงในไฟล์ SVF (Synopsys Verification Format):

  • guide_reg_constant — บันทึกว่ารีจิสเตอร์ตัวใดถูกตัดออกเนื่องจากมีค่าคงที่ '0' หรือ '1'
  • guide_uniquify — บันทึกการเปลี่ยนชื่อโมดูลที่ถูกก็อปปี้ซ้ำใน Hierarchy
  • guide_fsm_reencoding — บันทึกการแปลง State Machine จาก Binary เป็น One-Hot Encoding

06 คู่มือการแก้ไข Non-Equivalence & Unmapped Points

หาก LEC ขึ้นสถานะ VERIFICATION FAILED วิศวกรต้องวิเคราะห์ตามลำดับ:

สาเหตุของข้อผิดพลาด ลักษณะอาการ วิธีการแก้ไข (Resolution)
Missing SVF Guidance เกิด Unmapped Registers นับร้อยตัวเนื่องจากชื่อถูกเปลี่ยนในการสังเคราะห์ ตรวจสอบว่าได้โหลดไฟล์ default.svf ครบถ้วนจาก Synthesis Run ล่าสุด
Scan Chain Inversion หลัง DFT Insertion ขา Scan-Out ส่งผลึกตรรกะกลับหัว (Inverted) สั่งตั้งค่า set_constant test_mode 0 หรือ set_constant scan_enable 0 ใน Revised Container
Clock Gating Logic Integrated Clock Gating (ICG) ทำให้ Data Cone ของ Flip-Flop ดูไม่ตรงกัน เปิดการสนับสนุน Clock Gating set_app_var verification_clock_gate_hold_mode true

07 กระบวนการ Functional ECO Signoff Flow

เมื่อพบ Bug ในช่วงท้ายของโครงการ (Post-PnR) วิศวกรจะแก้บั๊กผ่าน Functional ECO:

  1. แก้ไขโค้ด RTL ในส่วนที่ผิดพลาด → สร้างเป็น New Golden RTL
  2. ใช้เครื่องมือ ECO Synthesis (เช่น Conformal ECO หรือ Formality Auto-ECO) วิเคราะห์ความแตกต่างและสร้าง Patch Logic
  3. นำ Patch Logic ไปต่อเข้ากับ Spare Cells (เซลล์สำรอง) ที่กระจายตัวอยู่ในเลย์เอาต์
  4. รัน LEC เปรียบเทียบ New Golden RTL กับ Post-ECO Netlist เพื่อรับประกันว่า Bug ถูกแก้ไขสมบูรณ์และไม่มีผลข้างเคียง (Zero Regressions)

08 ปฏิบัติการจำลองบน HDL Sandbox Lab

คุณสามารถทดสอบการปรับแต่งวงจรตรรกะและการตรวจสอบความเทียบเท่าของลอจิกเกตได้ในห้องแล็บจำลองของเรา:

HDL & Digital Logic Sandbox

เขียนโค้ด Verilog HDL, ทดสอบโครงสร้างลอจิกเกต และสังเกตพฤติกรรมเอาต์พุตในเบราว์เซอร์

เปิดห้องแล็บ HDL Sandbox →