SEMICONDUCTOR — DEEP DIVE

Equivalence Checking:
Equivalence Checking

ENGINEERING

01 บทนำ: Eqcheck คืออะไร

Equivalence Checking (EqCheck) หรือที่มักเรียกกันว่า Formal Verification (FV) เป็นขั้นตอนวิกฤตในกระบวนการ IC Design เพื่อยืนยันว่าการเปลี่ยนผ่านทางสถานะของ Design จากระดับหนึ่งไปยังอีกระดับหนึ่ง (เช่น RTL ไปยัง Gate-level netlist) นั้นยังคงความถูกต้องเชิงตรรกะ (Logical Equivalence) ไว้โดยไม่มีการเปลี่ยนแปลงฟังก์ชันการทำงาน

ในยุคที่การออกแบบมีความซับซ้อนสูงและมีจำนวน Gate หลายพันล้านตัว การพึ่งพาเพียง Simulation อาจไม่เพียงพอที่จะตรวจหาข้อผิดพลาดที่ซ่อนอยู่ (Corner cases) ได้ทั้งหมด EqCheck จึงเข้ามาทำหน้าที่เปรียบเทียบวงจรทั้งสองฝั่งผ่านทางคณิตศาสตร์แบบ Formal เพื่อรับประกันว่า output ของวงจรทั้งสองฝั่งจะตรงกันในทุกๆ input vector ที่เป็นไปได้

📍 CAREER ROADMAP CONTEXT

STAGE 04 — SYNTHESIS & STA: Logic Synthesis & Static Timing Analysis
แปลง RTL เป็น gate-level netlist ด้วย Design Compiler กำหนด SDC constraints, วิเคราะห์ timing path, fix hold/setup violations, clock gating
Tools: Synopsys Design Compiler / Genus, PrimeTime, Formality
Related: Logic Synthesis (DC/Genus) · SDC Constraints · Static Timing Analysis
Path: IC Design Engineer

02 หลักการพื้นฐาน

หัวใจสำคัญของ EqCheck คือการแปลง Logic Circuit ให้เป็น Boolean Satisfiability (SAT) หรือ Binary Decision Diagrams (BDD) เพื่อสร้างสมการเปรียบเทียบระหว่างฟังก์ชัน $F$ ของ RTL และ $G$ ของ Netlist โดยเราต้องตรวจสอบว่า $F \oplus G = 0$ (XOR operation) สำหรับทุกอินพุตที่เป็นไปได้

ในเชิงทฤษฎี EqCheck จะใช้หลักการเปรียบเทียบในลักษณะของ Point-to-Point Comparison โดยเริ่มจากการระบุ Compare Points ซึ่งมักจะเป็น Primary Inputs, Primary Outputs, Register (DFF) boundaries และ Black-box pins โดยเครื่องมือจะทำการพิสูจน์ว่าในทุกๆ สภาวะ $S_n$ สถานะถัดไป $S_{n+1}$ ของทั้งสองดีไซน์มีความสอดคล้องกันภายใต้เงื่อนไข $Q_{RTL} = Q_{Netlist}$

03 วิธีการและเทคนิค

กระบวนการ EqCheck มักจะถูกทำหลังจากขั้นตอน Logic Synthesis ด้วย Synopsys Design Compiler (DC) หรือ Genus โดยมีขั้นตอนหลักดังนี้: 1. Setup: โหลดดีไซน์ต้นทาง (Reference) และดีไซน์ปลายทาง (Implementation) 2. Elaboration: เครื่องมือจะทำการแยกแยะโครงสร้างของวงจรให้อยู่ในรูปแบบ Internal Database 3. Mapping: ทำการจับคู่จุดเปรียบเทียบ (Compare Points) เช่น Register หรือ Output Pins ที่สอดคล้องกัน 4. Verification: เครื่องมือจะเริ่มกระบวนการพิสูจน์ (Proof engine) หากพบความไม่สอดคล้อง ระบบจะรายงานเป็น Counter-example เพื่อให้ผู้ออกแบบแก้ไข

