邏輯電路的設(shè)計(jì)驗(yàn)證

第6章邏輯電路的設(shè)計(jì)驗(yàn)證1驗(yàn)證(verification)是檢查設(shè)計(jì)實(shí)現(xiàn)的結(jié)果是否達(dá)到了設(shè)計(jì)規(guī)范的要求的過(guò)程。這里所指的設(shè)計(jì)實(shí)現(xiàn)的結(jié)果，包括功能、性能、規(guī)模、功耗等方面的實(shí)現(xiàn)結(jié)果。驗(yàn)證是IC設(shè)計(jì)過(guò)程中必不可少的關(guān)鍵步驟，對(duì)于保證設(shè)計(jì)的正確性，提高設(shè)計(jì)效率具有重要意義。隨著IC規(guī)模和設(shè)計(jì)復(fù)雜度的增加，驗(yàn)證工作量也迅速增加，甚至超過(guò)設(shè)計(jì)本身的工作量。研究IC設(shè)計(jì)驗(yàn)證的方法具有重要意義。26.1驗(yàn)證概述設(shè)計(jì)過(guò)程是將設(shè)計(jì)規(guī)范轉(zhuǎn)換為設(shè)計(jì)實(shí)現(xiàn)的過(guò)程。從規(guī)范到實(shí)現(xiàn)是一個(gè)從抽象到具體的不斷細(xì)化的過(guò)程，如最初設(shè)計(jì)描述采用自然語(yǔ)言方式，然后是系統(tǒng)結(jié)構(gòu)級(jí)描述、算法級(jí)描述、RTL代碼、門級(jí)網(wǎng)表、晶體管級(jí)，最終到物理版圖。驗(yàn)證過(guò)程是一個(gè)與設(shè)計(jì)過(guò)程相反的過(guò)程。它從實(shí)現(xiàn)方案開(kāi)始，驗(yàn)證其是否符合設(shè)計(jì)規(guī)范。在設(shè)計(jì)的每一步驟都有驗(yàn)證步驟與之相對(duì)應(yīng)。例如綜合前的RTL模型和綜合后網(wǎng)表的功能等效性驗(yàn)證。設(shè)計(jì)和驗(yàn)證的關(guān)系見(jiàn)教材139頁(yè)圖6-1。36.1.1驗(yàn)證方法建立驗(yàn)證方案，詳細(xì)列出需要驗(yàn)證的功能等項(xiàng)目。需要有一種度量驗(yàn)證質(zhì)量的尺度：功能覆蓋率和代碼覆蓋率。驗(yàn)證方法：基于仿真的驗(yàn)證和形式化驗(yàn)證?；诜抡娴尿?yàn)證依賴于測(cè)試向量，設(shè)計(jì)者給定輸入，然后評(píng)估輸出是否符合規(guī)范要求。形式化驗(yàn)證方法包括等價(jià)性驗(yàn)證和模型驗(yàn)證。等價(jià)性驗(yàn)證是指通過(guò)分析、對(duì)比兩個(gè)設(shè)計(jì)，論證兩個(gè)設(shè)計(jì)實(shí)現(xiàn)的功能是否一致。等價(jià)性驗(yàn)證不需要生成測(cè)試向量，但必須有一個(gè)功能完全正確的參考設(shè)計(jì)。模型驗(yàn)證是在一定的約束條件下，遍歷設(shè)計(jì)的狀態(tài)空間，以數(shù)學(xué)建模的方式從理論上推導(dǎo)、論證方案實(shí)現(xiàn)的正確性。46.1.2基于仿真的驗(yàn)證基于仿真(simulation)的驗(yàn)證可分為軟件仿真、硬件加速、硬件仿真三種方式。軟件仿真是最常用的驗(yàn)證方法。軟件仿真通過(guò)仿真工具(simulator)對(duì)設(shè)計(jì)的行為進(jìn)行模擬。仿真器的輸入包括：設(shè)計(jì)模塊和驗(yàn)證平臺(tái)(testbench)。面向驗(yàn)證的高層次語(yǔ)言HVL：把高級(jí)語(yǔ)言中面向?qū)ο蟮姆椒八惴?jí)描述同HDL中的并行性和時(shí)序結(jié)構(gòu)結(jié)合在一起，可以大大提高驗(yàn)證代碼的效率。硬件加速用于加速軟件仿真，縮短仿真時(shí)間。仿真系統(tǒng)被分為兩部分，其一為軟件仿真器，仿真不可綜合的HDL代碼和驗(yàn)證平臺(tái)；其二為硬件加速器，仿真所有可綜合的代碼。硬件加速器通常為FPGA或處理器陣列，可以將仿真速度提高兩三個(gè)數(shù)量級(jí)。5硬件仿真又稱為電路仿真或在線仿真，是使用可配置硬件實(shí)現(xiàn)設(shè)計(jì)，并在真實(shí)的應(yīng)用環(huán)境中對(duì)設(shè)計(jì)進(jìn)行驗(yàn)證的方法。硬件仿真的優(yōu)點(diǎn)：仿真手段更加接近于設(shè)計(jì)實(shí)現(xiàn)的實(shí)際情況，因此仿真的真實(shí)性更強(qiáng)，發(fā)現(xiàn)錯(cuò)誤的可能性更大，對(duì)設(shè)計(jì)正確性的保障更加有力；軟硬件的集成可以在實(shí)際的流片之前進(jìn)行，能夠及時(shí)發(fā)現(xiàn)系統(tǒng)級(jí)的設(shè)計(jì)錯(cuò)誤，提高了流片成功率；仿真速度快，縮短了開(kāi)發(fā)周期。硬件仿真的缺點(diǎn)：調(diào)試比較困難，通常需要借助專用儀器，如邏輯分析儀和示波器來(lái)監(jiān)控信號(hào)。軟件仿真和硬件仿真是互為補(bǔ)充的兩種驗(yàn)證方法。66.1.3形式化驗(yàn)證方法形式化驗(yàn)證(conformal)不需要生成測(cè)試向量。（1）等價(jià)性驗(yàn)證等價(jià)性驗(yàn)證可用于驗(yàn)證綜合后網(wǎng)表與原始RTL描述的功能是否一致。等價(jià)性驗(yàn)證也可用于比較兩個(gè)網(wǎng)表功能是否等價(jià)，如綜合后網(wǎng)表插入測(cè)試掃描鏈之后功能是否改變等。等價(jià)性驗(yàn)證也可用于檢查兩個(gè)RTL設(shè)計(jì)在邏輯上是否一致。（2）模型驗(yàn)證把設(shè)計(jì)規(guī)范體現(xiàn)的屬性和設(shè)計(jì)作為輸入，證明或反駁該設(shè)計(jì)具有這種屬性。模型驗(yàn)證的思想是在設(shè)計(jì)的整個(gè)狀態(tài)空間中搜索不符合屬性的點(diǎn)。如果發(fā)現(xiàn)這種點(diǎn)，則屬性不滿足，該點(diǎn)就成為一個(gè)反例，接著生成一個(gè)從反例中導(dǎo)出的路徑，引導(dǎo)設(shè)計(jì)者排除這個(gè)缺陷。7軟件仿真舉例1:RSA加密處理器仿真8RSA算法描述1、密鑰生成算法：(1)隨機(jī)取兩個(gè)不同且大小相近的大素?cái)?shù)p和q(保密)。(2)計(jì)算n=p.q(公開(kāi))，φ(n)=(p-1)(q-1)，其中φ(n)是n的歐拉函數(shù)值(保密)。(3)隨機(jī)選取整數(shù)e，使得1<e<φ(n),滿足gcd(e,φ(n))=1(公開(kāi))。(4)使用擴(kuò)展的歐幾里得算法計(jì)算d,滿足de≡1(modφ(n))的惟一整數(shù)d，且1<d<φ(n)(保密)。2、加解密算法：(1)加密算法:c=E(m)≡memodn(2)解密算法:m=D(c)≡cdmodn式中，m是明文，c是密文，n稱為模數(shù)，e是加密指數(shù)，(e,n)對(duì)是公鑰，d是解密指數(shù)，(d,n)對(duì)是私鑰。因?yàn)槟孢\(yùn)算m＝十分復(fù)雜，且存在多義性(不定)，所以它是一個(gè)單向陷門函數(shù)。同時(shí)，僅由公鑰e和n是無(wú)法求出d的，除非能將n分解求出p和q，這是大素?cái)?shù)分解(NP)難題難以實(shí)現(xiàn)。910信號(hào)名稱信號(hào)寬度傳輸方向信號(hào)含義clk1位輸入時(shí)鐘信號(hào)rst1位輸入復(fù)位信號(hào)，1有效。load1位輸入數(shù)據(jù)裝載使能信號(hào)，用于控制輸入明/密文、密鑰、模數(shù)以及某些參數(shù)，1有效。address3位輸入寄存器地址，用于表示明/密文寄存器、密鑰寄存器、模數(shù)寄存器以及某些參數(shù)寄存器。start1位輸入加/解密運(yùn)算開(kāi)始使能信號(hào)，1有效。din16位輸入輸入數(shù)據(jù)總線，用于輸入明/密文、密鑰、模數(shù)以及某些參數(shù)。wraddress6位輸入將1024位數(shù)據(jù)分成64個(gè)16位數(shù)據(jù)，每次寫(xiě)入1個(gè)16位數(shù)據(jù)，該地址指明16位數(shù)據(jù)的地址。result_shift1位輸入結(jié)果移位使能信號(hào)，1有效。有效時(shí)，將1024位加/解密結(jié)果右移16位，并將最低16位輸出。ready1位輸出加/解密運(yùn)算完成標(biāo)識(shí)信號(hào)，1有效。dout16位輸出輸出數(shù)據(jù)總線，用于輸出加/解密結(jié)果。表6-1:RSA模塊外部信號(hào)說(shuō)明11RSA加密處理器仿真:（1）測(cè)試數(shù)據(jù)輸入數(shù)據(jù)：N=0ac66f597f338ca1;//模數(shù)PT=0072418cccccccc3;//明文KEY=0000000000000007;//密鑰A=22kmodn=22048mod776430415944846497=(726986989413441796)10=(A16C6D0AC51A104)16;//常數(shù)AC=2kmodn=21024mod776430415944846497=(686167533972011608)10=(985C1BC96CEBA58)16;//常數(shù)C輸出結(jié)果：CT=52dc2c78533d116;//密文

