跳轉到

08.1 veryl check 靜態檢查#

寫程式的人都知道：錯誤被發現得越早，修正成本越低。這個觀念在硬體界尤其殘酷——RTL 上的小錯誤，到了流片之後就是數萬到數百萬美元的修版費用。veryl check 就是把錯誤攔截在最前端的工具。

veryl check 做什麼#

veryl check 對 Veryl 原始碼執行靜態檢查，在不執行模擬的情況下找出問題。它涵蓋的檢查類別包括：

  • 型別與位寬：logic<8> 與 u32 之間的賦值是否相容、位寬是否匹配。Veryl 的型別系統在這裡發揮主力作用——許多在 Verilog 中靠「隱式擴位」矇混過關的位寬錯誤，在 Veryl 會被明確指出。
  • 未使用訊號與變數：宣告了卻沒讀寫的訊號，往往是介面設計失誤或殘留死碼的徵兆。
  • 未定義與未初始化的使用：引用不存在的識別字、語意錯誤等。
  • 語法與結構檢查：parse 階段就能發現的問題。

檢查背後的技術基礎是 Veryl 編譯前端的完整語意分析：符號表、型別推導、位寬計算。veryl check 就是把這套分析單獨跑一遍並回報診斷，不需要走到轉譯與模擬。

LSP 即時回饋#

veryl check 不只是命令列工具。Veryl 提供 LSP（Language Server Protocol）伺服器，編輯器（VS Code 等）可以即時呼叫同樣的分析引擎，在你打字的同時畫出紅線、浮出錯誤說明。

這個體驗的意義要放在軟體工具史的脈絡看：Rust 的 rust-analyzer、TypeScript 的語言服務，都把「錯誤回饋時間」從「存檔後編譯」壓縮到「打完字那一秒」。回饋越即時，錯誤越難累積。硬體開發者過去要等綜合器或模擬器跑完才知道程式碼有沒有問題，現在變成編輯器內即時提示——工作流的質變。

歷史：EDA lint 產業與錯誤訊息的痛點#

靜態檢查在硬體界有深厚的產業傳統。1990 年代起，專門的 RTL lint 工具成為一門生意：在綜合之前檢查程式碼的潛在問題——位寬不匹配、未驅動訊號、閂鎖器（latch inference）、組合迴圈、clock domain crossing 等。這些工具至今仍是大公司流程中的必要關卡，因為每一項漏掉的問題都可能在流片後變成損失。

但傳統 SV 工具鏈有一個長期痛點：錯誤訊息不易讀。綜合器與模擬器的診斷輸出常常是簡短的代碼加一行描述，位置資訊粗糙，加上語言本身隱式轉換規則複雜，使用者經常要靠搜尋文件或問資深同事才能理解錯在哪裡。這與現代編譯器（clang、rustc）以「把錯誤訊息當產品」的態度形成強烈對比——後者會指出確切位置、解釋原因、甚至建議修法。

Veryl 的診斷設計繼承了這個現代傳統：因為語言的隱式行為被刻意最小化（位寬必須明確、型別必須相容），錯誤訊息可以直白地說「這裡 8 bit 賦給 32 bit，你要不要明確寫出意圖」。語言設計與診斷品質是同一件事的兩面。

常見錯誤案例與解讀#

以下概念性列舉幾類常見的 check 診斷（訊息措辭依版本而定）：

  1. 位寬不匹配：把 logic<8> 的訊號賦給 logic<32>。Verilog 會默默補零，Veryl 會指出來讓你決定：是擴位（寫明轉換）還是接錯線。
  2. 未使用訊號：宣告了 var tmp: logic<8>; 卻從未讀取。可能是忘了驅動，也可能是殘留碼。
  3. latch 風險：always_comb 區塊中某個分支沒有對所有輸出賦值。Verilog 會默默推斷出閂鎖器，Veryl 的檢查會要求你把每個分支寫完整。

這些檢查的共通點是：它們都在攔截「Verilog 沉默、硬體出事」的那一類錯誤。

小結#

veryl check 把 1990 年代以來的 EDA lint 傳統，用現代編譯器診斷的標準重新實作，並透過 LSP 把回饋時間壓到即時。靜態檢查加上好的錯誤訊息，等於把資深工程師的 code review 中最機械化的部分自動化了。下一章看同屬品質管線的格式化工具 veryl fmt。