FUNCTIONAL VERIFICATION — FORMAL METHODS

Formal Verification & Model Checking
Cadence JasperGold, SystemVerilog Assertions (SVA) & SAT Solvers

Cadence JasperGold / Synopsys VC Formal SystemVerilog Assertions (SVA) SAT / SMT Solvers k-Induction Proof

ในขณะที่การจำลองแบบ Dynamic Simulation (UVM) สามารถทดสอบเส้นทางการทำงานได้เพียงเศษเสี้ยวของสถานะทั้งหมด Formal Property Verification (FPV) ใช้ระเบียบวิธีพิสูจน์ทางคณิตศาสตร์ (Mathematical Proof) ในการสำรวจปริภูมิสถานะ (State Space) ทั้งหมด 100% พร้อมกัน เพื่อรับประกันว่าวงจรจะไม่มีบั๊กหรือสภาวะจนมุม (Deadlock) ซ่อนอยู่

📍 CAREER ROADMAP CONTEXT

STAGE 02 — FORMAL VERIFICATION: Formal Property Verification & Equivalence
เขียน SystemVerilog Assertions (SVA), พิสูจน์ Protocol Compliance (AXI5/PCIe), ดักจับ Corner-case Deadlocks, ทำ Connectivity & Security Verification ด้วย Cadence JasperGold หรือ Synopsys VC Formal
Industry Tools: Cadence JasperGold, Synopsys VC Formal, Siemens Questa Formal, OneSpin 360
Related: UVM Dynamic Verification · Logic Equivalence Checking (LEC) · Clock Domain Crossing (CDC) · HDL Sandbox Lab
Role: Formal Verification Engineer / ASIC Signoff Lead / Security Verification Specialist

01 ทำไม Formal Verification จึงเป็น "Holy Grail" ของ Verification?

ในการออกแบบวงจรขนาดกลางที่มี Register เพียง 200 ตัว ปริภูมิสถานะที่เป็นไปได้คือ $2^{200} \approx 1.6 \times 10^{60}$ สถานะ ซึ่งมากกว่าจำนวนอะตอมในโลก การรัน Simulation ด้วยเวกเตอร์สุ่มล้านล้านตัวก็ยังครอบคลุมได้ไม่ถึง $0.000001\%$ ของความเป็นไปได้ทั้งหมด

Formal Verification ไม่จำเป็นต้องใช้ Testbench หรือ Stimulus Generator แต่จะแปลงวงจร RTL และข้อกำหนด (Properties) ให้อยู่ในรูปของสมการตรรกะแบบบูลีน (Boolean Formulas) แล้วใช้ SAT / SMT Solver Engines ในการค้นหาว่ามีกรณีใดในจักรวาลที่ทำให้สมการเป็นเท็จหรือไม่ หาก Solver พิสูจน์ได้ว่าไม่มีกรณีใดผิด จะถือว่าคุณสมบัตินั้น PROVEN 100%

02 คณิตศาสตร์ Model Checking & Boolean SAT Solvers

การทำงานของ Formal Engine แบ่งออกเป็น 2 ทฤษฎีหลัก:

BOOLEAN SATISFIABILITY (SAT) & TRANSITION RELATIONS

\Phi(S_0, S_1, \dots, S_k) = I(S_0) \wedge \left(\bigwedge_{i=0}^{k-1} T(S_i, I_i, S_{i+1})\right) \wedge \neg P(S_k)

เมื่อ $I(S_0)$ คือสถานะเริ่มต้นของวงจร (Initial State), $T(S_i, I_i, S_{i+1})$ คือความสัมพันธ์การเปลี่ยนสถานะของวงจร (Transition Relation จาก RTL), และ $\neg P(S_k)$ คือนิเสธของคุณสมบัติที่ต้องการตรวจสอบ หากเครื่องมือ SAT สามารถหาอินพุต $I_0 \dots I_{k-1}$ ที่ทำให้สมการ $\Phi$ เป็นจริง (Satisfiable) จะได้เวกเตอร์ตัวอย่างข้อผิดพลาด (Counter-Example Waveform หรือ "CEX") ทันที

03 ไวยากรณ์ SystemVerilog Assertions (SVA)

ภาษา SVA คือมาตรฐานสากลในการระบุคุณสมบัติเชิงเวลา (Temporal Properties):