12（2）驗(yàn)證平臺(tái)設(shè)計(jì)`timescale1ns/1nsmoduleRSA_tb;

reg

clk,rst,load,start,result_shift;

reg[2:0]address;

reg[15:0]din;

reg[5:0]wraddress;wire[15:0]dout;wireready;RSArsa(clk,rst,load,address,din,start,

dout,ready,wraddress,result_shift);//clk_gen

initialclk=1;always#50clk=~clk;13initialbegin#20rst=1;

result_shift=0;#200rst=0;start=0;load=1;//load1024bitsmodulus.address=3'd0;

wraddress=6'd0;din=16'h8ca1;#100wraddress=6'd1;din=16'h7f33;#100wraddress=6'd2;din=16'h6f59;#100wraddress=6'd3;din=16'h0ac6;#100wraddress=6'd4;din=16'h0000;……#100wraddress=6'd63;din=16'h0000;14#100load=1;//load1024bitsplaintext.address=3'd1;

wraddress=6'd0;din=16'hccc3;#100wraddress=6'd1;din=16'hcccc;#100wraddress=6'd2;din=16'h418c;#100wraddress=6'd3;din=16'h0072;#100wraddress=6'd4;din=16'h0000;……#100wraddress=6'd63;din=16'h0000;15#100load=1;//load1024bitskey.address=3'd2;

wraddress=6'd0;din=16'h0007;#100wraddress=6'd1;din=16'h0000;#100wraddress=6'd2;din=16'h0000;#100wraddress=6'd3;din=16'h0000;#100wraddress=6'd4;din=16'h0000;……#100wraddress=6'd63;din=16'h0000;16#100load=1;//load1024bitsparameterA.address=3'd3;

wraddress=6'd0;din=16'hA104;#100wraddress=6'd1;din=16'hAC51;#100wraddress=6'd2;din=16'hC6D0;#100wraddress=6'd3;din=16'h0A16;#100wraddress=6'd4;din=16'h0000;……#100wraddress=6'd63;din=16'h0000;

17#100load=1;//load1024bitsparameterC.address=3'd4;

wraddress=6'd0;din=16'hBA58;#100wraddress=6'd1;din=16'h96CE;#100wraddress=6'd2;din=16'hC1BC;#100wraddress=6'd3;din=16'h0985;#100wraddress=6'd4;din=16'h0000;……#100wraddress=6'd63;din=16'h0000;

18#100load=0;start=1;

#100start=0;

#106000000result_shift=1;#6300result_shift=0;#200$finish;

end

endmodule

19（3）仿真波形圖20仿真波形圖的局部放大：21軟件仿真舉例2:fifo_usb_rsa_tb仿真。

`timescale1ns/1nsmodulefifo_usb_rsa_tb;

