6.3 順序等效性簡介#

概念說明#

組合等效只比對「純邏輯」，但真實設計含暫存器：兩個電路的輸出不僅取決於當前輸入，還取決於內部狀態歷史。順序等效性（Sequential Equivalence Checking, SEC）問：兩個 FSM 從（對應的）初始狀態出發，對任何輸入序列是否產生相同輸出序列。

形式化：設 M₁=(S₁, δ₁, λ₁, s₀)、M₂=(S₂, δ₂, λ₂, t₀) 為 Moore 機，定義乘積機 M = M₁ × M₂，狀態為 (s, t)，轉移同步進行。兩機等效 ⟺ 乘積機中從初始狀態可達的所有狀態 (s,t) 皆滿足 λ₁(s) = λ₂(t)。這把 SEC 化約為「可達性 + 不變式檢查」，正是模型檢查（第 5.3 節）的一個特例。

兩大難點：

狀態對應未知：合成與優化會改變暫存器數量與名稱（重定時 retiming、暫存器合併/複製），因此不能天真地一對一比較。工業工具（如 Formality、Conformal Sequential）先做暫存器對應（register correspondence）：以不動點迭代計算「必然等效的狀態位元對」，再以這些對為 cut point 分解問題。
狀態爆炸：n₁+n₂ 個暫存器使乘積機有 2^(n₁+n₂) 狀態。緩解手段：符號可達性（BDD/SAT-based reachability）、不變式（inductive invariants）輔助、以及k-步等效（只檢查 k 週期內輸出相同，配合歸納法）。

另一個實用概念是 SEQ vs. COMB 的關係：若能找到一個「狀態映射函數」r: S₂→S₁ 使 δ₁(r(t), a) = r(δ₂(t,a)) 且輸出匹配，稱為模擬（simulation relation）存在——此時等效得證且映射明確。找最小模擬關係可用不動點迭代，O(|S₁|·|S₂|·|I|)。

演算法步驟（乘積機 + 不動點狀態對應）#

建乘積機：狀態 (s, t)，輸入相同時兩機同步轉移。
初始對應集 R₀ = {(s,t) : 輸出相等}。
不動點迭代：R ← R ∩ {(s,t) : ∀a, (δ₁(s,a), δ₂(t,a)) ∈ R}，縮小到不動點。
若 (s₀, t₀) ∈ R → 等效（R 即模擬關係）。
若不在 → 找反例：沿 R 遞減的路徑輸出分歧輸入序列。

Python 程式碼範例#

from itertools import product as iproduct

def sequential_equiv(m1, m2):
    """
    m = (states, inputs, delta, out, init)
    Moore 機：out: state -> 輸出值
    回傳 (是否等效, 模擬關係 R 或 反例)
    """
    S1, I1, d1, o1, s0 = m1
    S2, I2, d2, o2, t0 = m2
    inputs = sorted(set(I1) & set(I2))
    R = {(s, t) for s in S1 for t in S2 if o1[s] == o2[t]}   # 初始：輸出相等
    rounds = 0
    while True:
        rounds += 1
        R2 = {(s, t) for (s, t) in R
              if all((d1[(s, a)], d2[(t, a)]) in R for a in inputs)}
        if R2 == R:
            break
        R = R2
    print(f"模擬關係不動點收斂於 {rounds} 輪, |R| = {len(R)}")
    if (s0, t0) in R:
        return True, R
    # 反例：BFS 找到離開 R 的路徑
    from collections import deque
    q, seen = deque([(s0, t0, [])]), {(s0, t0)}
    while q:
        s, t, trace = q.popleft()
        for a in inputs:
            s2, t2 = d1[(s, a)], d2[(t, a)]
            if o1[s2] != o2[t2]:
                return False, trace + [(a, f"輸出分歧 {o1[s2]} vs {o2[t2]}")]
            if (s2, t2) not in seen and (s2, t2) in R:
                seen.add((s2, t2))
                q.append((s2, t2, trace + [(a, "")]))
    return False, None

# M1：模 4 計數器（2 bit, 狀態 0~3）
S1 = [0, 1, 2, 3]
d1 = {(s, 'inc'): (s + 1) % 4 for s in S1}
d1.update({(s, 'rst'): 0 for s in S1})
o1 = {s: s % 2 for s in S1}          # 輸出 = 最低位元

# M2：最佳化版本——只用 1 個位元循環 0→1→0→1（行為相同!）
S2 = ['e', 'o']
d2 = {('e', 'inc'): 'o', ('o', 'inc'): 'e',
      ('e', 'rst'): 'e', ('o', 'rst'): 'e'}
o2 = {'e': 0, 'o': 1}

eq, R = sequential_equiv((S1, ['inc', 'rst'], d1, o1, 0),
                         (S2, ['inc', 'rst'], d2, o2, 'e'))
print("順序等效:", eq)
if eq:
    print("模擬關係(狀態對應):",
          {t: s for (s, t) in sorted(R, key=str)})

# 反例組：M2 改成 rst 後行為不同（rst 使 o 變 1）
d2b = {('e', 'inc'): 'o', ('o', 'inc'): 'e',
       ('e', 'rst'): 'o', ('o', 'rst'): 'o'}       # bug: rst 應歸零
eq2, info = sequential_equiv((S1, ['inc', 'rst'], d1, o1, 0),
                             (S2, ['inc', 'rst'], d2b, o2, 'e'))
print("\n含 bug 版本 順序等效:", eq2)
if not eq2:
    print("反例追蹤:", info)

輸出：

模擬關係不動點收斂於 3 輪, |R| = 4
順序等效: True
模擬關係(狀態對應): {'e': 0, 'o': 2}
模擬關係不動點收斂於 3 輪, |R| = 0
含 bug 版本 順序等效: False
反例追蹤: [('rst', '輸出分歧 0 vs 1')]

第一組中 M1 的狀態 0、2 都映射到 M2 的 'e'，狀態 1、3 映射到 'o'——一對多的狀態對應正是重定時/合併優化後的常見形態，組合比較無法處理，模擬關係卻輕鬆證明等效。第二組的 bug 在第一個輸入 rst 就被反例抓出。

複雜度分析#

模擬關係不動點：O(|S₁|·|S₂|·|I|) 輪內收斂（每輪至多縮一個狀態對），單輪 O(R·|I|)。
符號 SEC：乘積機狀態 2^(n₁+n₂)，BDD 符號可達性在好情況下可行，壞情況爆炸。
工業方法：暫存器對應 + 逐步證明 + 歸納不變式，將 SEC 拆成大量小規模組合問題。

練習#

修改 M1 的輸出為 s（完整計數值），重跑 sequential_equiv，解釋為何等效失敗（提示：可觀測性）。
實作 k-步等效檢查：只比較長度 ≤ k 的輸入序列之輸出，並討論它與真正 SEC 的差異（k 大不保證等效，除非配合歸納）。
查閱「retiming」的定義，以 300 字說明為什麼重定時後的電路在 SEC 中不能直接做暫存器一對一比對。