采用通用核查指令降低Verilog設(shè)計(jì)中命題的復(fù)雜性

命題方法在軟件設(shè)計(jì)中已經(jīng)應(yīng)用了很長(zhǎng)時(shí)間，并已成為許多軟件研發(fā)團(tuán)隊(duì)使用的主流方法，然而，在硬件描述語(yǔ)言Verilog 或 VHDL中采用命題來(lái)進(jìn)行硬件設(shè)計(jì)也不過(guò)最近才開(kāi)始普及。雖然VHDL具備固有的命題結(jié)構(gòu)，但是Verilog卻沒(méi)有。因此采用Verilog語(yǔ)言的設(shè)計(jì)及驗(yàn)證工程師要采用不同的命題方法。本文對(duì)幾種不同的命題方法進(jìn)行了研究，闡述了它們各自的優(yōu)缺點(diǎn)。



命題的作用



一般來(lái)說(shuō)，命題是描述一個(gè)特定的設(shè)計(jì)應(yīng)該實(shí)現(xiàn)何種功能或不應(yīng)該實(shí)現(xiàn)何種功能的語(yǔ)句。這樣的一個(gè)描述可以在所有的時(shí)間或環(huán)境下為真，或者在設(shè)計(jì)中的特定行為下有條件地部分為真。命題也可稱(chēng)為“設(shè)計(jì)意圖的表述”或“設(shè)計(jì)工程師的假設(shè)”，因?yàn)樗鼈儗?duì)設(shè)計(jì)的重要特性進(jìn)行歸檔。最具有價(jià)值的命題不僅僅是文檔，它們被動(dòng)地觀察設(shè)計(jì)并核查設(shè)計(jì)的行為是否與設(shè)計(jì)工程師的期望或假設(shè)一致。



作為命題的一個(gè)簡(jiǎn)單例程，我們可以觀察采用One-Hot編碼的狀態(tài)機(jī)。在Verilog語(yǔ)言中沒(méi)有任何特殊的編碼方案來(lái)識(shí)別狀態(tài)寄存器，若一個(gè)設(shè)計(jì)錯(cuò)誤導(dǎo)致寄存器違反了One-Hot規(guī)則，則沒(méi)有內(nèi)在的機(jī)制來(lái)核查及報(bào)告這種違規(guī)。在這種情況下，采用命題是最適宜的。命題可描述寄存器的行為：它可以是被設(shè)計(jì)成、打算設(shè)計(jì)成或者被假設(shè)具有One-Hot編碼的多種行為。這個(gè)命題既可是個(gè)注釋并僅進(jìn)行純粹的信息描述，也可以是一個(gè)主動(dòng)的命令,對(duì)One-Hot規(guī)則進(jìn)行連續(xù)地核查。



命題的例程包括：



一個(gè)Verilog實(shí)例描述是并行的，兩個(gè)項(xiàng)目永遠(yuǎn)不會(huì)同時(shí)為真；

一個(gè)狀態(tài)機(jī)不會(huì)進(jìn)行非法行為轉(zhuǎn)換；

存儲(chǔ)器要從經(jīng)過(guò)初始化的地址讀取信息；

接口上的兩個(gè)信號(hào)要遵循請(qǐng)求-確認(rèn)握手協(xié)議。



在所有的這些例程中，設(shè)計(jì)工程師企圖匹配命題定義的行為來(lái)實(shí)現(xiàn)邏輯，但有時(shí)設(shè)計(jì)工程師會(huì)出錯(cuò)，而命題在這時(shí)則提供了一種交叉核查的方法；當(dāng)設(shè)計(jì)工程師設(shè)計(jì)出來(lái)的行為與命題規(guī)定的行為不符時(shí)，命題就會(huì)發(fā)出報(bào)警。若在Verilog仿真時(shí)出現(xiàn)違反命題的情況，人們就非常希望能核查并報(bào)告這種違反命題的情況。



