VERIFICATION — FORMAL

Formal Verification:
Formal Verification: พิสูจน์ความถูกต้อง

ENGINEERING

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

Formal Verification (FV) เป็นกระบวนการตรวจสอบความถูกต้องของวงจรดิจิทัล (Logic Design) โดยอาศัยหลักการทางคณิตศาสตร์ (Mathematical Proof) แทนที่จะพึ่งพาการจำลองด้วยข้อมูลสุ่ม (Stimulus-based Simulation) เพียงอย่างเดียว ในขั้นตอน Functional Verification ของการออกแบบ IC, FV ช่วยให้วิศวกรสามารถยืนยันได้ว่า Design ภายใต้เงื่อนไขที่เป็นไปได้ทั้งหมดนั้นสอดคล้องกับ Specification (Property Checking) หรือไม่

ความสำคัญของ FV อยู่ที่ความสามารถในการตรวจจับ Bug ที่ลึกและซับซ้อน ซึ่ง Simulation อาจหาไม่เจอเนื่องจากข้อจำกัดของจำนวน Test Case เช่น ปัญหาในสถานะขอบเขต (Corner cases) หรือ Deadlock ใน State Machine ที่เกิดขึ้นได้ยาก การนำ FV มาใช้ร่วมกับ UVM จะช่วยเพิ่มประสิทธิภาพของ Coverage-Driven Verification ได้อย่างมหาศาล ทำให้ลดความเสี่ยงในการ Re-spin silicon และเพิ่มความมั่นใจในคุณภาพระดับสูง

📍 CAREER ROADMAP CONTEXT

STAGE 03 — FUNCTIONAL VERIFICATION: Verification & Coverage
ตรวจสอบ design ด้วย UVM testbench, coverage-driven verification, constrained-random simulation และ formal verification (property checking)
Tools: Cadence Xcelium, Synopsys VCS, Questa Formal, Jasper Gold
Related: UVM / OVM Testbench · Coverage-Driven Verification · Lint & CDC Checking
Path: IC Design Engineer

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

หัวใจสำคัญของ Formal Verification คือการใช้ Formal Methods เพื่อพิสูจน์คุณสมบัติ (Properties) ของ Design โดยเปลี่ยนโครงสร้างของวงจร (Netlist หรือ RTL) ให้เป็น Model เชิงคณิตศาสตร์ เช่น Boolean Satisfiability (SAT) หรือ Binary Decision Diagrams (BDD) โดยการเขียนเงื่อนไขตรวจสอบผ่านภาษา SVA (SystemVerilog Assertions)

ในเชิงทฤษฎี เราตรวจสอบความถูกต้องผ่านสมการ logic สถานะ $S$ โดยให้ $P$ เป็นคุณสมบัติที่ต้องการพิสูจน์ หากเรามีสมการเปลี่ยนสถานะ $\delta(S, I) = S'$ เมื่อ $I$ คือ Input, Formal Tool จะทำการค้นหาว่ามีลำดับของ $I$ ใดหรือไม่ที่ทำให้เกิดสภาวะ $S$ ที่ละเมิดคุณสมบัติ $P$:

$ \forall I : S_{initial} \xrightarrow{I^*} \neg P $

การใช้ Symbolic Model Checking ช่วยให้สามารถตรวจสอบสถานะที่เป็นไปได้ทั้งหมดโดยไม่ต้องยิง Test Vector จริงๆ ทำให้แก้ปัญหาเรื่อง State Space Explosion ได้ดีขึ้น

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

กระบวนการทำงานเริ่มจากการเตรียม Formal Environment โดยต้องระบุคุณสมบัติผ่าน assert property ใน SVA และตั้งค่า Constraints (assume) เพื่อกำหนดขอบเขตของ Input ที่เป็นไปได้จริง เพื่อป้องกัน False Negative ที่เกิดจากสถานะที่ไม่มีวันเกิดขึ้นใน Hardware จริง