reg

clk,rst;wirefull,empty;wire[15:0]fd;wiresloe,slrd,slwr;wire[1:0]fifoadr;

fifo_rsa

fifo_rsa(clk,rst,full,empty,fd,sloe,slrd,slwr,fifoadr);

usb_rsa

usb_rsa(clk,rst,full,empty,fd,sloe,slrd,slwr,fifoadr); //clockgeneration initialclk=1;always#50clk=~clk;initialbegin #20rst=1;//reset. #200rst=0; #318000000$finish; end endmodule22modulefifo_rsa(clk,rst,full,empty,fd,sloe,slrd,slwr,fifoadr);

inputclk,rst,sloe,slrd,slwr; input[1:0]fifoadr; inout[15:0]fd;

outputfull,empty;

reg[5231:0] readfifo; reg[1023:0]writefifo; reg[8:0]read_wordcount; reg[6:0]write_wordcount;

always@(posedgeclk) begin if(rst) readfifo={16'h0001,16'h0002,2316'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0072,16'h418c,16'hcccc,16'hccc3,16'h0004,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0985,16'hC1BC,16'h96CE,16'hBA58,16'h0008,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0A16,16'hC6D0,16'hAC51,16'hA104,16'h0010,24

16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0007,16'h0020,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0000,16'h0ac6,16'h6f59,16'h7f33,16'h8ca1,16'h0040}; 25 elseif((~slrd)&(fifoadr==2'b00)) readfifo<=(readfifo>>16); else readfifo<=readfifo; end

assignfd=(sloe==0)?readfifo[15:0]:16'bz;

//read_wordcountregister always@(posedgeclk) if(rst) read_wordcount<=9'd0; else if(slrd==0) read_wordcount<=read_wordcount+1; else read_wordcount<=read_wordcount;

assignempty=~(read_wordcount==9'd327);26//write_wordcountregister always@(posedgeclk) if(rst) write_wordcount<=7'd0; else if(slwr==0) write_wordcount<=write_wordcount+1; else write_wordcount<=write_wordcount;

assignfull=~(write_wordcount==7'd64);

always@(posedgeclk) begin if(rst) writefifo=1024'd0; elseif((~slwr)&(fifoadr==2'b10)) writefifo<={fd,writefifo[1023:16]}; else writefifo<=writefifo; end

endmodule27moduleusb_rsa(clk,rst,full,empty,fd,sloe,slrd,slwr,fifoadr);inputclk,rst,full,empty;

inout[15:0]fd;outputsloe,slrd,slwr;output[1:0]fifoadr;wireload,start,result_shift,ready;wire[2:0]address;wire[5:0]wraddress;wire[15:0]din,dout;

usb_rsa_intfu0(clk,rst,full,empty,fd,ready,dout,

load,address,wraddress,din,start,result_shift,

sloe,slrd,slwr,fifoadr);

RSAu1(clk,rst,load,address,din,start,dout,ready,

wraddress,result_shift);endmodule2829AES時(shí)序仿真波形圖-輸入密鑰30AES時(shí)序仿真波形圖-輸入明文31AES時(shí)序仿真波形圖-輸出密文32AES時(shí)序仿真波形圖-輸入密文33AES時(shí)序仿真波形圖-輸出明文34硬件仿真舉例:可移動(dòng)電腦加密機(jī)。

35可移動(dòng)電腦加密機(jī)樣機(jī)的主要技術(shù)指標(biāo)：（1）加/解密算法：可移動(dòng)高性能電腦加密機(jī)能夠?qū)崿F(xiàn)AES加/解密算法和RSA加/解密算法。其中，AES是對(duì)稱密鑰分組算法，其密鑰、明文和密文分組長(zhǎng)度均為128位；RSA是非對(duì)稱密鑰分組算法，其模數(shù)、密鑰、明文和密文分組長(zhǎng)度均為1024位。另外，由于加密芯片采用FPGA實(shí)現(xiàn)，因此可以根據(jù)應(yīng)用的需要，方便快捷地更換或升級(jí)加/解密算法。（2）加/解密芯片的性能與規(guī)模：可移動(dòng)高性能電腦加密機(jī)中的AES加/解密芯片和RSA加/解密芯片均采用Altera公司Cyclone系列的EP1C12Q240C8FPGA實(shí)現(xiàn)。其中，AES芯片的加/解密速度可達(dá)465Mbps(時(shí)鐘頻率40Mhz)，規(guī)模為4102個(gè)邏輯單元（logicelements）和40960個(gè)存儲(chǔ)位（memorybits）；RSA芯片的加/解密速度可達(dá)7812bps(時(shí)鐘頻率48Mhz)，規(guī)模為7271個(gè)邏輯單元和5120個(gè)存儲(chǔ)位。（3）與電腦的接口：可移動(dòng)高性能電腦加密機(jī)采用USB2.0接口與電腦通信，數(shù)據(jù)傳輸率為480Mbps，支持熱插拔，可以即插即用。36USB固件下載界面37FPGA配置文件下載界面38發(fā)送密鑰和S盒數(shù)據(jù)39發(fā)送明文40接收密文41接收解密后的明文

42加密機(jī)控制軟件用戶界面43加密機(jī)加載文件界面44加密機(jī)加密界面456.2驗(yàn)證平臺(tái)編碼風(fēng)格驗(yàn)證平臺(tái)通常指一段仿真代碼，用來(lái)為設(shè)計(jì)產(chǎn)生特定的輸入向量序列，也用來(lái)觀測(cè)設(shè)計(jì)輸出的響應(yīng)。一般的HDL語(yǔ)言都支持驗(yàn)證平臺(tái)的建模。驗(yàn)證過(guò)程需要模仿設(shè)計(jì)的外部環(huán)境，為設(shè)計(jì)提供輸入激勵(lì)信號(hào)，并監(jiān)視設(shè)計(jì)的輸出信號(hào)。驗(yàn)證平臺(tái)不需要綜合成硬件網(wǎng)表，相對(duì)于可綜合的編碼風(fēng)格，用于驗(yàn)證的代碼對(duì)編碼風(fēng)格限制較少。驗(yàn)證平臺(tái)相對(duì)于設(shè)計(jì)，往往代碼量更大，也更復(fù)雜，且因?yàn)轵?yàn)證代碼沒(méi)有可綜合的要求，所以提倡采用更高抽象層次的描述，如行為級(jí)描述，以減少代碼工作量，提高仿真速度。RTL編碼風(fēng)格與驗(yàn)證編碼風(fēng)格的不同。RTL編碼要可綜合，驗(yàn)證編碼僅僅關(guān)注行為。見(jiàn)P151例子。466.3驗(yàn)證平臺(tái)模塊設(shè)計(jì)復(fù)雜的驗(yàn)證平臺(tái)需要清晰的結(jié)構(gòu)。驗(yàn)證平臺(tái)的要求：結(jié)構(gòu)化、易維護(hù)、可重用。驗(yàn)證平臺(tái)一般可分為3個(gè)主要部分：激勵(lì)產(chǎn)生、響應(yīng)檢查和覆蓋率收集。6.3.1激勵(lì)產(chǎn)生激勵(lì)是賦給電路輸入信號(hào)的數(shù)據(jù)。信號(hào)賦值需要遵循一定的時(shí)序規(guī)則。為了使信號(hào)賦值簡(jiǎn)潔、高效、整齊，建議采用建立信號(hào)賦值任務(wù)和調(diào)用信號(hào)賦值任務(wù)的方式實(shí)現(xiàn)信號(hào)賦值。47信號(hào)賦值任務(wù)建立舉例：taskwrite_data_mode8;inputA0;input[7:0]send_data;beginRS=A0;RW=1’b0;#40;E=1’b1;#150;MPU_DB[7:0]=send_data[7:0];