除了仿真之外，命題也是形式或半形式驗(yàn)證工具要達(dá)到的驗(yàn)證目標(biāo)。這些工具構(gòu)造基于形式的數(shù)學(xué)模型，并采用推理技術(shù)來(lái)證明或反證設(shè)計(jì)工程師所期望達(dá)到的電路行為的特性。



若驗(yàn)證工具發(fā)現(xiàn)了一種可以違反電路特性的方法，那么也就發(fā)現(xiàn)了電路設(shè)計(jì)中的某種缺陷。如果驗(yàn)證工具能夠證明無(wú)法違反電路屬性，那么就得到了有價(jià)值的驗(yàn)證信息。



形式或半形式驗(yàn)證工具能夠證明兩個(gè)Verilog例程項(xiàng)目不能同時(shí)評(píng)估，或沒(méi)有辦法讓狀態(tài)機(jī)進(jìn)行非法行為轉(zhuǎn)換。工程師非常希望形式驗(yàn)證工具的目標(biāo)特性與仿真中使用的命題相匹配。這使命題具體化并在利用形式驗(yàn)證方法之前的仿真過(guò)程中排除故障。進(jìn)一步來(lái)說(shuō)，如果仿真測(cè)試套件中包含某種違反命題的測(cè)試，則表明存在設(shè)計(jì)缺陷，要在進(jìn)行形式的分析前改正這種缺陷。



設(shè)計(jì)中的命題是“白盒”驗(yàn)證的一個(gè)極好的實(shí)例，因?yàn)樗鼈兡軌驅(qū)⒃O(shè)計(jì)所期望的的內(nèi)部行為具體化而不僅僅定義從設(shè)計(jì)輸入到輸出的端到端行為。在許多場(chǎng)合，包括上述幾個(gè)實(shí)例，命題直接映射到內(nèi)部設(shè)計(jì)結(jié)構(gòu)，如狀態(tài)機(jī)和存儲(chǔ)器。



除了核查表示設(shè)計(jì)缺陷的問(wèn)題之外，對(duì)電路內(nèi)部結(jié)構(gòu)的命題提高了整個(gè)設(shè)計(jì)的可觀測(cè)性和設(shè)計(jì)行為的能見(jiàn)度。對(duì)于一個(gè)大型設(shè)計(jì)的輸出，人們不容易核查到深藏在電路設(shè)計(jì)內(nèi)部的設(shè)計(jì)缺陷的作用，并且診斷及改正這種缺陷也非常耗時(shí)。最好在缺陷源頭或接近源頭處核查到缺陷，這些地方往往就是內(nèi)部設(shè)計(jì)結(jié)構(gòu)命題所報(bào)告的設(shè)計(jì)違規(guī)之處。



基本Verilog命題



在Verilog設(shè)計(jì)中給定一個(gè)命題的最基本方法是加入一條注釋。例如考慮前面討論過(guò)的One-Hot狀態(tài)寄存器。下列的代碼表示，在代碼文件中增加一段注釋以表明總是采取One-Hot編碼方式：



=============


reg [3:0] state_var；


// This state register should always be one_hot；


=============



對(duì)于設(shè)計(jì)工程師來(lái)說(shuō)，將設(shè)計(jì)的要點(diǎn)在文件中進(jìn)行注釋是必不可少的，不管注釋是否按可執(zhí)行的命題形式編寫(xiě)。一個(gè)注釋形式的命題記錄了設(shè)計(jì)工程師的假設(shè)，并使另一工程師容易理解設(shè)計(jì)工程師的意圖。



當(dāng)然，注釋的不利點(diǎn)也在于它僅僅是一個(gè)注釋?zhuān)诜抡孢^(guò)程中不能自動(dòng)進(jìn)行核查。因此，設(shè)計(jì)工程師有時(shí)采用特定的Verilog代碼來(lái)核查設(shè)計(jì)假設(shè)并用Verilog “$display”語(yǔ)句來(lái)報(bào)告所有違規(guī)的設(shè)計(jì)。通常，設(shè)計(jì)工程師希望這個(gè)代碼在仿真過(guò)程中被激活，但實(shí)際上不綜合到邏輯關(guān)系中。有些設(shè)計(jì)工程師忽略了這個(gè)問(wèn)題，他們指望邏輯綜合工具來(lái)刪除不影響任何模塊輸出的邏輯。



