硬件設(shè)計(jì)復(fù)雜度的增加使功能驗(yàn)證成為硬件設(shè)計(jì)方法學(xué)中的重要內(nèi)容，基于斷言技術(shù)的硬件設(shè)計(jì)驗(yàn)證技術(shù)得到越來(lái)越多的應(yīng)用。
作為一種對(duì)設(shè)計(jì)對(duì)象的屬性特性或行為特性的的描述，斷言（聲明，assertion）并不是一個(gè)新的概念。實(shí)際上在軟件設(shè)計(jì)中，斷言已經(jīng)得到了廣泛的應(yīng)用，它可以幫助軟件工程師在軟件開發(fā)及測(cè)試過(guò)程中更早更快的發(fā)現(xiàn)、定位出軟件中可能存在的錯(cuò)誤。例如在JAVA中定義了一種斷言的語(yǔ)法：assert Expression1:Expression2，當(dāng)程序運(yùn)行到這個(gè)斷言，如果Expression1的值為假，則程序會(huì)報(bào)錯(cuò)，并根據(jù)Expression2給出相應(yīng)的錯(cuò)誤信息。許多JAVA的工程師都認(rèn)為斷言是最快也是最有效的調(diào)試方法�，F(xiàn)在同樣的概念越來(lái)越多被引入到硬件及SoC設(shè)計(jì)中。
隨著設(shè)計(jì)復(fù)雜度的增加，如何進(jìn)行有效、充分的硬件設(shè)計(jì)驗(yàn)證，尤其是功能驗(yàn)證已經(jīng)成為硬件設(shè)計(jì)方法學(xué)中重要的內(nèi)容。普遍認(rèn)為在RTL設(shè)計(jì)中超過(guò)70％的工作在進(jìn)行功能驗(yàn)證，同時(shí)有超過(guò)2/3的芯片設(shè)計(jì)需要進(jìn)行重新流片以糾正功能錯(cuò)誤。 本文將說(shuō)明基于斷言的驗(yàn)證（Assertion Based Verification: ABV）是硬件設(shè)計(jì)功能驗(yàn)證的一種有效方法，尤其當(dāng)我們將斷言和形式驗(yàn)證進(jìn)行有機(jī)結(jié)合時(shí)。
硬件設(shè)計(jì)的斷言和基于斷言的驗(yàn)證
A. 硬件設(shè)計(jì)的斷言
每一個(gè)硬件設(shè)計(jì)都包含了設(shè)計(jì)對(duì)象的特性，這些特性保證了硬件能夠正常工作。某些特性屬于電路本身的屬性特性，例如為了避免latch的引入，在case語(yǔ)句的描述中，我們需要進(jìn)行滿足full case特性的描述。另外一些特性屬于電路行為的特征，包括靜態(tài)特性－這些特性在任何時(shí)候都應(yīng)該保持，例如三態(tài)總線在任何時(shí)候只允許最多一個(gè)驅(qū)動(dòng)－和時(shí)序（temporal）特性，即只在給定時(shí)刻（或時(shí)間段內(nèi)）需要滿足的特性。在AMBA AHB的master寫操作中，slave可以在數(shù)據(jù)傳輸周期插入等待狀態(tài)以擴(kuò)展整個(gè)寫周期。在整個(gè)擴(kuò)展周期里，master要保持?jǐn)?shù)據(jù)和控制信號(hào)的穩(wěn)定［1］，如圖1所示。
圖1，在擴(kuò)展整個(gè)寫周期里，master應(yīng)保持?jǐn)?shù)據(jù)和控制信號(hào)穩(wěn)定。
我們?cè)谠O(shè)計(jì)AHB的master時(shí)要遵從這樣的特性，同時(shí)我們?cè)诿枋鯝HB總線的master write測(cè)試激勵(lì)時(shí)也要遵從這樣的特性。在硬件設(shè)計(jì)中，實(shí)現(xiàn)對(duì)這些特性進(jìn)行檢查的方法或?qū)崿F(xiàn)這些方法的描述則被稱為斷言。
設(shè)計(jì)特性可以使用各種語(yǔ)言來(lái)描述，例如Verilog，VHDL，SystemC等。VHDL已經(jīng)包含了對(duì)一些簡(jiǎn)單的特性描述的能力［5］，例如在VHDL語(yǔ)言中可以使用如下的斷言聲明：
assert condition report assertion_message;
這樣在VHDL仿真過(guò)程中，當(dāng)condition的值為“假”的時(shí)候，VHDL仿真器會(huì)給出assertion_message所定義的信息。但某些特性使用硬件或系統(tǒng)描述語(yǔ)言會(huì)非常低效，例如以下的時(shí)序特性：當(dāng) sigA觸發(fā)時(shí)，在5個(gè)時(shí)鐘周期內(nèi)，sigB必須觸發(fā)， 6個(gè)時(shí)鐘周期后，sigA必須復(fù)位。如果使用HDL語(yǔ)言來(lái)描述這個(gè)特性，可能需要一個(gè)狀態(tài)機(jī)來(lái)描述。為了更方便和高效地描述設(shè)計(jì)特性，一種方法是基于當(dāng)前流行的設(shè)計(jì)語(yǔ)言開發(fā)特性描述庫(kù)，Open Verification Library（OVL,www.accellera.org）是其中的一個(gè)例子。
同時(shí)一些專門用于硬件特性描述的語(yǔ)言（Property Specification Language: PSL）和斷言描述的語(yǔ)言已經(jīng)開始被應(yīng)用到實(shí)際設(shè)計(jì)之中。IBM公司開發(fā)的Suger語(yǔ)言被Accellera組織接受成為PSL的標(biāo)準(zhǔn)[2]。Synopsys的OVA則是另一個(gè)經(jīng)過(guò)實(shí)際設(shè)計(jì)驗(yàn)證的斷言描述語(yǔ)言。當(dāng)前設(shè)計(jì)工程師和驗(yàn)證工程師使用不同的語(yǔ)言，其所帶來(lái)的弊端顯而易見(jiàn)，于是人們希望一個(gè)統(tǒng)一的既支持硬件設(shè)計(jì)又支持硬件驗(yàn)證的語(yǔ)言。Accellera組織采用了SystemVerilog[2]。Synopsys則將OVA捐獻(xiàn)到SystemVerilog中作為其用于斷言描述的語(yǔ)言基礎(chǔ)[3]。
B. 基于斷言的驗(yàn)證（ABV：Assertion Based Verification）
基于斷言的驗(yàn)證適用于“白盒”“灰盒”“黑盒”三種驗(yàn)證方法。在“白盒”的情況下，斷言是嵌入在設(shè)計(jì)的實(shí)現(xiàn)代碼里，應(yīng)該由設(shè)計(jì)工程師加入，它和設(shè)計(jì)的實(shí)現(xiàn)緊密相關(guān)。例如下面的例子在設(shè)計(jì)里面加入了斷言：
module fifo(rst,clk,data,rd_wr,full, empty);
input rst,clk, rd_wr;
output full, empty;
// ova ova_mutex(!rst,clk,full,empty);
input [7:0] data;
always @(posedge clk)
..
endmodule
斷言ova_mutex描述了設(shè)計(jì)的屬性：當(dāng)rst為0的時(shí)候，在clk的上升沿，full和empty不可以同時(shí)為1。其中，ova_mutex是定義在ova中的檢查庫(kù)（checker）[4]。支持OVA的驗(yàn)證工具會(huì)動(dòng)態(tài)（通過(guò)仿真技術(shù)）或靜態(tài)（通過(guò)形式驗(yàn)證技術(shù)）分析設(shè)計(jì)描述是否滿足所設(shè)定的設(shè)計(jì)屬性。
在“黑盒”的情況下，斷言與設(shè)計(jì)的具體實(shí)現(xiàn)不相關(guān)，通常是可以在一個(gè)單獨(dú)的斷言描述文件中描述設(shè)計(jì)接口應(yīng)該滿足的特性。一般應(yīng)該由驗(yàn)證工程師給出相應(yīng)的斷言文件。下面以O(shè)VA為例來(lái)說(shuō)明“黑盒”的基于斷言的驗(yàn)證方法。
一個(gè)典型的OVA文件包括：
● 布爾關(guān)系的定義 ：定義一組信號(hào)之間的邏輯關(guān)系；
● 時(shí)序事件的定義 ：定義信號(hào)之間的時(shí)序?qū)傩裕?br> ● 斷言聲明：檢測(cè)上述定義的時(shí)序?qū)傩裕?br> ● 綁定斷言與相應(yīng)的設(shè)計(jì)
下面的一段代碼是一個(gè)典型的OVA文件：
//“unit” 包含了時(shí)鐘、相應(yīng)的邏輯信號(hào)、布爾關(guān)系和時(shí)序事件的定義以及斷言聲明
unit protocol( logic clk, logic valid,
logic [423:0] framein,
logic frame0,logic frame1);
clock posedge clk {
//信號(hào)布爾關(guān)系的定義
bool b_valid0 : (valid) & (framein[7:4] == 4"b0000);
bool b_valid1 : (valid) & (framein[7:4] == 4"b0001);
//時(shí)序事件的定義
event e_frame0 : if ((b_valid0)) then #[0..3] frame0;
event e_frame1 : if ((b_valid1)) then #[0..3] frame1;
}
//設(shè)計(jì)屬性的斷言聲明
assert a_frame0 : check(e_frame0);
assert a_frame1 : check(e_frame1);
endunit
//綁定相應(yīng)的斷言和設(shè)計(jì)
bind module router : protocol uprotocol
(clk,valid,frame_data,frame0,frame1,frame2,frame3);
在上述的OVA定義下，不管模塊“router”具體的實(shí)現(xiàn)細(xì)節(jié)，我們都要求router的信號(hào)滿足OVA文件定義的設(shè)計(jì)屬性。
“灰盒”的情況處于“白盒”和“黑盒”之間，它包含了一定的設(shè)計(jì)實(shí)現(xiàn)的特性。
基于斷言的設(shè)計(jì)驗(yàn)證方法對(duì)設(shè)計(jì)驗(yàn)證方法學(xué)帶來(lái)一些重要的影響，成為先進(jìn)的設(shè)計(jì)驗(yàn)證方法學(xué)的核心：
● 設(shè)計(jì)功能的驗(yàn)證已經(jīng)成為復(fù)雜設(shè)計(jì)中的主要任務(wù)，尤其是復(fù)雜設(shè)計(jì)中不同子模塊之間的接口很容易帶來(lái)潛在的錯(cuò)誤需要驗(yàn)證。斷言語(yǔ)言允許驗(yàn)證工程師在較高的描述層次上對(duì)設(shè)計(jì)屬性進(jìn)行定義，這種定義比硬件描述語(yǔ)言的描述要簡(jiǎn)潔和自然得多。
● 用斷言語(yǔ)言描述的設(shè)計(jì)屬性具有重用性。由于“黑盒”的斷言描述與具體的實(shí)現(xiàn)不相關(guān)，用戶可以方便地在不同的設(shè)計(jì)中重用已有的屬性定義，例如，對(duì)PCI、AMBA等所定義的設(shè)計(jì)屬性描述可在不同的設(shè)計(jì)中用于功能仿真。
● 傳統(tǒng)的驗(yàn)證覆蓋率分析是基于代碼覆蓋的覆蓋率分析，例如，代碼行覆蓋率、條件分支覆蓋率、信號(hào)翻轉(zhuǎn)覆蓋率等。由于斷言定義了設(shè)計(jì)的屬性（或可認(rèn)為是功能），通過(guò)對(duì)斷言的覆蓋率統(tǒng)計(jì)我們可以將傳統(tǒng)的代碼覆蓋率分析提升到功能覆蓋率分析[6]。功能覆蓋率分析對(duì)于設(shè)計(jì)的功能檢查具有更加直接的意義。
傳統(tǒng)上，設(shè)計(jì)功能的驗(yàn)證是基于動(dòng)態(tài)的仿真，通過(guò)觀察仿真結(jié)果發(fā)現(xiàn)、定位設(shè)計(jì)的缺陷。隨著ASIC和SoC設(shè)計(jì)復(fù)雜性的增加，如何有效的構(gòu)建設(shè)計(jì)的測(cè)試激勵(lì)，縮短驗(yàn)證周期為功能驗(yàn)證帶來(lái)了巨大的挑戰(zhàn)。因此高效率的測(cè)試激勵(lì)自動(dòng)生成技術(shù)也是當(dāng)前設(shè)計(jì)驗(yàn)證的熱點(diǎn)技術(shù)之一。測(cè)試激勵(lì)自動(dòng)生成的核心是帶約束的隨機(jī)測(cè)試激勵(lì)自動(dòng)生成。在仿真過(guò)程中，從斷言驗(yàn)證而給出的功能測(cè)試覆蓋信息，我們可以知道哪些功能已經(jīng)經(jīng)過(guò)測(cè)試，根據(jù)這些信息我們可以動(dòng)態(tài)調(diào)整產(chǎn)生隨機(jī)測(cè)試激勵(lì)的約束條件，從而明顯的提高測(cè)試效率。采用上述方法的驗(yàn)證流程如圖 2所示。
圖2，帶約束的隨機(jī)測(cè)試激勵(lì)自動(dòng)生成法的驗(yàn)證流程。
然而基于斷言的驗(yàn)證方法所帶來(lái)的驗(yàn)證方法學(xué)上的巨大變化是將斷言與形式驗(yàn)證技術(shù)相結(jié)合。門級(jí)的形式驗(yàn)證技術(shù)由于大大提高了門級(jí)驗(yàn)證的效率而得到了越來(lái)越多的采用。相對(duì)于動(dòng)態(tài)的仿真技術(shù)，形式驗(yàn)證技術(shù)（門級(jí)的或更高抽象層次上的）具有以下明顯的特點(diǎn)：
● 形式驗(yàn)證技術(shù)不需要測(cè)試激勵(lì)。
● 形式驗(yàn)證技術(shù)可以更加有效地發(fā)現(xiàn)深層的、不易發(fā)現(xiàn)的設(shè)計(jì)缺陷。
在越來(lái)越復(fù)雜的設(shè)計(jì)中，基于斷言的設(shè)計(jì)功能、行為的形式驗(yàn)證技術(shù)得到了廣泛的關(guān)注，并在一些實(shí)際的復(fù)雜設(shè)計(jì)中加以采用。在這種設(shè)計(jì)方法中，通過(guò)形式驗(yàn)證的方法證明設(shè)計(jì)的功能、行為是否滿足斷言所定義的屬性。
但是形式驗(yàn)證技術(shù)，尤其是包括了時(shí)序關(guān)系的形式驗(yàn)證技術(shù)，其計(jì)算復(fù)雜度隨著“狀態(tài)寄存器”的數(shù)目呈指數(shù)關(guān)系增加，限制了形式驗(yàn)證技術(shù)在大規(guī)模設(shè)計(jì)中的應(yīng)用[7]。為了解決這個(gè)問(wèn)題，一種采用 “動(dòng)態(tài)仿真”和形式驗(yàn)證相結(jié)合的“混合形式驗(yàn)證”應(yīng)用了動(dòng)態(tài)仿真和形式驗(yàn)證兩種技術(shù)的特點(diǎn)（圖3）。通過(guò)混合形式驗(yàn)證中的仿真引擎使設(shè)計(jì)“到達(dá)“某一狀態(tài)，然后在此狀態(tài)上應(yīng)用形式驗(yàn)證引擎進(jìn)行形式驗(yàn)證，分析設(shè)計(jì)是否遵從斷言所定義的屬性。然后再應(yīng)用動(dòng)態(tài)仿真的引擎使設(shè)計(jì)到達(dá)一個(gè)新的狀態(tài)，進(jìn)行形式驗(yàn)證。重復(fù)這樣一個(gè)過(guò)程，直到達(dá)到某一設(shè)定的驗(yàn)證目標(biāo)。混合形式驗(yàn)證與傳統(tǒng)的形式驗(yàn)證一樣也不需要測(cè)試激勵(lì)，而且當(dāng)設(shè)計(jì)被證明違反一設(shè)計(jì)屬性時(shí)，混合形式驗(yàn)證還可以給出導(dǎo)致這一設(shè)計(jì)缺陷的測(cè)試激勵(lì)。
圖3，混合形式驗(yàn)證技術(shù)的圖示和采用混合形式驗(yàn)證的設(shè)計(jì)流程。
基于斷言的形式驗(yàn)證改變了傳統(tǒng)的基于動(dòng)態(tài)仿真的硬件驗(yàn)證方法，從而轉(zhuǎn)向了基于設(shè)計(jì)屬性的定義、描述和分析。而且基于斷言的形式驗(yàn)證技術(shù)不依賴于測(cè)試激勵(lì)，能夠有效地提高驗(yàn)證效率。這樣我們就可以從以往的”先設(shè)計(jì)，再驗(yàn)證“的設(shè)計(jì)方法學(xué)轉(zhuǎn)變到”先定義，然后設(shè)計(jì)和驗(yàn)證“的方法學(xué)。這種方法學(xué)已經(jīng)在一些非常復(fù)雜的設(shè)計(jì)中得到應(yīng)用[9][10][11].
OVL、OVA和OVA庫(kù)
OVL是由Accellera（www.accellera.com）推出的采用了斷言思想的驗(yàn)證庫(kù)。它實(shí)際上是使用HDL語(yǔ)言（VHDL和Verilog）定義和實(shí)現(xiàn)了一些非常常用的屬性聲明。用戶可以在設(shè)計(jì)里面直接使用這些屬性聲明來(lái)檢測(cè)設(shè)計(jì)是否遵從了相應(yīng)的設(shè)計(jì)屬性。最新版本提供了以下屬性斷言［8］：
. assert_always . assert_no_underflow . assert_always_on_edge . assert_odd_parity
. assert_change . assert_one_cold . assert_cycle_sequence . assert_one_hot
. assert_decrement . assert_proposition . assert_delta . assert_quiescent_state
. assert_even_parity . assert_range . assert_fifo_index . assert_time
. assert_frame . assert_transition . assert_handshake . assert_unchange
. assert_implication . assert_width . assert_increment . assert_win_change
. assert_never . assert_win_unchanged . assert_next . assert_window
. assert_no_overflow . assert_zero_one_hot . assert_no_transition
例如用戶可以在Verilog設(shè)計(jì)中使用assert_never來(lái)設(shè)定某種情形永不發(fā)生的屬性特性。下面是使用assert_nerver的一個(gè)例子：
module guarded_fifo (clk, reset_n, read, write, data_in, data_out);
input clk, reset_n, read, write;
input [15:0] data_in;
output [15:0] data_out;
wire fifo_full, fifo_empty;
fifo fifo (clk, reset_n, read, write, data_in, data_out, fifo_full, fifo_empty);
assert_never #(0, 0, “Fifo overflow”) fifo_overflow (clk, reset_n, fifo_full && write);
assert_never #(0, 0, “Fifo underflow”) fifo_underflow (clk, reset_n, fifo_empty && read);
endmodule
對(duì)于更復(fù)雜的屬性定義，OVL的用戶可能需要將多個(gè)屬性聲明配合使用。
為了更有效的進(jìn)行設(shè)計(jì)屬性描述，一些專門的屬性描述語(yǔ)言被開發(fā)出來(lái)。OpenVera Assertion（OVA）是被廣泛使用的一種斷言描述語(yǔ)言。OpenVera(www.openvera.org)是一個(gè)開放的用于硬件測(cè)試激勵(lì)自動(dòng)生成的語(yǔ)言。在 OpenVera的基礎(chǔ)上，Synopsys和Intel一起將Intel的斷言描述語(yǔ)言ForSpec融合到OpenVera中并提出了新的斷言描述語(yǔ)言O(shè)penVera Assertion[3]。下面簡(jiǎn)要的介紹一下OVA以及在OVA中定義的設(shè)計(jì)屬性庫(kù)。
像上面OVA的例子中看到的一樣，OVA采用一種層次化的結(jié)構(gòu)來(lái)對(duì)設(shè)計(jì)對(duì)象的屬性進(jìn)行描述。從底到上，這些層次依次是：布爾表達(dá)式、事件表達(dá)式、斷言聲明表達(dá)式、以及由上述表達(dá)式所構(gòu)成的一個(gè)設(shè)計(jì)屬性描述單元。最后，設(shè)計(jì)屬性描述單元綁定到一個(gè)設(shè)計(jì)模塊或設(shè)計(jì)模塊的一個(gè)例化。
· 布爾表達(dá)式：布爾表達(dá)式用來(lái)描述一組信號(hào)之間的邏輯關(guān)系。
· 事件表達(dá)式：事件表達(dá)式用來(lái)描述一組信號(hào)（設(shè)計(jì)信號(hào)或上述布爾表達(dá)式所定義的信號(hào)）之間的時(shí)序關(guān)系。OVA通過(guò)事件表達(dá)式來(lái)定義設(shè)計(jì)的時(shí)序?qū)傩浴Ｍㄟ^(guò)OVA的事件表達(dá)式來(lái)描述時(shí)序?qū)傩员韧ㄟ^(guò)HDL進(jìn)行描述要簡(jiǎn)單明了的多。例子如下：
event chk : if (a) then
#1 istrue (a==1) in (#[0..3] b);
表述了這樣的時(shí)序關(guān)系：在任何時(shí)候，當(dāng)信號(hào)a為真的時(shí)候，信號(hào)b必須在此后的1到4個(gè)時(shí)鐘周期內(nèi)置位為真，并且在此期間，信號(hào)a必須一直保持為真，直到b為真。除了支持描述不同信號(hào)之間的時(shí)序關(guān)系外，OVA也支持描述所定義的事件之間的時(shí)序關(guān)系。例如下面的例子：
event e1: posedge rdy #1 proc_1 #1 proc_2;
event rule: if (reset)
then inst #1 ended e1 #1 branch_back;
表述了這樣的時(shí)序關(guān)系：事件e1：在rdy的上升沿一個(gè)時(shí)鐘周期之后，信號(hào)proc_1置位為真，再過(guò)一個(gè)時(shí)鐘周期，信號(hào)proc_2置位為真。事件rule：在reset信號(hào)置位的情況下，若信號(hào)inst置位則一個(gè)時(shí)鐘周期后事件e1必須結(jié)束，再一個(gè)時(shí)鐘周期之后，信號(hào)branch_back置位。這樣通過(guò)描述信號(hào)之間的時(shí)序關(guān)系以及事件之間的時(shí)序關(guān)系，我們可以方便地由一些簡(jiǎn)單的事件表達(dá)式構(gòu)成非常復(fù)雜的時(shí)序關(guān)系表示。
● 斷言聲明 ：斷言聲明指出設(shè)計(jì)所應(yīng)遵從的設(shè)計(jì)屬性。斷言聲明有兩類：forbid和check。forbid表示相應(yīng)的事件在設(shè)計(jì)中不應(yīng)發(fā)生，而check則表示相應(yīng)的事件在設(shè)計(jì)中應(yīng)該發(fā)生。例如下面的例子：
unit mutex_check (logic clk, logic a, logic b);
clock posedge (clk) {
event e_mutex: !(a && b);
}
assert a_mutex : check(e_mutex);
endunit
定義了一個(gè)事件e_mutex，并且定義了一個(gè)斷言聲明：在設(shè)計(jì)中，e_mutex應(yīng)當(dāng)為真。這樣當(dāng)信號(hào)a和b都置位的時(shí)候,事件e_mutex為假，仿真或形式驗(yàn)證工具會(huì)給出設(shè)計(jì)違背了斷言聲明所定義的屬性的信息。
● 設(shè)計(jì)屬性描述單元和綁定：上述所定義的信號(hào)、事件和斷言聲明可以組成一個(gè)設(shè)計(jì)屬性描述單元�？梢哉J(rèn)為設(shè)計(jì)屬性單元是一個(gè)設(shè)計(jì)屬性庫(kù)，同時(shí)在定義設(shè)計(jì)屬性單元時(shí)可以使用參數(shù)，以增加設(shè)計(jì)屬性單元的通用性、重用性。作為一個(gè)設(shè)計(jì)屬性庫(kù)，設(shè)計(jì)屬性單元可以以兩種方式綁定到相應(yīng)的設(shè)計(jì)：綁定到一個(gè)模塊，則在設(shè)計(jì)中，這個(gè)模塊的所有的例化都應(yīng)遵從斷言設(shè)定的屬性；或綁定到一個(gè)模塊的某一或某幾個(gè)的例化。下面兩個(gè)例子是上面兩種情形的示例：
bind module mpu : states mpu_states
#(3, 8, 2, "Not state 2") (clk, state_var, {{0}, {1}, {2}});
上面的例子將模塊mpu與設(shè)計(jì)屬性單元states進(jìn)行綁定。代碼的第二行設(shè)定了屬性描述單元states所包含的參數(shù)相應(yīng)的值。
bind instances tb.mpu1, tb.mpu2 : states mpu_states_instances
#(3, 8, 2, "Not state 2") (clk, state_var, {{0}, {1}, {2}});
這段代碼則將設(shè)計(jì)單元屬性states與模塊mpu的兩個(gè)例化tb.mpu1和tb.mpu2進(jìn)行綁定。
與OVL一樣，在OVA中也定義了常用的屬性聲明，構(gòu)成了OVA的檢查庫(kù)。OVA的檢查庫(kù)包括以下幾類：
· 對(duì)象值屬性檢查庫(kù)
. ova_arith_overflow . ova_asserted . ova_bits . ova_check_bool
. ova_const . ova_deasserted . ova_dec . ova_delta
. ova_even_parity .ova_forbid_bool . ova_inc
. ova_odd_parity . ova_overflow . ova_range ova_underflow . ova_value
· 狀態(tài)轉(zhuǎn)移屬性檢查庫(kù)
. ova_code_distance . ova_driven . ova_mutex . ova_next_state
. ova_one_cold . ova_one_hot . ova_quiescent_state . ova_tri_state
· 事件定時(shí)時(shí)序?qū)傩詸z查庫(kù)
. ova_hold . ova_hold_value . ova_reg_loaded . ova_sequence
. ova_timeout . ova_window
· 事件協(xié)議屬性檢查庫(kù)
. ova_arbiter . ova_data_used . ova_dual_clk_fifo . ova_fifo
. ova_follows . ova_memory . ova_memory_async . ova_no_contention
. ova_req_requires . ova_req_resp ova_stack . ova_valid_id
結(jié)論
設(shè)計(jì)復(fù)雜度的增加、IP重用等當(dāng)前復(fù)雜SoC/ASIC設(shè)計(jì)的特性要求對(duì)設(shè)計(jì)的功能進(jìn)行更加充分的驗(yàn)證。基于斷言技術(shù)并結(jié)合了動(dòng)態(tài)仿真、形式驗(yàn)證、測(cè)試激勵(lì)自動(dòng)化等方法的硬件驗(yàn)證平臺(tái)構(gòu)成了新的驗(yàn)證方法學(xué)，能有效提高驗(yàn)證的質(zhì)量和效率。
參考文獻(xiàn)
[1] AMBATM Specification(Rev2.0)
[2] www.accellera.com
[3] Gabe Moretti, “Formal verification is ready for the limelight”, EDN,2002,9,26
[4] OpenVera Assertions Language Reference Manual, Synopsys, Inc.
[5] 1076TM IEEE Standard VHDL Language Reference Manual
[6] Surrendra Dudani, “High Level Functional Verification Closure”, IEEE International Conference on Computer Design, 2002
[7] Michael C McFarland, “Formal Verification of Sequential Hardware: A Tutorial”, IEEE Transactions on Computer-aided Design of Integrated Circuites and Systems. Vol 12,No.5, May 1993
[8] Open Verification Library, Assertion Monitor Reference Manual. http://www.verificationlib.org/
[9] Bob Bentley, “Validating the Intel Pentium 4 Microprocessor”, Dependable Systems and Networks, 2001. Proeedings. The International Conference on , 1-4 July 2001
[10] Patankar,V.A, “Formal Verification of an ARM processor”, VLSI Design, 1999. Proceedings. Twelfth International Conference On , 7-10 Jan. 1999
|
|
66821730(技術(shù)支持)