data_set=1;#80;E=1’b0;#10;

data_set=0;RS=1’b1;RW=1’b1;#260;endendtask48信號(hào)賦值任務(wù)調(diào)用舉例：initialbegin…write_data_mode8(1,8’hab);…write_data_mode8(0,8’h38);#2000;$finish;end對(duì)于大數(shù)據(jù)量驗(yàn)證的情況，可預(yù)先生成一個(gè)測(cè)試向量文件，仿真時(shí)讀入內(nèi)存，并安時(shí)序加載到端口上作為仿真激勵(lì)。見(jiàn)下一頁(yè)例子。目前在驗(yàn)證領(lǐng)域?qū)崿F(xiàn)激勵(lì)產(chǎn)生的一個(gè)趨勢(shì)是采用有約束的隨機(jī)生成方式，可以提高工作效率和驗(yàn)證質(zhì)量。49taskapply_vector;inputindex,vector;output[N:1]primary_input;

reg[N:1]vector;begin

generate_vector(index,vector);

primary_input<=vector;endendtaskInitialbegin$load_memory(input_vectors,”stimuli_file”);endalways@(start)begin#10;

apply_vector(i,input_vectors);i=i+1;end506.3.2響應(yīng)檢查響應(yīng)檢查(responsechecking)包括兩個(gè)內(nèi)容：一是在仿真時(shí)對(duì)設(shè)計(jì)節(jié)點(diǎn)的監(jiān)視；二是把節(jié)點(diǎn)的響應(yīng)值與預(yù)期的值相比較。如果二者有差異，則需要分析原因，可能是由于設(shè)計(jì)缺陷引起的，也可能是由于規(guī)范的缺陷導(dǎo)致的。沒(méi)有差異，也不一定沒(méi)有缺陷，可能是錯(cuò)誤的接點(diǎn)沒(méi)有被采樣到，也可能是錯(cuò)誤沒(méi)有被激發(fā)。波形觀察是最常見(jiàn)的響應(yīng)檢查手段。波形按時(shí)間連續(xù)顯示，能夠得到完整的信號(hào)軌跡。但是，對(duì)信號(hào)波形連續(xù)的采樣耗費(fèi)大量的仿真資源，可通過(guò)減少采樣信號(hào)的數(shù)量或持續(xù)時(shí)間，提高仿真速度。這需要在采樣信號(hào)的數(shù)量、采樣持續(xù)時(shí)間和仿真速度進(jìn)行折中。一般來(lái)講，仿真前期應(yīng)采樣所有信號(hào)，當(dāng)代碼逐步穩(wěn)定后，或者進(jìn)入更高層次的集成仿真時(shí)，應(yīng)逐步減少采樣信號(hào)。51節(jié)點(diǎn)監(jiān)視方式：固定時(shí)間間隔采樣、當(dāng)數(shù)據(jù)發(fā)生變化時(shí)采樣。使用的系統(tǒng)函數(shù)：$strobe、$display、$monitor等。例子見(jiàn)p154圖6-12。仿真結(jié)果輸出或者是屏幕打印，或者是寫(xiě)文件，都會(huì)占用機(jī)器時(shí)間，特別對(duì)于大數(shù)據(jù)量的輸出，不僅會(huì)減慢仿真速度，而且還會(huì)導(dǎo)致觀察者因數(shù)據(jù)量過(guò)大而忽略重要信息。所以應(yīng)盡量減少輸出數(shù)據(jù)量，某些系統(tǒng)函數(shù)可以利用，如$monitoron,$monitoroff等。見(jiàn)p155圖6-13。人工檢查只適合處理較少數(shù)量的信號(hào)，不適合大型設(shè)計(jì)。把采樣信息與已知的正確信息(稱為黃金向量)相比較，比較由軟件工具自動(dòng)完成(文本比較、波形比較)，這樣的方式適合于大數(shù)據(jù)量的響應(yīng)檢查。黃金向量可以直接從規(guī)范生成，也可以由不同的設(shè)計(jì)模型(例如，不可綜合的高層模型或者C\C++模型)生成，例如p155圖6-15。52黃金向量文件的存儲(chǔ)占用大量存儲(chǔ)資源，維護(hù)困難，可以通過(guò)在驗(yàn)證平臺(tái)中增加自檢代碼的方法解決。在驗(yàn)證平臺(tái)中對(duì)信號(hào)采樣并與預(yù)期的行為進(jìn)行比較，這種技術(shù)稱為自檢。自檢代碼由兩部分構(gòu)成：自檢和警告。參見(jiàn)p156圖6-16。預(yù)期的行為可以離線先期完成或者即時(shí)生成。如果被檢測(cè)的信號(hào)與所預(yù)期的行為不匹配，則檢測(cè)錯(cuò)誤并將其分類為不同嚴(yán)重等級(jí)。根據(jù)錯(cuò)誤的嚴(yán)重程度，可以在發(fā)出錯(cuò)誤信息后繼續(xù)仿真，或者可以退出仿真狀態(tài)，也可以轉(zhuǎn)儲(chǔ)信號(hào)跟蹤信息。檢查代碼應(yīng)該與設(shè)計(jì)代碼相分離，因?yàn)闄z查代碼不是最終代碼的構(gòu)成部分。分離的方法：給檢查代碼加條件編譯指令，把檢查代碼單獨(dú)寫(xiě)到一個(gè)任務(wù)中，在調(diào)用處加編譯開(kāi)關(guān)。53舉例：乘法器自檢驗(yàn)證。multiplierinstance(.in1(mult1),in2(mult2),.prod(product));assignexpected=mult1*mult2;always@(product)beginif(expected!=product)$display(“ERROR:incorrectproduct.result=%d,multiplicant1=%d,multiplicant2=%d”,product,mult1,mult2);$finish;end舉例：帶條件編譯指令的自檢驗(yàn)證代碼，見(jiàn)p157。自檢代碼也可利用C/C++編程，然后利用PLI接口與HDL驗(yàn)證環(huán)境相連。見(jiàn)p157圖6-18。54參考模型驗(yàn)證技術(shù)：參考模型通常采用高級(jí)語(yǔ)言或行為級(jí)HDL編寫(xiě)，實(shí)現(xiàn)設(shè)計(jì)的規(guī)范并將其響應(yīng)和RTL模型的響應(yīng)進(jìn)行比較。參考模型可以和RTL模型一起或單獨(dú)運(yùn)行。對(duì)于獨(dú)立運(yùn)行，參考模型取得一組RTL模型上仿真的激勵(lì)，并把響應(yīng)寫(xiě)入文件，然后RTL模型用同一組激勵(lì)仿真，將響應(yīng)與參考模型的響應(yīng)進(jìn)行比較。如果參考模型與RTL模型并發(fā)運(yùn)行，稱為協(xié)同仿真。參見(jiàn)p158圖6-19。隨著仿真工具的發(fā)展，協(xié)同仿真逐漸成為主流，可以將C/C++、SystemC、Matlab等工具和仿真工具聯(lián)合起來(lái)進(jìn)行協(xié)同仿真。這種協(xié)同仿真的優(yōu)點(diǎn)是在完成系統(tǒng)級(jí)和RTL級(jí)設(shè)計(jì)后，可以將RTL設(shè)計(jì)和系統(tǒng)級(jí)設(shè)計(jì)結(jié)合進(jìn)行結(jié)果比對(duì)，從而保證設(shè)計(jì)結(jié)果的一致性。556.3.3初始化初始化(initialization)是把系統(tǒng)正常工作所需要的一些值賦給某些輸入信號(hào)和存儲(chǔ)器等變量。初始化使用HDL代碼或編程語(yǔ)言接口實(shí)現(xiàn)。HDL代碼初始化通常封裝在initial語(yǔ)句塊中，參見(jiàn)p159圖6-20例子。初始化的代碼描述了一個(gè)過(guò)程，它不能綜合，不應(yīng)把他們放在任何庫(kù)單元內(nèi)部。6.3.4時(shí)鐘生成與同步時(shí)鐘是主要的同步(synchronization)信號(hào)。時(shí)鐘波形是周期性的，只要寫(xiě)出一個(gè)時(shí)鐘周期的HDL代碼，就可以循環(huán)產(chǎn)生完整的波形。生成單周期波形可以使用過(guò)程賦值，也可以利用邏輯取反操作。舉例：見(jiàn)p159圖6-21。56時(shí)鐘的分頻和倍頻：參見(jiàn)p160圖6-22。無(wú)關(guān)時(shí)鐘：對(duì)于相對(duì)獨(dú)立的時(shí)鐘，為了強(qiáng)調(diào)它們更多的獨(dú)立性，在其中一個(gè)時(shí)鐘引入抖動(dòng)的概念，使得兩個(gè)無(wú)關(guān)時(shí)鐘具有不確定的相對(duì)移位。可以利用隨機(jī)數(shù)使時(shí)鐘抖動(dòng)，參見(jiàn)p160圖6-23。移相時(shí)鐘：兩個(gè)時(shí)鐘信號(hào)之間存在確定的相位差。參見(jiàn)p160圖6-24。6.3.5驗(yàn)證平臺(tái)和設(shè)計(jì)之間的接口驗(yàn)證平臺(tái)到系統(tǒng)設(shè)計(jì)之間的接口負(fù)責(zé)它們之間的數(shù)據(jù)交換，這包括4個(gè)方面和渠道：設(shè)計(jì)的I/O端口、分層訪問(wèn)、文件I/O以及PLI接口。設(shè)計(jì)的I/O端口是設(shè)計(jì)功能體現(xiàn)的基本界面，也是與驗(yàn)證平臺(tái)連通的基本接口。驗(yàn)證平臺(tái)通過(guò)這些I/O端口輸入激勵(lì)信號(hào)，也從中獲取響應(yīng)信號(hào)。57分層訪問(wèn)是驗(yàn)證平臺(tái)快速訪問(wèn)設(shè)計(jì)內(nèi)部的通道，因?yàn)橥ㄟ^(guò)I/O訪問(wèn)或改變?cè)O(shè)計(jì)內(nèi)部狀態(tài)需要長(zhǎng)的控制序列。分層訪問(wèn)是驗(yàn)證平臺(tái)提供的虛擬接口得以直接訪問(wèn)設(shè)計(jì)的內(nèi)部信息，最終在物理上是無(wú)法實(shí)現(xiàn)的。文件I/O是設(shè)計(jì)和驗(yàn)證平臺(tái)交流信息的媒介。驗(yàn)證平臺(tái)把激勵(lì)信號(hào)寫(xiě)入文件，設(shè)計(jì)讀出后相當(dāng)于獲得相應(yīng)的輸入信號(hào)；設(shè)計(jì)把響應(yīng)寫(xiě)入文件供驗(yàn)證平臺(tái)讀出分析。設(shè)計(jì)通過(guò)PLI與驗(yàn)證平臺(tái)也有一個(gè)接口。HDL通過(guò)任務(wù)調(diào)用用戶C/C++程序，這些程序提供算法級(jí)的參考模型，同時(shí)參考模型通過(guò)PLI接口可以反向訪問(wèn)設(shè)計(jì)內(nèi)部資源。擴(kuò)展利用PLI可以實(shí)現(xiàn)設(shè)計(jì)與參考模型的協(xié)同仿真。586.4驗(yàn)證平臺(tái)結(jié)構(gòu)設(shè)計(jì)6.4.1基于harness封裝的驗(yàn)證平臺(tái)結(jié)構(gòu)良好的驗(yàn)證平臺(tái)結(jié)構(gòu)應(yīng)該是由多個(gè)可復(fù)用的驗(yàn)證模塊組成，利用這些可復(fù)用的驗(yàn)證模塊可以很方便地構(gòu)造出驗(yàn)證功能所需要的多個(gè)測(cè)試用例。通常，整個(gè)驗(yàn)證平臺(tái)用一個(gè)分層模塊結(jié)構(gòu)實(shí)現(xiàn)，將一些固定的序列激勵(lì)用task封裝。在保證task賦值序列的時(shí)序沒(méi)有問(wèn)題的情況下，不同的測(cè)試用例調(diào)用相同的task和使用不同的參數(shù)。舉例：參見(jiàn)p161圖6-25。從外部來(lái)看設(shè)計(jì)，通常設(shè)計(jì)可以看作有多個(gè)接口的黑盒子。如p162圖6-26所示。并且，很多接口為標(biāo)準(zhǔn)接口，如PCI接口、MCU接口、USB接口等。這些接口在很多設(shè)計(jì)中使用，接口驅(qū)動(dòng)任務(wù)也可以在很多設(shè)計(jì)的驗(yàn)證平臺(tái)中重用。59基于總線的驗(yàn)證平臺(tái)，如p163圖6-27所示。該平臺(tái)包括總線功能模型(BFM)，設(shè)計(jì)和測(cè)試用例。所有的測(cè)試用例都通過(guò)總線功能模型與待驗(yàn)證設(shè)計(jì)連接起來(lái)，這樣就可以把待驗(yàn)證設(shè)計(jì)和總線功能模型封裝在一起，作為所有驗(yàn)證平臺(tái)共用的、更高層次的驗(yàn)證對(duì)象，稱為驗(yàn)證平臺(tái)的外殼(harness)。每個(gè)測(cè)試用例加上harness形成各自的驗(yàn)證平臺(tái)。采用harness結(jié)構(gòu)將大大簡(jiǎn)化驗(yàn)證平臺(tái)，降低驗(yàn)證的工作量。參見(jiàn)p163圖6-28。6.4.2用Verilog構(gòu)建結(jié)構(gòu)化的驗(yàn)證平臺(tái)p164圖6-30是一個(gè)用Verilog語(yǔ)言構(gòu)建的驗(yàn)證平臺(tái)。包含測(cè)試用例、harness平臺(tái)、harness平臺(tái)中包括的模塊。圖6-31是應(yīng)用層封裝的驗(yàn)證平臺(tái)。6.4.3用SystemVerilog構(gòu)建結(jié)構(gòu)化的驗(yàn)證平臺(tái)常用的高級(jí)驗(yàn)證語(yǔ)言：SystemVerilog、SystemC、Vera、e等，高級(jí)驗(yàn)證語(yǔ)言通?？梢蕴峁┗谒惴ǖ拿枋鲆约皩?duì)復(fù)雜數(shù)據(jù)結(jié)構(gòu)的描述和封裝。參見(jiàn)p167圖6-32。606.5斷言6.5.1斷言簡(jiǎn)介斷言是由一組語(yǔ)句組成的結(jié)構(gòu)，用于對(duì)信號(hào)或變量是否滿足某個(gè)條件進(jìn)行檢測(cè)