還有一些設(shè)計(jì)工程師認(rèn)為，這種方法風(fēng)險(xiǎn)性太大，轉(zhuǎn)而在命題核查代碼附近采用“synthesis off/on”附注或某些其它形式的條件編譯來(lái)確保命題核查代碼不被綜合。附注或許是必需的，它能使其它的RTL分析工具(如代碼覆蓋工具)也能夠忽略核查邏輯。



下面是Verilog代碼中用One-Hot命題來(lái)核查邏輯的一個(gè)例程。即使這樣一個(gè)簡(jiǎn)單的命題也會(huì)引出若干問(wèn)題：



============================

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


==============================



工程師在這個(gè)模塊中增加了兩個(gè)新變量(ones_found和idx)來(lái)支持核查邏輯。核查與設(shè)計(jì)緊密鏈接。



在本例中，若設(shè)計(jì)工程師要將“state_var”寄存器改名，那么核查邏輯也要做若干相應(yīng)的變化。對(duì)更加復(fù)雜的命題核查而言，這種由RTL代碼變化引起的波動(dòng)效應(yīng)的后果很?chē)?yán)重，因?yàn)檫@種命題核查需要有幾十甚至上百行Verilog代碼。



這個(gè)簡(jiǎn)單的例程忽略了許多細(xì)節(jié)。例如，它核查的僅僅是1'b1位，而不管其它位是1'b0、未知的1'bx還是三態(tài)的1'bz。若設(shè)計(jì)工程師要報(bào)告“state_var”值(4'b0x10)的違規(guī)情況，那就需要更多的核查邏輯。在復(fù)位脈沖附近，需要特別處理，因?yàn)?ldquo;state_var”值為4'b0000時(shí)就會(huì)超出復(fù)位范圍，這時(shí)只有在第一個(gè)時(shí)鐘后開(kāi)始調(diào)出One-Hot值。頻繁出現(xiàn)的情況是，看上去一個(gè)簡(jiǎn)單的命題核查實(shí)際上需要占用設(shè)計(jì)工程師的大量時(shí)間。



采用行間Verilog核查邏輯不需要驗(yàn)證復(fù)用。設(shè)計(jì)工程師可以結(jié)束在編程時(shí)進(jìn)行大規(guī)模程序代碼模塊的剪切和粘貼以完成在不同地方進(jìn)行的相似核查的編碼。設(shè)計(jì)假設(shè)中的一個(gè)變更會(huì)導(dǎo)致多處代碼也進(jìn)行相應(yīng)的變更。從仿真轉(zhuǎn)移到形式或半形式驗(yàn)證時(shí)，這種方法就不需驗(yàn)證復(fù)用。通常，形式驗(yàn)證工具不能驗(yàn)證混在可綜合或不可綜合Verilog代碼中的僅用“$display”語(yǔ)句表示的特性。



Verilog命題庫(kù)



最明顯的給定Verilog命題的方法是采用通用命題核查庫(kù)，如最近引入的開(kāi)放式驗(yàn)證庫(kù)(OVL)。鏈接到特定設(shè)計(jì)結(jié)構(gòu)的命題通?？梢杂迷赗TL代碼的多處。每當(dāng)可以采用相同的命題核查時(shí)，允許以復(fù)用方式調(diào)用這些以Verilog模塊形式出現(xiàn)的通用命題。前述的一些復(fù)雜問(wèn)題(如復(fù)位附近的特別處理)，一旦是庫(kù)中模塊，便能夠解決，并且無(wú)論在何處引用，模塊均會(huì)發(fā)生作用。



進(jìn)一步而言，設(shè)計(jì)工程師可以不必花費(fèi)很多精力來(lái)調(diào)整某種類(lèi)型的RTL變更。當(dāng)變量名稱(chēng)改變時(shí)，設(shè)計(jì)工程師只要更改在引用模塊時(shí)使用的變量而不用在命題核查代碼中進(jìn)行多項(xiàng)更改。相對(duì)于采用行間Verilog核查邏輯來(lái)給定命題的方法來(lái)說(shuō)，新方法的優(yōu)點(diǎn)顯著。



OVL定義了Verilog“監(jiān)測(cè)器”模塊庫(kù)，它可在設(shè)計(jì)所用RTL代碼表示命題的適當(dāng)?shù)胤揭?。?dāng)進(jìn)行仿真并報(bào)告違規(guī)時(shí)，OVL監(jiān)測(cè)程序執(zhí)行命題核查。OVL的始創(chuàng)還表現(xiàn)在用形式驗(yàn)證工具可以在模塊庫(kù)內(nèi)方便地設(shè)計(jì)一個(gè)命題。



