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