เพื่อให้การทำ EqCheck เป็นไปอย่างราบรื่น วิศวกรต้องจัดการกับ Non-equivalent points ที่อาจเกิดขึ้นจากการทำ Clock Gating, Retiming หรือ Physical Optimization ซึ่งต้องมีการตั้งค่า Constrain พิเศษเพื่อบอกให้เครื่องมือเข้าใจว่าโครงสร้างที่ต่างกันนั้นมีความหมายทางตรรกะที่เหมือนกัน

04 เทคนิคขั้นสูง

Challenge in Sub-5nm: การออกแบบระดับ Advanced Node มักมีการทำ Physical-aware Synthesis ที่ซับซ้อน ทำให้เกิดความแตกต่างอย่างมากระหว่าง RTL และ Netlist ส่งผลให้เครื่องมือ EqCheck ทำงานได้ยากขึ้น (State space explosion)

ในเทคโนโลยี sub-5nm ปัญหาเรื่อง Design-for-Test (DFT) logic และ Power gating cells กลายเป็นความท้าทายหลัก เนื่องจากมีการแทรกวงจร Test-mode และ Isolation cells เข้าไป ทำให้การเปรียบเทียบต้องอาศัยการกำหนด Formal Constraints ที่แม่นยำเพื่อไม่ให้เครื่องมือรายงานผลผิดพลาด (False Negative)

เทคนิคขั้นสูงที่ใช้คือการทำ Hierarchical Verification โดยการแบ่งดีไซน์เป็น Block ย่อยๆ เพื่อลดความซับซ้อนในการทำ Proof พร้อมทั้งการใช้ Parallel formal engines เพื่อเร่งกระบวนการพิสูจน์ในระดับ Gate-level ที่มีขนาดใหญ่ขึ้นเรื่อยๆ

05 เครื่องมือและอุปกรณ์

อุตสาหกรรม EDA ครองตลาดโดยผู้เล่นหลักสามรายใหญ่ ได้แก่ Synopsys กับเครื่องมือ Formality ซึ่งเป็นมาตรฐานทองคำในอุตสาหกรรม, Cadence กับ Conformal LEC (Logic Equivalence Checker) และ Siemens EDA (Mentor Graphics) ที่มีเครื่องมือ Formal Verification ที่แข็งแกร่ง

เครื่องมือเหล่านี้ทำงานร่วมกับ Design Compiler/Genus โดยรับค่าไฟล์ Netlist ในรูปแบบ Verilog/SystemVerilog และ SDC Constraints เพื่อนำไปวิเคราะห์ร่วมกับ RTL ต้นฉบับ นอกจากนี้ยังมีการทำ ECO (Engineering Change Order) Equivalence Check เพื่อยืนยันว่าการแก้ปัญหา Timing หรือความผิดพลาดในขั้นตอนท้ายๆ จะไม่กระทบต่อฟังก์ชันหลักของชิป

06 การประยุกต์ใช้ในอุตสาหกรรม

ในโรงงานผลิตชั้นนำอย่าง TSMC, Samsung Foundry และ Intel การทำ Equivalence Checking ถือเป็นขั้นตอนบังคับใน Sign-off flow หากชิปไม่ผ่านการตรวจสอบ EqCheck จะถือว่าดีไซน์นั้นยังไม่พร้อมสำหรับการส่งไปยัง Physical Implementation (Layout/GDSII) เพื่อป้องกันความผิดพลาดที่อาจส่งผลให้เกิด Respin ซึ่งมีมูลค่าความเสียหายสูงถึงหลายล้านดอลลาร์สหรัฐ

ความถูกต้องในระดับ Logic นี้มีผลโดยตรงต่อ Yield และ Time-to-market ของผลิตภัณฑ์ระดับโลก ไม่ว่าจะเป็นชิป CPU สำหรับ Data Center หรือหน่วยประมวลผลในสมาร์ทโฟน การันตีได้ว่าข้อมูลภายในจะถูกประมวลผลอย่างถูกต้องตามดีไซน์ต้นฉบับ ไม่เกิดข้อมูลสูญหายหรือการตีความผิดพลาดอันเนื่องมาจากความผิดพลาดในระดับ Gate-level