下面是一個(gè)調(diào)用OVL模塊核查狀態(tài)寄存器的One-Hot編碼例程。在核查邏輯附近，監(jiān)測(cè)器模塊包含有“systhesis translate off/on”附注，設(shè)計(jì)工程師不需要為了確保核查邏輯不被綜合而采用特別的架構(gòu)：



=========================


reg [3:0] state_var；


.


assert_one_hot #(0,4) oh1 (.clk(clock),.reset_n(rst_n),


.test_expr(state_var))；


============================



與顯式Verilog代碼相比，采用命題核查庫(kù)的優(yōu)點(diǎn)是顯而易見(jiàn)的，但這種方法有其自身內(nèi)在的局限性。例如，命題的風(fēng)格使命題不能放在RTL代碼的上下段之間?？紤]到僅當(dāng)某些條件為真的前提下命題有效(這種有效性需要核查)的情況，若命題條件已經(jīng)在RTL代碼中表達(dá)(如用Verilog if語(yǔ)句進(jìn)行陳述)，在具體化核查程序時(shí)非常重要一點(diǎn)就是利用這些命題條件。



上下條件語(yǔ)句可以存在適用于行間Verilog核查邏輯之中，其中的不同命題核查可以根據(jù)周?chē)腞TL代碼執(zhí)行。



不同的核查可放置在if和else子句之間，僅當(dāng)相應(yīng)的if或else條件為真時(shí)激活。上下條件語(yǔ)句之間的命題不能采用OVL之類(lèi)的命題庫(kù)來(lái)表達(dá)。Verilog的句法規(guī)則不允許在RTL的任意點(diǎn)上調(diào)用模塊。這通常意味著設(shè)計(jì)邏輯必須被復(fù)制成為核查邏輯的一部分以構(gòu)建適用的條件。



調(diào)用Verilog模塊進(jìn)行命題核查的另一個(gè)局限性在于，這種方法缺乏自變量句法的靈活性。雖然Verilog參數(shù)有一定的靈活性(例如變量寬度),但調(diào)用Verilog模塊時(shí)不允許簡(jiǎn)單指定任選自變量的變量數(shù)(這種自變量具有缺省的自變量值)。通常來(lái)說(shuō)，在調(diào)用的每個(gè)Verilog命題庫(kù)元素中，每一個(gè)自變量必須被明確地指定。



命題庫(kù)并不一定用Verilog語(yǔ)言寫(xiě)成。有些人用C語(yǔ)言或其它的測(cè)試平臺(tái)語(yǔ)言來(lái)寫(xiě)命題程序，通過(guò)PLI接口將命題程序與Verilog程序相連。采用PLI調(diào)用允許比用Verilog模塊調(diào)用有更靈活的句法。不足之處是PLI自身是一種低效的接口，因而采用這種類(lèi)型的命題核查通常會(huì)增加一些不堪承受的仿真開(kāi)銷(xiāo)。