ตัวดำเนินการ SVA (Operator)	ความหมายเชิงเวลา	ตัวอย่างการใช้งาน
`##N` (Cycle Delay)	หน่วงเวลาไปข้างหน้า $N$ คาบสัญญาณนาฬิกา	`req ##2 ack` (เกิด ack หลังจาก req 2 คาบ)
`\|->` (Overlapped Implication)	ถ้า Antecedent เป็นจริง ให้ตรวจสอบ Consequent ในคาบเดียวกันทันที	`valid \|-> ready`
`\|=>` (Non-Overlapped Implication)	ถ้า Antecedent เป็นจริง ให้ตรวจสอบ Consequent ในคาบถัดไป ($+1$ Cycle)	`req \|=> gnt`
`[*N]` (Consecutive Repetition)	เงื่อนไขต้องเป็นจริงต่อเนื่องกัน $N$ คาบติดกัน	`enable [*3] \|=> data_valid`
`[->1]` (Goto Repetition)	รอจนกว่าเงื่อนไขจะเกิดขึ้น 1 ครั้ง ณ คาบใดก็ได้ในอนาคต	`req ##[1:$] ack[->1]`

04 Safety Properties vs Liveness Properties

1. Safety Properties ("Bad thing never happens")

ตรวจสอบว่าระบบจะต้องไม่ก้าวเข้าสู่สถานะอันตรายเด็ดขาด เช่น สัญญาณ Grant 2 ตัวต้องไม่แอคทีฟพร้อมกัน (Mutual Exclusion) หรือ FIFO ต้องไม่เกิด Overflow/Underflow พิสูจน์ได้ง่ายด้วย Finite Bounded Search

2. Liveness Properties ("Good thing eventually happens")

ตรวจสอบว่าระบบจะบรรลุเป้าหมายเสมอ เช่น หากร้องขอ Request จะต้องได้รับ Grant ในที่สุด เพื่อป้องกันปัญหา Livelock / Starvation ตรวจสอบโดยมองหา Infinite Fair Loops

05 Bounded Model Checking (BMC) & $k$-Induction Proof

ในวงจรขนาดใหญ่ การพิสูจน์แบบเต็ม State Space อาจใช้เวลานาน เครื่องมือจึงใช้วิธี $k$-Induction:

Base Step: ตรวจสอบว่าคุณสมบัติ $P$ เป็นจริงในทุกสเต็ปตั้งแต่ $0$ ถึง $k$ จาก Initial State
Induction Step: สมมติว่า $P$ เป็นจริงในสถานะใดๆ ต่อเนื่องกัน $k$ คาบ ($S_m \dots S_{m+k-1}$) แล้วพิสูจน์ว่า $P$ จะต้องเป็นจริงในคาบถัดไป ($S_{m+k}$) เสมอ หากผ่าน จะถือว่าพิสูจน์สมบูรณ์แบบไม่จำกัดความลึก (Unbounded Proof)

06 Cadence JasperGold & Synopsys VC Formal Apps

เครื่องมือ Formal ยุคปัจจุบันมีแอปพลิเคชันเฉพาะทาง (Turnkey Apps):

FPV (Formal Property Verification): การล่าบั๊กเชิงลอจิกและพิสูจน์ RTL สมบูรณ์
JasperGold SEC (Sequential Equivalence): ตรวจเทียบ RTL ดั้งเดิมกับ RTL ที่ถูกปรับปรุง (เช่น Clock Gating, Pipeline Retiming)
JasperGold CC (Connectivity Checking): ตรวจสอบการเชื่อมต่อสายนับหมื่นเส้นใน SoC Top-Level ภายในไม่กี่นาที
CSR (Control & Status Register Verification): พิสูจน์คุณสมบัติ Read/Write/Mask ของรีจิสเตอร์นับพันตัวอัตโนมัติ

07 โค้ดต้นแบบ SVA Protocol Assertions

ตัวอย่างการเขียน Assertions ตรวจสอบบัส AXI4-Stream Handshake Protocol:

              // AXI4-Stream Rule: Once TVALID is asserted, TDATA must remain stable until TREADY
                is high

              property p_axis_data_stability;

                @( posedge aclk )
              disable iff (!aresetn)

                (tvalid && !tready)
              |=> (tvalid && $stable(tdata));

              endproperty

              assert_axis_stability:
              assert property (p_axis_data_stability)

                else $error("[FORMAL ERROR] TDATA changed while TVALID was waiting for TREADY!");

              // Mutual Exclusion Rule: Arbiter must never grant two masters simultaneously

              property p_mutex_grant;

                @( posedge aclk )
              disable iff (!aresetn)

                $onehot0( {gnt_master0, gnt_master1, gnt_master2} );

              endproperty

              assert_mutex_gnt:
              assert property (p_mutex_grant);

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

คุณสามารถเขียนโค้ดวงจรตรรกะและทดลองเพิ่ม Assertions เพื่อสังเกตผลการจำลองได้ในเบราว์เซอร์:

HDL & Digital Logic Sandbox

ทดลองเขียนโค้ด SystemVerilog, ต่อวงจรดิจิทัล, และดู Timing Waveforms ในเครื่องมือจำลองของเรา

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