# SOCV 全範圍總複習筆記（講義 0 \~ 13-2） BDD: https://nicze.de/philipp/bdds/ SAT Solver: https://www.msoos.org/cryptominisat/ GV: https://github.com/DVLab-NTU/gv > **使用方式** > > * 建議先 **通讀一遍** 掌握脈絡，再回到薄弱章節細讀投影片。 > * 每個章節均列出 **必懂觀念、常見考點、常踩陷阱**；把這些寫成自己的「錯題筆記」效果最佳。 > * 內文已穿插投影片原文或圖示編號，方便你回到 PDF 定位。 --- ## 0–1 導論：SoC 驗證全貌 ### 必懂觀念 1. **驗證痛點**：狀態空間爆炸、時序交互、隱性並發。 2. **三大驗證支柱**：Simulation（動態）、Equivalence Checking（組合/時序）、Property Checking（形式）。 3. **Safety vs Liveness** – 兩種性質在 CEX 形狀上的根本差別：前者有限路徑即可證偽；後者必須找 **lasso (prefix + loop)** 反例 。 ### 常見考點 * 「AG p = ¬EF ¬p」與「AF p = ¬EG ¬p」能否互換？為何？ * 指出一條 CEX 並標註 prefix/suffix。 ### 陷阱 * 把「最短 CEX = 假設路徑長度 k」誤寫成「證明性質為真」——BMC UNSAT 只代表 ≤ k 無錯 。 --- ## 2 形式化建模與性質描述 ### 必懂觀念 * **Kripke Structure**：〈S,I,T,L〉；T 為完全決定性？ (*考點*) * CTL / LTL 語法語意；「模型檢查」實際做三件事：reachable、trace、proof 。 ### 常見考點 * 給一段 SystemVerilog assertion，翻成 LTL/CTL\*。 * 為何某些組合不變式可「只看 cone-of-fanin」而不需做 reachable？&#x20; --- ## 3–5 BDD 與 BDD-Based Verification ### 必懂觀念 1. **ROBDD**：唯一性 + 無冗測；不同變數排序可致線性↔指數差距 。 2. **變數重排**：Sifting、Window swap；動態觸發時機 。 3. **Reachability with BDD**：前像/後像 + 固定點；Safety 用 μ-fp，Liveness 用 ν-fp（找 loop 集合） 。 ### 常見考點 * 手畫一個 3-input 函數在好／壞排序下的 BDD 大小比較。 * 給 transition relation，用 BDD 寫出 R₀‥Rₙ、判斷性質。 ### 陷阱 * **想用 BDD 硬啃 multiplier**——投影片直接提醒：>200 inputs 風險極高 。 * 忽略「部分 BDD / cut-BDD」可減爆炸，考試常要求舉例。 --- ## 6–7 SAT 與 Advanced SAT Techniques ### 必懂觀念 1. **CNF + Implication**：Unit clause rule；衝突 = 空子句 。 2. **2-Watched-Literal**：O(衝突) 掃描；維護 watching list 。 3. **CDCL**：衝突分析 → UIP 學習 → 非單調回溯；VSIDS 分數衰減 。 ### 常見考點 * 讓你手玩一輪 Watched-Literal 更新或 VSIDS 分數計算。 * 解釋「為何 CNF-SAT 輕鬆做到 2-watch，但電路 SAT 很煩」 。 ### 陷阱 * 把「decision order」和「implication graph」混淆；衝突切割一定經過 1st-UIP。 --- ## 8 Bounded Model Checking (BMC) ### 必懂觀念 * **Φ\_k 公式**：I₀ ∧ ∧\_{t=0}^{k−1} T\_t ∧ ¬p\_k。 * BMC 只保證「最短反例」，無法證明性質；需配 k-induction、simple-path 等延伸 。 ### 常見考點 * 寫出 EF ¬p、AG p 的 BMC CNF 展開。 * 說明 simple-path constraint 內容以及何時爆炸 。 --- ## 9 Unbounded Model Checking & Interpolation ### 必懂觀念 * **k-Step Induction**：Base + Inductive；自環會害失敗。 * **CBA vs PBA**：抽象細化兩路徑；效率比較圖 。 ### 常見考點 * 給一個「真但非 1-inductive」例子，請證明要 k>1。 * 比較 CBA、PBA 在 refinement 次數、SAT 難度。 ### 陷阱 * 以為 interpolation 一定收斂；事實上遇到 non-convex image 仍卡。 --- ## 10 Property-Directed Reachability (IC3 / PDR) ### 必懂觀念 1. **Block–Propagate–Converge** 三環：用 clause 逐格逼近；fixed-point 成立即證明 。 2. **CTI → Generalize → Inductive Clause**：為何要擴大？為何要求 inductive relative to F? ### 常見考點 * 手動示範「碰到 CTI 如何 generalize」。 * 證明 “Ri ⊆ Ri+1” 保證單調性。 ### 陷阱 * 忘了 **cube ⇄ clause** 的轉換方向 。 --- ## 11 SAT 在邏輯合成中的應用（精要） * 了解 SAT 可用於 **不要的線移除 (RAR)**、**冗餘電路偵測**，但期末通常僅測觀念： * Mandatory Assignment, 2-way R-AR 流程。 * 會給一條 wire，要求判斷是否冗餘。 --- ## 12 From SAT to Optimization（Pseudo-Boolean / Max-SAT） * 需知 Adder-Network 編碼與 *arc-consistency* 缺點 。 * 常見考題：把 Σ cᵢxᵢ ≥ k 轉 CNF、說明為何 BCP 推不出隱含值。 --- ## 13-1 Liveness Property Checking ### 必懂觀念 1. **Safety CEX vs Liveness CEX** (lasso) 。 2. **L2S (Biere)**：把 AF p 轉 AG (looped → live)，可沿用 safety checker；優缺點分析 。 3. **Stabilization Property**（GF/FG 原子與其布林組合）在 VeriABC 中的支援 。 ### 常見考點 * 畫出 lasso 形反例並註解 prefix/suffix。 * 解釋 counter-based vs state-recording 兩種 L2S。 ### 陷阱 * 忽略 L2S 會放大模型，導致簡化成本；考題常要比較性能表。 --- ## 13-2 SMT 簡介（課堂重點較輕，仍要會） * **SAT + theory solver** 架構；DPLL(T) 流程；常見理論：EUF、Bit-Vector、Linear Arith. * 基礎考題：給一組約束，說明為何 SAT 而理論 UNSAT。 --- ## 考前衝刺建議 | 時間 | 重點 | 行動 | | --------- | --------- | --------------------------------- | | **T-3 天** | 全章節筆記再掃一次 | 自己講一次每章的 *核心演算法* | | **T-2 天** | 強化演算法細節 | 用白紙寫 **BMC Φ\_k、VSIDS 流程、PDR 三步** | | **T-1 天** | 模擬寫題 | 90 min 把模擬卷 A 題全寫完；檢查時間分配 | | **當天** | 手邊備查 | 開三個視窗：1) 講義索引 2) 自己的公式小抄 3) 搜尋工具 | --- 下面是一份 3 小時／200 分的「SoC Verification（SOCV）」期末模擬考，涵蓋講義 0 \~ 13-2 的所有核心主題。 考題之後直接附上標準解答，方便你對照；真考時可把「解答」部分先摺起來當閉卷練習，再對答案。 --- ## 模擬試題 | 題號 | 題目 | 配分 | | ------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -- | | **A-1** | 比較 **Safety** 與 **Liveness** 性質：<br>1. 分別給出 CTL\* 與 LTL 的典型表示式。<br>2. 說明兩者在 counter-example（CEX）形狀上的差異。 | 20 | | **A-2** | (Combinational) 說明用 **ROBDD** 證明一個不含時序的斷言 `p` 為永真 tautology 的流程；討論變數排序對 BDD 大小的影響及兩種動態重排策略。 | 20 | | **A-3** | 以 SAT-Based **Bounded Model Checking (BMC)** 為例：<br>1. 寫出長度 *k* 的公式 Φ<sub>k</sub>(EF ¬p)。<br>2. 說明 BMC 為何「若 UNSAT 亦不足以證明性質為真」。 | 20 | | **A-4** | 何謂 **k-Step Induction**？為何需要 **Simple-Path Constraint**？舉一個 induction 失敗但性質其實為真的最小例。 | 15 | | **A-5** | 描述 **IC3 / Property-Directed Reachability (PDR)** 的三大迴圈：Block、Propagate、Converge。說明「從 CTI 推廣出 inductive clause」的目的。 | 15 | | **A-6** | 比較 **Counter-example-Based Abstraction (CBA)** 與 **Proof-Based Abstraction (PBA)** 在 refinement 步驟與效能上的優缺點。 | 15 | | **A-7** | 敘述三個經典 **Advanced SAT Techniques**：<br>(a) VSIDS、(b) 2-Watched-Literal BCP、(c) Conflict-Driven Clause Learning。 | 15 | | **A-8** | 針對 **Pseudo-Boolean (PB) 優化**：<br>1. 說明將 PB 條件   ∑ c<sub>i</sub>x<sub>i</sub> ≥ k 轉成 SAT 的 **Adder Network** 方法。<br>2. 何謂 *arc-consistency*？Adder 為何通常不滿足？ | 20 | | **B-1** | 給定下列 2-bit 同步向上計數器 (state = y<sub>1</sub>y<sub>0</sub>)：<br>`verilog<br>y <= (y + 1) % 4;<br>`<br>要求驗證 *property* P：`y ≤ 2`。<br>1. 列出 TR(Y, X) 的布林展開。<br>2. 用 BDD **reachability** 演算法列出 R<sub>0..n</sub>，並判定 P 成立與否。 | 40 | | **B-2** | 下圖為一段多層組合電路，目標是將 **紅色線 wt** 移除。請<br>(a) 列出 wt 的 **Mandatory Assignments** (MA)；<br>(b) 依 **2-Way RAR** / **SatRAR** 找出一條可能的 **alternative wire** 並說明其必為冗餘；<br>(c) 說明移除 wt 後電路功能不變的理由。<br>(附圖見講義 11.23) | 40 | --- ## 參考解答 ### A-1（20 分） 1. **Safety**：`AG p` 或 `¬EF ¬p`； **Liveness**：`AF q` 或 `¬EG ¬q`&#x20; 2. Safety CEX 為**有限**路徑（到達 !p 的 prefix）；Liveness CEX 為「lasso」(prefix + loop)，因為需證明 *永遠* 不會到達 p。 --- ### A-2（20 分） * **流程**：PI → BDD(各 PIs) → 拓樹排序建 BDD → 檢查 PO p 是否約化為常數 1。若非 1，任一路徑至 0 為反例。 * **Ordering**：好順序 ⇒ 節點數線性；壞順序 ⇒ 指數。動態重排<br> (a) **Sifting** (Rudell ’93) (b) **Window/Adjacent Swap**。 --- ### A-3（20 分） 1. Φ<sub>k</sub> ≜ I₀ ∧ ∧<sub>t=0..k-1</sub>T(Xₜ, Xₜ₊₁) ∧ ¬p(X\_k) 2. 若 Φₖ SAT ⇒ 得長度≤k 之 CEX；UNSAT 只說「無長度≤k 之 CEX」，不能保證更長路徑不存在。需增 k 或用歸納/PDR 做 unbounded 證明。 --- ### A-4（15 分） * **k-Step Induction**：Base：I ⇒ P₀...P\_{k-1}；Inductive：P\_t..P\_{t+k-1} ∧ T ⇒ P\_{t+k}. * 若狀態空間存在 **自環** 於 P 區外 (xi → xi)，則一步歸納失敗。加上 **Simple-Path Constraint** (所有中繼狀態互異) 可阻斷此假 CEX。 --- ### A-5（15 分） 1. **Block**：遇 CTI → 以 SAT 衍生 *inductive clause* c 封鎖。 2. **Propagate**：嘗試把 F‐frame 中的 c 前推到前一層。 3. **Converge**：所有 frame 相等 ⇒ 得到不含 CTI 的不變式。 --- ### A-6（15 分） | | CBA | PBA | | | ---------- | ----------- | ----------------------------- | - | | 起始抽象 | 任剪切；易過粗 | 由 BMC refutation 自動擷取 | | | Refinement | 逐條 CTI 延伸 | 用 UNSAT proof 取 *relevant* FF | | | 優點 | 每步增量小 | 一步剔除大量無關訊號 | | | 缺點 | 可能退化為多次無效細化 | 一次細化過大→MC 爆炸 | | --- ### A-7（15 分） * **VSIDS**：衝突時提升涉入變數分數，週期衰減；決策選高分文字。 * **2-Watched-Literal**：每子句僅監兩文字，令 BCP 僅在 watched 變 0 時掃描子句，O(#衝突) 時間。 * **CDCL**：遇衝突由 Implication Graph 回溯切割，學得 UIP 子句並非時間序回溯，可非同步跳層。 --- ### A-8（20 分） 1. 以 n-bit Adder（FA/HA 鏈）計算 S = ∑ cᵢxᵢ，接著以 Comparator 實現 (S ≥ k)。所有閘再經 Tseitin 編碼成 CNF。 2. **Arc-consistency**：若原 PB 條件隱含某文字之值，則在 SAT 編碼中單靠 BCP 也能推出同值。Adder 編碼因總和經過**carry 階層**，局部 0/1 變動難即時傳到最高位，故多數情況非 arc-consistent。 --- ### B-1（40 分） 1. TR(Y,X): `y1' = x1 ⊕ x0 ⊕ y1`, `y0' = x0 ⊕ y0` (⊕ 為 mod-2 加) …… 示意 2. R₀ = {00}; S₁ = {01}; R₁ = {00,01}; S₂ = {10}; R₂ = {00,01,10}; S₃ = {11}; R₃ = 全集。交集 R ∩ ¬P = {11} ≠ ∅ ⇒ P **不成立**。 --- ### B-2（40 分） (a) MA(wt=g6→g7, s-a-1)：{g6=0,g2=0,d=0,g1=0,g4=0,g5=0,g3=1,a=1,b=1,f=1}&#x20; (b) 取 gd=g9 (AND) 之 MA：{g9=1, … , f=0}；觀察 `(g5=1)` 與 `(g5=0)` 矛盾 ⇒ 加線 **g5→g9** (非反相) 為 alternative wire。其冗餘性由 Single-Wire Replacement 定理保證：新增線之 s-a-1/0 均 untestable。 (c) 加入冗餘線後，MA 將 g6 之故障變成 untestable → g6、g7 可安全移除而不改輸出函數。 --- ### 使用建議 * 先計時寫完整份卷，對完解答後再回講義複習被扣分處。 * 真考是 open-everything，但時間仍吃緊，熟記 **核心流程圖、定義、演算法步驟** 最省查找。祝考試順利!