在操作性 SVA 中擷取時序圖

為了對設計功能進行形式驗證，必須以形式驗證語言擷取受驗證設計 (DUV) 的預期行為。規格文件中經常包含時序圖，這對擷取設計的預期行為是個非常好的起點。但是，以序列範例為基礎的標準形式驗證語言 SVA 和PSL，並未提供直截的構造來擷取時序圖。序列範例的意思是序列延伸正規表示式 (SEREs)。

本文介紹了從時序圖和波形輕鬆衍生屬性所需使用的語言構造，以及這些構造在 Siemens EDA 操作性 SVA 中的實作。

操作性 SVA 簡介

在定義和採用 SVA 標準時，ITL 使用者請求將廣泛公認的標準與 ITL 的易用性結合起來。為了解決這個需求，Siemens EDA 開發出一種稱為操作性 SVA 的 SVA 建模層。操作性 SVA 未使用 SVA 的整套語言構造，而是以一個小型的 SVA 構造資料庫為基礎，稱為「時序圖斷言資料庫」(TiDAL)。TiDAL 基於十多年豐富的 ITL 經驗打造而成，有助於從時序圖編寫斷言，下文將會展示。

使用操作性 SVA 時，使用者不必瞭解 SVA 大部分複雜的層面，只要瞭解表達時間層面所使用的幾個簡單構造。建模層能避開語義方面的陷阱和複雜問題，例如巢套序列、局部變數資料流規則、較強和較弱的語義等等。TiDAL 資料庫由不到 5 頁的標準 SVA 程式碼組成，定義了能將時序圖直接轉錄為 SVA 的構造。圖 1 說明了建模層的概念：VMM 和 OVM 是用於動態驗證的眾所周知的建模層。其大大減輕了使用者以基礎語言 SystemVerilog、SystemC 或 C++ 直接編程的負擔。同樣地，TiDAL 也讓 SVA 變得更容易使用。右下角的窄式中間區塊，表示操作性 SVA 內使用了 SVA 的基本子集。