核查器指令



在Verilog中，給定命題核查的最靈活方法是使用注釋指令句法從一個(gè)命題核查庫(kù)中調(diào)用相應(yīng)元素。采用注釋意味著不用“synthesis off/on”附注或其它的特別處理就能使命題對(duì)邏輯綜合或其它的工具透明。自由的Verilog模塊調(diào)用句法允許采用上下條件命題，命題的自變量數(shù)目也具有高度靈活性。



更重要的是，一個(gè)智能核查器生成工具組合了核查器指令和RTL設(shè)計(jì)中的信息來(lái)產(chǎn)生核查碼，這種核查碼針對(duì)特定的設(shè)計(jì)度身定制。下面給出的代碼是一個(gè)One-Hot命題的例程。任何相關(guān)的時(shí)鐘、復(fù)位甚至要核查的變量均能夠從處于指令同一行的寄存器說(shuō)明來(lái)推斷。一個(gè)核查器生成工具能夠讀取包含有這種指令的RTL文件，然后構(gòu)建適用于對(duì)“state_var”進(jìn)行One-Hot核查的程序，“state_var”將在仿真時(shí)工作并報(bào)告任何可能的違規(guī)設(shè)計(jì)。



==========================


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


==========================



這段程序表明了采用命題庫(kù)的另一優(yōu)點(diǎn)。精選的指令名稱(chēng)有助于設(shè)計(jì)程序自行對(duì)文件進(jìn)行歸檔。對(duì)于必須閱讀和理解RTL代碼的工程師來(lái)說(shuō)，采用一個(gè)名為One_Hot的命題較之行間Verilog代碼更易理解。



組合了智能核查器生成工具的核查器指令方法具有強(qiáng)大的功能，它允許核查器程序適應(yīng)RTL代碼中可能產(chǎn)生的變更。上面顯示的所有三個(gè)指令是相互等效的，然而，由于待核查的狀態(tài)寄存器的名稱(chēng)和寬度可從RTL中推斷，核查器生成工具會(huì)產(chǎn)生不同的核查程序。因此，在RTL中進(jìn)行的一般性更改不需對(duì)核查指令作任何的調(diào)整。



由于具備上述的優(yōu)點(diǎn)，在研制白盒驗(yàn)證套件時(shí)選擇了核查器指令方法。核查器指令使設(shè)計(jì)工程師在編寫(xiě)Verilog RTL代碼時(shí)能非常方便地給定命題。0-In公司的通用指令參考了0-In CheckerWare庫(kù)，它們包括：



Verilog核查器的數(shù)據(jù)路徑元素。例如驗(yàn)證數(shù)據(jù)在電纜傳輸時(shí)沒(méi)有發(fā)生數(shù)據(jù)丟失，或在FIFO或存儲(chǔ)器中沒(méi)有發(fā)生數(shù)據(jù)錯(cuò)誤；

Verilog 核查器的控制結(jié)構(gòu)。例如驗(yàn)證仲裁方案是否正確，或狀態(tài)機(jī)工作是否正常；

Verilog核查器的接口。例如驗(yàn)證信號(hào)間的多周期時(shí)序關(guān)系或核查三態(tài)總線是否始終處于被驅(qū)動(dòng)狀態(tài)。



在CheckerWare庫(kù)中有五十多個(gè)項(xiàng)目的核查器，單個(gè)接口核查器被組合來(lái)構(gòu)成CheckerWare監(jiān)測(cè)程序，此監(jiān)測(cè)程序核查復(fù)雜總線的完整協(xié)議規(guī)則。CheckerWare監(jiān)測(cè)程序可以進(jìn)行標(biāo)準(zhǔn)接口的正確性核查，所涉及的標(biāo)準(zhǔn)接口包括PCI、PCI-X、UTOPIA、SDRAM及ARM微處理器所用的AMBA總線。