ขั้นตอนปฏิบัติมีดังนี้: 1. Defining Properties: เขียน Assertion ระบุพฤติกรรมที่คาดหวัง 2. Constraint Modeling: จำกัด Input เพื่อลด Search Space 3. Formal Analysis: ใช้ Tool ทำการตรวจสอบ Logic และหา Counter-example หากพบ Bug, Tool จะแสดงรูปคลื่น (Waveform) ที่นำไปสู่ความผิดพลาดนั้น เพื่อให้วิศวกรวิเคราะห์และแก้ไขทันที ซึ่งต่างจากการ debug ใน UVM ที่ต้องหาลำดับเหตุการณ์เอง

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

ความท้าทายหลักในระดับ sub-5nm คือความซับซ้อนของ Design (Complexity) ที่มี Gate count สูงขึ้น ทำให้ State Space ขนาดใหญ่เกินกว่าจะคำนวณได้โดยตรง เทคนิคที่นำมาใช้เพื่อแก้ปัญหานี้คือ Abstraction Techniques เช่น Data Path Reduction หรือ Counter Abstraction เพื่อลดขนาดของ State machine โดยยังคงรักษาความถูกต้องของ Logic ไว้

อีกความท้าทายคือ Formal-based Equivalence Checking (LEC/CEC) ที่ต้องทำในหลายขั้นตอนของ Synthesis/Place & Route เพื่อให้มั่นใจว่าการเปลี่ยนจาก RTL เป็น Gate-level netlist ไม่ทำลายคุณสมบัติเดิม รวมถึงการรับมือกับ Low-power design ที่มี Power gating ทำให้ Formal Tool ต้องเข้าใจพฤติกรรมของ Control Signal ที่เปลี่ยนไปตามโหมดการทำงานของชิป (UPF/CPF awareness)

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

ตลาด EDA Tools สำหรับ Formal Verification มีผู้เล่นหลักที่ถือเป็นมาตรฐานอุตสาหกรรม ได้แก่ Cadence JasperGold ซึ่งเป็นที่ยอมรับอย่างสูงในเรื่องของ Formal Apps ที่ครอบคลุมทั้ง Connectivity, Security และ Verification Plan, รวมถึง Synopsys VC Formal ที่มีความสามารถโดดเด่นในการเชื่อมต่อกับ UVM Testbench (Formal-driven Verification)

นอกจากนี้ยังมี Siemens EDA (Questa Formal) ที่ใช้เทคนิคการพิสูจน์ขั้นสูง เหมาะสำหรับการตรวจสอบความถูกต้องของ RTL ที่มีความซับซ้อนสูง เครื่องมือเหล่านี้ทำงานร่วมกับระบบตรวจสอบ Lint & CDC (Clock Domain Crossing) เพื่อให้แน่ใจว่าทั้ง Logical Integrity และ Structural Integrity ของออกแบบมีความถูกต้องสมบูรณ์ก่อนเข้าสู่กระบวนการ Fabrication

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

ในโรงงานผลิตชิปชั้นนำอย่าง TSMC, Intel และ Samsung การทำ Formal Verification ไม่ได้เป็นเพียงส่วนเสริม แต่เป็นข้อกำหนดบังคับ (Requirement) เพื่อรักษา Yield และลดต้นทุนการออกแบบ โดยเฉพาะในชิป AI Accelerator และ Processor ที่มีความซับซ้อนสูง การปล่อยให้มี Bug เล็ดลอดไปถึงขั้นตอน Mask making จะหมายถึงความสูญเสียหลายล้านดอลลาร์

การประยุกต์ใช้ FV ส่งผลโดยตรงต่อ Supply chain ทั่วโลก เพราะช่วยลดระยะเวลา Time-to-Market ของอุปกรณ์อิเล็กทรอนิกส์ การที่บริษัท Semiconductor สามารถการันตี Zero-bug สำหรับโมดูล critical (เช่น Memory Controller หรือ Interconnect Fabric) ผ่าน Formal proof ทำให้เกิดมาตรฐานความเชื่อถือได้สูง (High-reliability) ในผลิตภัณฑ์รถยนต์ไฟฟ้า (EV) และศูนย์ข้อมูล (Data Center) ทั่วโลก