采用通用核查指令降低Verilog設計中命題的復雜性
加入技術交流群
命題的作用
一般來說，命題是描述一個特定的設計應該實現何種功能或不應該實現何種功能的語句。這樣的一個描述可以在所有的時間或環(huán)境下為真，或者在設計中的特定行為下有條件地部分為真。命題也可稱為“設計意圖的表述”或“設計工程師的假設”，因為它們對設計的重要特性進行歸檔。最具有價值的命題不僅僅是文檔，它們被動地觀察設計并核查設計的行為是否與設計工程師的期望或假設一致。
作為命題的一個簡單例程，我們可以觀察采用One-Hot編碼的狀態(tài)機。在Verilog語言中沒有任何特殊的編碼方案來識別狀態(tài)寄存器，若一個設計錯誤導致寄存器違反了One-Hot規(guī)則，則沒有內在的機制來核查及報告這種違規(guī)。在這種情況下，采用命題是最適宜的。命題可描述寄存器的行為：它可以是被設計成、打算設計成或者被假設具有One-Hot編碼的多種行為。這個命題既可是個注釋并僅進行純粹的信息描述，也可以是一個主動的命令,對One-Hot規(guī)則進行連續(xù)地核查。
命題的例程包括：
一個Verilog實例描述是并行的，兩個項目永遠不會同時為真；
一個狀態(tài)機不會進行非法行為轉換；
存儲器要從經過初始化的地址讀取信息；
接口上的兩個信號要遵循請求-確認握手協議。
在所有的這些例程中，設計工程師企圖匹配命題定義的行為來實現邏輯，但有時設計工程師會出錯，而命題在這時則提供了一種交叉核查的方法；當設計工程師設計出來的行為與命題規(guī)定的行為不符時，命題就會發(fā)出報警。若在Verilog仿真時出現違反命題的情況，人們就非常希望能核查并報告這種違反命題的情況。
除了仿真之外，命題也是形式或半形式驗證工具要達到的驗證目標。這些工具構造基于形式的數學模型，并采用推理技術來證明或反證設計工程師所期望達到的電路行為的特性。
若驗證工具發(fā)現了一種可以違反電路特性的方法，那么也就發(fā)現了電路設計中的某種缺陷。如果驗證工具能夠證明無法違反電路屬性，那么就得到了有價值的驗證信息。
形式或半形式驗證工具能夠證明兩個Verilog例程項目不能同時評估，或沒有辦法讓狀態(tài)機進行非法行為轉換。工程師非常希望形式驗證工具的目標特性與仿真中使用的命題相匹配。這使命題具體化并在利用形式驗證方法之前的仿真過程中排除故障。進一步來說，如果仿真測試套件中包含某種違反命題的測試，則表明存在設計缺陷，要在進行形式的分析前改正這種缺陷。
設計中的命題是“白盒”驗證的一個極好的實例，因為它們能夠將設計所期望的的內部行為具體化而不僅僅定義從設計輸入到輸出的端到端行為。在許多場合，包括上述幾個實例，命題直接映射到內部設計結構，如狀態(tài)機和存儲器。
除了核查表示設計缺陷的問題之外，對電路內部結構的命題提高了整個設計的可觀測性和設計行為的能見度。對于一個大型設計的輸出，人們不容易核查到深藏在電路設計內部的設計缺陷的作用，并且診斷及改正這種缺陷也非常耗時。最好在缺陷源頭或接近源頭處核查到缺陷，這些地方往往就是內部設計結構命題所報告的設計違規(guī)之處。
基本Verilog命題
在Verilog設計中給定一個命題的最基本方法是加入一條注釋。例如考慮前面討論過的One-Hot狀態(tài)寄存器。下列的代碼表示，在代碼文件中增加一段注釋以表明總是采取One-Hot編碼方式：
=============
reg [3:0] state_var；
// This state register should always be one_hot；
=============
對于設計工程師來說，將設計的要點在文件中進行注釋是必不可少的，不管注釋是否按可執(zhí)行的命題形式編寫。一個注釋形式的命題記錄了設計工程師的假設，并使另一工程師容易理解設計工程師的意圖。
當然，注釋的不利點也在于它僅僅是一個注釋，在仿真過程中不能自動進行核查。因此，設計工程師有時采用特定的Verilog代碼來核查設計假設并用Verilog “$display”語句來報告所有違規(guī)的設計。通常，設計工程師希望這個代碼在仿真過程中被激活，但實際上不綜合到邏輯關系中。有些設計工程師忽略了這個問題，他們指望邏輯綜合工具來刪除不影響任何模塊輸出的邏輯。
還有一些設計工程師認為，這種方法風險性太大，轉而在命題核查代碼附近采用“synthesis off/on”附注或某些其它形式的條件編譯來確保命題核查代碼不被綜合。附注或許是必需的，它能使其它的RTL分析工具(如代碼覆蓋工具)也能夠忽略核查邏輯。
下面是Verilog代碼中用One-Hot命題來核查邏輯的一個例程。即使這樣一個簡單的命題也會引出若干問題：
============================
reg [3:0] state_var；
.
//synopsys translate_offinteger idx, ones_found；
always @(state_var)
begin
ones_found = 0；
for (idx = 0； idx 4 ； idx = idx + 1)
if (state_var[idx] === 1'b1)
ones_found = ones_found + 1；
if (ones_found != 1)
$display(one_hot violation at %d,$time)；
end
//synopsys translate_on
==============================
工程師在這個模塊中增加了兩個新變量(ones_found和idx)來支持核查邏輯。核查與設計緊密鏈接。
在本例中，若設計工程師要將“state_var”寄存器改名，那么核查邏輯也要做若干相應的變化。對更加復雜的命題核查而言，這種由RTL代碼變化引起的波動效應的后果很嚴重，因為這種命題核查需要有幾十甚至上百行Verilog代碼。
這個簡單的例程忽略了許多細節(jié)。例如，它核查的僅僅是1'b1位，而不管其它位是1'b0、未知的1'bx還是三態(tài)的1'bz。若設計工程師要報告“state_var”值(4'b0x10)的違規(guī)情況，那就需要更多的核查邏輯。在復位脈沖附近，需要特別處理，因為“state_var”值為4'b0000時就會超出復位范圍，這時只有在第一個時鐘后開始調出One-Hot值。頻繁出現的情況是，看上去一個簡單的命題核查實際上需要占用設計工程師的大量時間。
采用行間Verilog核查邏輯不需要驗證復用。設計工程師可以結束在編程時進行大規(guī)模程序代碼模塊的剪切和粘貼以完成在不同地方進行的相似核查的編碼。設計假設中的一個變更會導致多處代碼也進行相應的變更。從仿真轉移到形式或半形式驗證時，這種方法就不需驗證復用。通常，形式驗證工具不能驗證混在可綜合或不可綜合Verilog代碼中的僅用“$display”語句表示的特性。
Verilog命題庫
最明顯的給定Verilog命題的方法是采用通用命題核查庫，如最近引入的開放式驗證庫(OVL)。鏈接到特定設計結構的命題通?？梢杂迷赗TL代碼的多處。每當可以采用相同的命題核查時，允許以復用方式調用這些以Verilog模塊形式出現的通用命題。前述的一些復雜問題(如復位附近的特別處理)，一旦是庫中模塊，便能夠解決，并且無論在何處引用，模塊均會發(fā)生作用。
進一步而言，設計工程師可以不必花費很多精力來調整某種類型的RTL變更。當變量名稱改變時，設計工程師只要更改在引用模塊時使用的變量而不用在命題核查代碼中進行多項更改。相對于采用行間Verilog核查邏輯來給定命題的方法來說，新方法的優(yōu)點顯著。
OVL定義了Verilog“監(jiān)測器”模塊庫，它可在設計所用RTL代碼表示命題的適當地方引用。當進行仿真并報告違規(guī)時，OVL監(jiān)測程序執(zhí)行命題核查。OVL的始創(chuàng)還表現在用形式驗證工具可以在模塊庫內方便地設計一個命題。
下面是一個調用OVL模塊核查狀態(tài)寄存器的One-Hot編碼例程。在核查邏輯附近，監(jiān)測器模塊包含有“systhesis translate off/on”附注，設計工程師不需要為了確保核查邏輯不被綜合而采用特別的架構：
=========================
reg [3:0] state_var；
.
assert_one_hot #(0,4) oh1 (.clk(clock),.reset_n(rst_n),
.test_expr(state_var))；
============================
與顯式Verilog代碼相比，采用命題核查庫的優(yōu)點是顯而易見的，但這種方法有其自身內在的局限性。例如，命題的風格使命題不能放在RTL代碼的上下段之間?？紤]到僅當某些條件為真的前提下命題有效(這種有效性需要核查)的情況，若命題條件已經在RTL代碼中表達(如用Verilog if語句進行陳述)，在具體化核查程序時非常重要一點就是利用這些命題條件。
上下條件語句可以存在適用于行間Verilog核查邏輯之中，其中的不同命題核查可以根據周圍的RTL代碼執(zhí)行。
不同的核查可放置在if和else子句之間，僅當相應的if或else條件為真時激活。上下條件語句之間的命題不能采用OVL之類的命題庫來表達。Verilog的句法規(guī)則不允許在RTL的任意點上調用模塊。這通常意味著設計邏輯必須被復制成為核查邏輯的一部分以構建適用的條件。
調用Verilog模塊進行命題核查的另一個局限性在于，這種方法缺乏自變量句法的靈活性。雖然Verilog參數有一定的靈活性(例如變量寬度),但調用Verilog模塊時不允許簡單指定任選自變量的變量數(這種自變量具有缺省的自變量值)。通常來說，在調用的每個Verilog命題庫元素中，每一個自變量必須被明確地指定。
命題庫并不一定用Verilog語言寫成。有些人用C語言或其它的測試平臺語言來寫命題程序，通過PLI接口將命題程序與Verilog程序相連。采用PLI調用允許比用Verilog模塊調用有更靈活的句法。不足之處是PLI自身是一種低效的接口，因而采用這種類型的命題核查通常會增加一些不堪承受的仿真開銷。
核查器指令
在Verilog中，給定命題核查的最靈活方法是使用注釋指令句法從一個命題核查庫中調用相應元素。采用注釋意味著不用“synthesis off/on”附注或其它的特別處理就能使命題對邏輯綜合或其它的工具透明。自由的Verilog模塊調用句法允許采用上下條件命題，命題的自變量數目也具有高度靈活性。
更重要的是，一個智能核查器生成工具組合了核查器指令和RTL設計中的信息來產生核查碼，這種核查碼針對特定的設計度身定制。下面給出的代碼是一個One-Hot命題的例程。任何相關的時鐘、復位甚至要核查的變量均能夠從處于指令同一行的寄存器說明來推斷。一個核查器生成工具能夠讀取包含有這種指令的RTL文件，然后構建適用于對“state_var”進行One-Hot核查的程序，“state_var”將在仿真時工作并報告任何可能的違規(guī)設計。
==========================
reg [3:0] state_var； //assertion one_hot
reg [5:0] state_var； //assertion one_hot
reg [3:0] renamed_state_var； //assertion one_hot
==========================
這段程序表明了采用命題庫的另一優(yōu)點。精選的指令名稱有助于設計程序自行對文件進行歸檔。對于必須閱讀和理解RTL代碼的工程師來說，采用一個名為One_Hot的命題較之行間Verilog代碼更易理解。
組合了智能核查器生成工具的核查器指令方法具有強大的功能，它允許核查器程序適應RTL代碼中可能產生的變更。上面顯示的所有三個指令是相互等效的，然而，由于待核查的狀態(tài)寄存器的名稱和寬度可從RTL中推斷，核查器生成工具會產生不同的核查程序。因此，在RTL中進行的一般性更改不需對核查指令作任何的調整。
由于具備上述的優(yōu)點，在研制白盒驗證套件時選擇了核查器指令方法。核查器指令使設計工程師在編寫Verilog RTL代碼時能非常方便地給定命題。0-In公司的通用指令參考了0-In CheckerWare庫，它們包括：
Verilog核查器的數據路徑元素。例如驗證數據在電纜傳輸時沒有發(fā)生數據丟失，或在FIFO或存儲器中沒有發(fā)生數據錯誤；
Verilog 核查器的控制結構。例如驗證仲裁方案是否正確，或狀態(tài)機工作是否正常；
Verilog核查器的接口。例如驗證信號間的多周期時序關系或核查三態(tài)總線是否始終處于被驅動狀態(tài)。
在CheckerWare庫中有五十多個項目的核查器，單個接口核查器被組合來構成CheckerWare監(jiān)測程序，此監(jiān)測程序核查復雜總線的完整協議規(guī)則。CheckerWare監(jiān)測程序可以進行標準接口的正確性核查，所涉及的標準接口包括PCI、PCI-X、UTOPIA、SDRAM及ARM微處理器所用的AMBA總線。
核查指令可以用RTL代碼或獨立的Verilog文件直接調用。核查工具是一個智能核查生成工具，它可從指令周圍的RTL上下條件推斷出盡可能多的信息。若將指令放置在RTL的最佳位置，核查程序就會自動前后調節(jié)并在文件自行調用時增加指令值。
下面的例程說明了如何應用0-In核查指令來自動完成不同的核查，這種核查依據寄存器的配置行為(遞增或遞減)來進行：
==========================
reg [7:0] cnt；
.
if (monotonic_direction === 1'b1) cnt = cnt + 8'h01； //0in overflow
else
cnt = cnt - 8'h01； //0in underflow
==========================
利用0-In核查器，可從Verilog RTL推斷的信息數量非常巨大。例如，CheckerWare庫包括了“data_used”核查，這種核查揭示的是裝入源寄存器的數據在重寫之前至少被一個目標寄存器使用。當0-In核查器讀取如下所示的簡單指令后，就可推斷出所有的目標寄存器及所有相關的選擇條件、加載啟動和可以防止源數據到達目標寄存器的時鐘門。所產生的Verilog核查綜合考慮了所有這些條件，因此指令會自動適應RTL的邏輯變化。0-In核查器也會自動將核查與設計等級相匹配，以使同一指令既能在模塊級也能在系統級的仿真中使用。
====================
reg [7:0] pipe_stage_3； // 0in data_used
====================
所有CheckerWare核查器和監(jiān)測程序可以跟蹤結構覆蓋范圍內的信息，也能夠提供在仿真中表現出的設計結構運用好壞情況的反饋信息。例如，FIFO核查器主張FIFO既不在其空時接受讀操作也不在其滿時接受寫操作。不管仿真測試是否曾經充滿FIFO或在至少增加了一個輸入項后全部耗盡，結構覆蓋分析均會提供報告。如果這兩種情況均沒有發(fā)生，那么FIFO并沒有通過仿真來達到足夠的核查。當驗證工程師在指導測試研發(fā)時，這些結構覆蓋“孔”被證明非常有價值。
最后，所有的0-In指令產生的核查器不僅用于仿真，也用于0-In Search半形式驗證工具。傳統的形式工具如模型核查器也能容易實現0-In核查器。這樣相同的0-In核查指令可以提供用于仿真的命題、形式及半形式驗證并支持文件自動調用的RTL代碼。
雖然Verilog本身不支持命題，但抓住設計意圖和設計工程師的假設的意義是人所共知的。由于降低了給定命題的復雜程度，所有工程師都愿意采用這種經證明有效的白盒驗證工具。目前，在Verilog設計中采用不同的方法表示命題核查。這些方法中最具靈活性的是通用核查指令，它可以接入具有最小規(guī)范說明、適應性強、內容豐富的命題核查庫。
作者：Ramesh Sathianathan
設計驗證經理
0-In設計自動化公司
Tom Anderson
應用工程副總裁
0-In設計自動化公司
評論