核查指令可以用RTL代碼或獨(dú)立的Verilog文件直接調(diào)用。核查工具是一個(gè)智能核查生成工具，它可從指令周?chē)腞TL上下條件推斷出盡可能多的信息。若將指令放置在RTL的最佳位置，核查程序就會(huì)自動(dòng)前后調(diào)節(jié)并在文件自行調(diào)用時(shí)增加指令值。



下面的例程說(shuō)明了如何應(yīng)用0-In核查指令來(lái)自動(dòng)完成不同的核查，這種核查依據(jù)寄存器的配置行為(遞增或遞減)來(lái)進(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庫(kù)包括了“data_used”核查，這種核查揭示的是裝入源寄存器的數(shù)據(jù)在重寫(xiě)之前至少被一個(gè)目標(biāo)寄存器使用。當(dāng)0-In核查器讀取如下所示的簡(jiǎn)單指令后，就可推斷出所有的目標(biāo)寄存器及所有相關(guān)的選擇條件、加載啟動(dòng)和可以防止源數(shù)據(jù)到達(dá)目標(biāo)寄存器的時(shí)鐘門(mén)。所產(chǎn)生的Verilog核查綜合考慮了所有這些條件，因此指令會(huì)自動(dòng)適應(yīng)RTL的邏輯變化。0-In核查器也會(huì)自動(dòng)將核查與設(shè)計(jì)等級(jí)相匹配，以使同一指令既能在模塊級(jí)也能在系統(tǒng)級(jí)的仿真中使用。



====================


reg [7:0] pipe_stage_3； // 0in data_used


====================



所有CheckerWare核查器和監(jiān)測(cè)程序可以跟蹤結(jié)構(gòu)覆蓋范圍內(nèi)的信息，也能夠提供在仿真中表現(xiàn)出的設(shè)計(jì)結(jié)構(gòu)運(yùn)用好壞情況的反饋信息。例如，F(xiàn)IFO核查器主張F(tuán)IFO既不在其空時(shí)接受讀操作也不在其滿時(shí)接受寫(xiě)操作。不管仿真測(cè)試是否曾經(jīng)充滿FIFO或在至少增加了一個(gè)輸入項(xiàng)后全部耗盡，結(jié)構(gòu)覆蓋分析均會(huì)提供報(bào)告。如果這兩種情況均沒(méi)有發(fā)生，那么FIFO并沒(méi)有通過(guò)仿真來(lái)達(dá)到足夠的核查。當(dāng)驗(yàn)證工程師在指導(dǎo)測(cè)試研發(fā)時(shí)，這些結(jié)構(gòu)覆蓋“孔”被證明非常有價(jià)值。



最后，所有的0-In指令產(chǎn)生的核查器不僅用于仿真，也用于0-In Search半形式驗(yàn)證工具。傳統(tǒng)的形式工具如模型核查器也能容易實(shí)現(xiàn)0-In核查器。這樣相同的0-In核查指令可以提供用于仿真的命題、形式及半形式驗(yàn)證并支持文件自動(dòng)調(diào)用的RTL代碼。



雖然Verilog本身不支持命題，但抓住設(shè)計(jì)意圖和設(shè)計(jì)工程師的假設(shè)的意義是人所共知的。由于降低了給定命題的復(fù)雜程度，所有工程師都愿意采用這種經(jīng)證明有效的白盒驗(yàn)證工具。目前，在Verilog設(shè)計(jì)中采用不同的方法表示命題核查。這些方法中最具靈活性的是通用核查指令，它可以接入具有最小規(guī)范說(shuō)明、適應(yīng)性強(qiáng)、內(nèi)容豐富的命題核查庫(kù)。



作者：Ramesh Sathianathan


設(shè)計(jì)驗(yàn)證經(jīng)理


0-In設(shè)計(jì)自動(dòng)化公司



Tom Anderson


應(yīng)用工程副總裁


0-In設(shè)計(jì)自動(dòng)化公司