電子設(shè)計(jì)自動(dòng)化驗(yàn)證技術(shù)概述

1、驗(yàn)證技術(shù)概述Introduction to Verification1內(nèi)容驗(yàn)證技術(shù)概述功能驗(yàn)證、等價(jià)性驗(yàn)證、靜態(tài)分析及物理檢查3. 模擬4. 形式驗(yàn)證5. 驗(yàn)證方法學(xué)2 Cell Library Design Rule. .Spec.Behavior HDLRTL HDLSynthesisNetlistPlacement&RoutingIC LayoutFPGAAreaTimingPowerDFTSimulation and VerificationFPGA Compiler 自 頂 向 下3驗(yàn)證的重要性驗(yàn)證的重要性：占工程設(shè)計(jì)時(shí)間70，代碼總量80驗(yàn)證影響：產(chǎn)品的生命產(chǎn)品返工失去顧客成本4驗(yàn)

2、證的目的及其本質(zhì)驗(yàn)證的目的：原始描述的正確性：SPEC設(shè)計(jì)結(jié)果與原始描述的一致性設(shè)計(jì)結(jié)果是否符合設(shè)計(jì)規(guī)則驗(yàn)證的本質(zhì)：驗(yàn)證本質(zhì)上就是保證某種形式的轉(zhuǎn)換符合我們的期望，即保證設(shè)計(jì)正確的實(shí)現(xiàn)了規(guī)范所定義的功能和性能要求。 芯片的設(shè)計(jì)規(guī)范(一般是一個(gè)文本文件)與其系統(tǒng)級(jí)模型（高級(jí)語言模型，如C模型）之間的等效通過比較系統(tǒng)級(jí)模型與 HDL 實(shí)現(xiàn)的輸出，可以在規(guī)范的系統(tǒng)級(jí)模型與其 HDL 實(shí)現(xiàn)之間建立等效關(guān)系。 HDL實(shí)現(xiàn)與門級(jí) (綜合后的)之間通過應(yīng)用“邏輯等效性檢查”可以建立等效 5工程對(duì)驗(yàn)證的要求驗(yàn)證的完整性：只有充分接近全部功能得到驗(yàn)證，并達(dá)到功能覆蓋率的要求，才能對(duì)產(chǎn)品有信心。驗(yàn)證的自動(dòng)化：盡可

3、能減少驗(yàn)證時(shí)間對(duì)產(chǎn)品產(chǎn)出時(shí)間的影響，驗(yàn)證才是成功的，這需要EDA工具和先進(jìn)驗(yàn)證手段的支持。6驗(yàn)證系統(tǒng)驗(yàn)證系統(tǒng)的組成：驗(yàn)證說明：描述目標(biāo)行為以及不希望出現(xiàn)之行為的設(shè)計(jì)規(guī)范（Specification）成品模型：環(huán)境模型：模型類別：硬件：prototype-仿真(Emulation)軟件：C or RTL Code-模擬(Simulation)混合：7設(shè)計(jì)各階段驗(yàn)證的內(nèi)容前端設(shè)計(jì)：功能驗(yàn)證 ：代碼是否符合設(shè)計(jì)規(guī)范 等價(jià)性驗(yàn)證 ：各層次的功能是否滿足原有功能規(guī)范 后端設(shè)計(jì)：功能：門級(jí)仿真（后仿真） 性能（setup、hold、驅(qū)動(dòng)）：靜態(tài)時(shí)序分析物理設(shè)計(jì) ：規(guī)則檢查（design rule chec

4、k）電氣規(guī)則檢查 (ERC)、設(shè)計(jì)規(guī)則檢查 (DRC)、版圖對(duì)電路檢查 （LVS)信號(hào)完整性、干擾、金屬遷移、噪聲 8功能驗(yàn)證分類：目的性驗(yàn)證：目的是驗(yàn)證設(shè)計(jì)所試圖完成的功能在設(shè)計(jì)中已正確實(shí)現(xiàn)。最典型的情況是在抽象程度最高的層次完成，其最終結(jié)果是建立一套“黃金模型”，它可以在整個(gè)設(shè)計(jì)過程中作為設(shè)計(jì)細(xì)節(jié)的參考。等價(jià)性驗(yàn)證：目的是驗(yàn)證設(shè)計(jì)過程中產(chǎn)生的不同層次的設(shè)計(jì)結(jié)果功能是否符合“黃金模型”。9目的性驗(yàn)證 1. 動(dòng)態(tài)模擬：將一組輸入激勵(lì)施加到設(shè)計(jì)模型上，使其工作運(yùn)行，并觀察模型的響應(yīng)。2. 形式驗(yàn)證：用數(shù)學(xué)方法驗(yàn)證設(shè)計(jì)的功能，不需要驗(yàn)證測試向量。3. 模擬形式混合驗(yàn)證：混合驗(yàn)證取兩者之優(yōu)點(diǎn)，模擬能

5、處理的設(shè)計(jì)規(guī)模大，類型多，而形式驗(yàn)證具有完整性。4. 軟/硬件協(xié)同驗(yàn)證：協(xié)同驗(yàn)證可以在硬件開發(fā)的同時(shí)，讓軟件在硬件模擬平臺(tái)上運(yùn)行，從而硬件和軟件可以同時(shí)調(diào)試，而不是串行進(jìn)行，大大縮短了產(chǎn)品的開發(fā)時(shí)間。 10目的性驗(yàn)證（續(xù)）5.仿真系統(tǒng)：專門設(shè)計(jì)的硬件和軟件系統(tǒng)，典型的是采用FPGA-與最終設(shè)計(jì)接近的仿真速度。6.樣機(jī)系統(tǒng) ：系統(tǒng)測試、市場開發(fā)、演示(1)物理樣機(jī)：一種目標(biāo)設(shè)計(jì)的硬件替代品，它的運(yùn)行能夠“接近”目標(biāo)設(shè)計(jì)平臺(tái)的性能。與目標(biāo)系統(tǒng)速度相同的數(shù)量級(jí)，比仿真系統(tǒng)的速度快出許多。 (2)虛擬樣機(jī)：一個(gè)虛擬樣機(jī)就是一個(gè)產(chǎn)品、一個(gè)元件或一個(gè)系統(tǒng)的計(jì)算機(jī)模擬模型。 11 物理樣機(jī)Parterre之

6、FPGA驗(yàn)證平臺(tái)12等價(jià)性驗(yàn)證 1.動(dòng)態(tài)等價(jià)驗(yàn)證i)確定模擬：復(fù)用高層次模型開發(fā)的驗(yàn)證測試向量和測試程序 ii)回歸測試：批處理模擬；自動(dòng)比較結(jié)果 2.形式等價(jià)驗(yàn)證：完全的等價(jià)驗(yàn)證，如Formality 形式等價(jià)驗(yàn)證工具生成一個(gè)數(shù)據(jù)結(jié)構(gòu)并比較在相同的輸入模式下得出的輸出數(shù)值模式，如果這些輸出數(shù)值模式不相同，那么同一設(shè)計(jì)的兩種描述(如門級(jí)和 RTL級(jí))就不是等價(jià)的。組合等價(jià)檢驗(yàn)和時(shí)序等價(jià)檢驗(yàn) 13靜態(tài)分析驗(yàn)證 1）Lint檢查：對(duì)設(shè)計(jì)代碼進(jìn)行靜態(tài)檢查，驗(yàn)證語法的正確性。Lint檢驗(yàn)對(duì)RTL設(shè)計(jì)代碼進(jìn)行靜態(tài)檢查，是在設(shè)計(jì)進(jìn)行綜合前的一種預(yù)處理，目的是消除代碼中的錯(cuò)誤，包括語法、可綜合性、未初始化的

7、變量、未支持的語言結(jié)構(gòu)、端口失配等。有些工具還能抽取FSM模型，檢測競爭條件，檢查可測試性和可重用性規(guī)定的一些設(shè)計(jì)規(guī)則等。2）靜態(tài)時(shí)序分析 每個(gè)存儲(chǔ)元件有時(shí)序要求，例如，建立時(shí)間、保持時(shí)間和各種延時(shí)。時(shí)序驗(yàn)證要確定電路時(shí)序是否滿足設(shè)計(jì)要求。 14物理驗(yàn)證 物理驗(yàn)證就是通過檢驗(yàn)圖形設(shè)計(jì)的數(shù)據(jù)庫以確信物理實(shí)現(xiàn)確實(shí)是原始邏輯設(shè)計(jì)的正確表述。物理驗(yàn)證包括以下三個(gè)部分：電學(xué)規(guī)則檢查、設(shè)計(jì)規(guī)則檢查及版圖對(duì)電路檢查。標(biāo)準(zhǔn)的圖形數(shù)據(jù)庫形式是GDSII數(shù)據(jù)流。15物理驗(yàn)證（續(xù)）1)電氣規(guī)則檢查 (ERC)：檢查是否違反電氣設(shè)計(jì)規(guī)則，包括未使用的輸出、浮空輸入、負(fù)載違例、連接違例，如開路和短路等。2)設(shè)計(jì)規(guī)則檢查

8、 (DRC)：檢查是否違反工藝過程設(shè)計(jì)規(guī)則，包括層與層的間距、特定層上的線條寬度、層與層的重疊等。3)版圖對(duì)電路檢查(LVS)：檢驗(yàn)提取的圖形數(shù)據(jù)庫是否有與“黃金”網(wǎng)表相違背之處。LVS工具從多邊形數(shù)據(jù)中構(gòu)建網(wǎng)表以及從物理布局中提取器件模型。提取出的網(wǎng)表需和“黃金”模型保持一致。所有的器件和互連都必須嚴(yán)格地相匹配。4)其他物理驗(yàn)證：包括信號(hào)完整性、干擾、金屬遷移、噪聲等。16模擬基于模擬的驗(yàn)證是功能驗(yàn)證最重要、用得最多的一種方法。它是在模擬器上通過模擬實(shí)際電路的工作環(huán)境來對(duì)設(shè)計(jì)進(jìn)行驗(yàn)證。模擬的基本方法：首先根據(jù)設(shè)計(jì)規(guī)范和測試規(guī)范,建立測試平臺(tái)，編寫測試數(shù)據(jù)組（testcase）以生成測試激勵(lì)以

9、及響應(yīng)檢查；然后在模擬器上進(jìn)行模擬，將測試數(shù)據(jù)組的激勵(lì)輸入到硬件描述語言代碼模型最后對(duì)輸出同標(biāo)準(zhǔn)輸出結(jié)果進(jìn)行比較，從而達(dá)到功能驗(yàn)證的目的。 17基于模擬的驗(yàn)證基于模擬的驗(yàn)證結(jié)構(gòu)可分為四個(gè)部分：測試數(shù)據(jù)組（testcase）測試平臺(tái)（testbench）參考模型（reference model）仿真器 （simulator）18測試數(shù)據(jù)組測試數(shù)據(jù)組是對(duì)待測模型產(chǎn)生激勵(lì)的來源。設(shè)計(jì)測試數(shù)據(jù)組的關(guān)鍵是確定待測模型需要驗(yàn)證的屬性（features），也就是功能驗(yàn)證點(diǎn)。正確識(shí)別和詳細(xì)分析屬性，并依此產(chǎn)生相應(yīng)的測試數(shù)據(jù)組，決定了驗(yàn)證的功能覆蓋率，從而最終決定了待測模型是否充分滿足設(shè)計(jì)規(guī)范的要求。測試數(shù)據(jù)組

10、的生成：是由驗(yàn)證工程師手工編寫。目前也出現(xiàn)了自動(dòng)測試數(shù)據(jù)組生成工具，如synopsys的半自動(dòng)測試數(shù)據(jù)組生成工具Vera。它利用語言定義各種約束，以指導(dǎo)偽隨機(jī)測試的生成，結(jié)合功能覆蓋分析，幫助驗(yàn)證工程師建立高效的驗(yàn)證環(huán)境，使得到高質(zhì)量的測試程序。 19測試數(shù)據(jù)組（續(xù)）每一個(gè)測試數(shù)據(jù)組一般包括激勵(lì)數(shù)據(jù)和輸出響應(yīng)數(shù)據(jù)。在實(shí)際設(shè)計(jì)過程中，測試數(shù)據(jù)組通常分為三部分：接口測試：檢驗(yàn)?zāi)K接口時(shí)序和協(xié)議子模塊測試：子模塊功能驗(yàn)證系統(tǒng)測試：全系統(tǒng)功能驗(yàn)證 2021測試平臺(tái) 測試平臺(tái)是為模擬驗(yàn)證而編寫的代碼，其目的是用來對(duì)待測設(shè)計(jì)產(chǎn)生預(yù)先確定的輸入序列，然后選擇性的觀察響應(yīng)。測試平臺(tái)可采用硬件描述語言來編寫，也

11、可以采用e或OpenVera等驗(yàn)證語言編寫。 22結(jié)構(gòu)化的測試平臺(tái) 可復(fù)用的測試基準(zhǔn)BFM（Bus-Function Model）概念：將測試數(shù)據(jù)組提供的測試數(shù)據(jù)，通過統(tǒng)一的任務(wù)接口，按照待測模型端口的時(shí)序和協(xié)議進(jìn)行封裝組合的程序模塊。由子程序以及Task等組成，代替總線的簡單模型，可以復(fù)用Testcase Reusable Verification Component BusFunction Model Design UnderVerification Bus Function Model Harness23結(jié)構(gòu)化的測試平臺(tái) BFM原理：能夠使用某種命令語言在總線上產(chǎn)生一系列事務(wù)。不含有總線

12、設(shè)備的實(shí)現(xiàn)，亦不需要包含總線設(shè)備的全部功能只含有總線、I/O接口的信號(hào)，并模擬這些信號(hào)的傳輸過程 24參考模型 參考模型：一種專門面向功能驗(yàn)證而設(shè)計(jì)的代碼，可以在施加于待測設(shè)計(jì)的相同激勵(lì)條件下，產(chǎn)生預(yù)期的結(jié)果，該結(jié)果做為testbench檢查器的預(yù)期響應(yīng)參與比較。參考模型的主要目的就是生成與目標(biāo)設(shè)計(jì)描述進(jìn)行比較的比對(duì)數(shù)據(jù)。參考模型側(cè)重于設(shè)計(jì)的邏輯功能，而不是功能實(shí)現(xiàn)的細(xì)節(jié)。 25參考模型Design Under Test （DUT）激勵(lì)發(fā)生器結(jié)果檢查黃金模型golden model26驗(yàn)證實(shí)例：UART驗(yàn)證環(huán)境和測試方案testbench根據(jù)設(shè)計(jì)文檔確定驗(yàn)證點(diǎn)（testcase）驗(yàn)證文檔：描述

13、每個(gè)驗(yàn)證點(diǎn)的目的、具體實(shí)現(xiàn)步驟驗(yàn)證文檔testcase提取覆蓋率分析不理想回到第2階段記錄驗(yàn)證結(jié)果.log文件27驗(yàn)證環(huán)境架構(gòu)及建立方式基于軟件模擬的層次式架構(gòu)testcase層：由過程（procedure）調(diào)用組成行為模型以及BFM：不可綜合的代碼，描述系統(tǒng)環(huán)境中可能的其他電路模型或行為testbench：驗(yàn)證配置testbench組織：configurations裝配testcase，行為模型，BFM以及待測模塊DUT28UART驗(yàn)證環(huán)境架構(gòu)29確定驗(yàn)證點(diǎn)testcase提?。簍asks激勵(lì)：從單一功能到復(fù)雜功能，輔以覆蓋率工具響應(yīng)：針對(duì)具體testcase描述檢查相關(guān)響應(yīng)30例：數(shù)據(jù)發(fā)送

14、進(jìn)程testcase生成testcase1:驗(yàn)證UART是否能夠正確發(fā)送數(shù)據(jù)a.保持發(fā)送時(shí)鐘基準(zhǔn)時(shí)鐘*8得到的位時(shí)鐘txtick；b.調(diào)用APB_write任務(wù)向UART 控制寄存器寫入“000101010”；c.調(diào)用APB_write任務(wù)向UART 發(fā)送保持寄存器thold寫入“10101010”；d.調(diào)用TXD_verify任務(wù)，并檢測是否正確接收“10101010”testcase2:驗(yàn)證UART能否檢驗(yàn)出奇偶校驗(yàn)錯(cuò)，并據(jù)此發(fā)出中斷請(qǐng)求a.保持發(fā)送時(shí)鐘基準(zhǔn)時(shí)鐘*8得到的位時(shí)鐘txtick；b.調(diào)用APB_write任務(wù)向UART 控制寄存器寫入“000101010”；c. 調(diào)用APB_w

15、rite任務(wù)向UART 發(fā)送保持寄存器thold寫入“10101010”；d.調(diào)用TXD_verify任務(wù)，并檢測是否正確接收“10101010”，偶校驗(yàn)無誤，并接收到IRQ信號(hào)；e.調(diào)用APB_write任務(wù)向UART 控制寄存器寫入“000111010”；f. 調(diào)用APB_write任務(wù)向UART 發(fā)送保持寄存器thold寫入“10101010”；g.調(diào)用TXD_verify任務(wù)，并檢測是否正確接收“10101010”，奇校驗(yàn)無誤，并接收到IRQ信號(hào)；testcase3：溢出錯(cuò)誤檢查testcase4：發(fā)送過程清TEtestcase5：流控制檢查testcase提取31testcase實(shí)例

16、-simulustask serial_data_input_generater;input7:0 data;input1:0 verify_indicate;input baudrate_clk;output RXD;/ verify_indicate 1=1，表示有校驗(yàn)位，否則無校驗(yàn)位； / verify_indicate 0 =1，表示奇校驗(yàn)，否則為偶校驗(yàn)；wire verify_bit = verify_indicate 0? data:data;begin (posedge baudrate_clk) TXD= 1b0; (posedge baudrate_clk) TXD= dat

17、a0; (posedge baudrate_clk) TXD= data1; (posedge baudrate_clk) TXD= data2; (posedge baudrate_clk) TXD= data3; (posedge baudrate_clk) TXD= data4; (posedge baudrate_clk) TXD= data5; (posedge baudrate_clk) TXD= data6; (posedge baudrate_clk) TXD= data7; (posedge baudrate_clk) TXD= verify_indicate1? verif

18、y_bit:1b1; (posedge baudrate_clk) TXD= 1b1;endendtask 32testcase實(shí)例-receiving datamodule testbench_for_UART_RXD;/例化待測模塊UART UART u1(RXD, TXD,.); /順序執(zhí)行任務(wù)序列，進(jìn)行功能驗(yàn)證initial begin/調(diào)用激勵(lì)產(chǎn)生模塊，輸入數(shù)據(jù)8ha5，1位偶校驗(yàn)位serial_data_input_generater(8ha5, 2b10, baudrate, RXD); Endendmodule33testbench1）將上述task在testbench的pro

19、cess中排列組合，分別調(diào)度就組成一個(gè)面向UART 的 黑盒子testbench generater2）把UART和testbench generater在頂層模塊配置指定testbench，則可進(jìn)行模擬驗(yàn)證 34模擬仿真工具模擬工具：模擬器SimulatorVerilog-XLModelsimNC VerilogVSS（VHDL）VCS（Verilog ）35模擬仿真工具模擬器工作原理：編譯法Compiler：將HDL的描述編譯成一般軟件語言或匯編語言再執(zhí)行事件表驅(qū)動(dòng)法Event Driven ：對(duì)描述進(jìn)行解釋執(zhí)行Cycle Based NC Verilog：一個(gè)時(shí)鐘周期只采一次數(shù)據(jù) ISS

20、 （Instruction Set Simulation）- 指令級(jí)模擬器： 用于有CPU的系統(tǒng)模擬 363738模擬仿真工具仿真（Emulation）： FPGA 把設(shè)計(jì)從RTL綜合后寫入FPGA中, 與周邊芯片連成系統(tǒng)進(jìn)行板級(jí)仿真. 特點(diǎn): 驗(yàn)證功能及接口 速度快：界于實(shí)物芯片和模擬之間 只模擬功能，不模擬速度39基于模擬的驗(yàn)證方法 組合邏輯MEMnmn+m2n+m121010241001.26E+3010001.07E+30110238.99E+307窮舉模擬？可能的狀態(tài)轉(zhuǎn)換 2n+m40基于模擬的驗(yàn)證方法測試向量生成：規(guī)范一致性測試：所有“指令”、“控制模式”邊角測試 （Corner

21、Case）隨機(jī)測試 無向隨機(jī)模擬 有向隨機(jī)模擬 設(shè)計(jì)錯(cuò)誤模型實(shí)代碼 (Real Code)回歸測試(Regression testing) 41基于模擬的驗(yàn)證衡量方法 代碼覆蓋率 通過硬件代碼覆蓋率分析工具來評(píng)定驗(yàn)證測試序列的覆蓋率指標(biāo)。把特定的測試驗(yàn)證序列輸入到特定設(shè)計(jì)中，通過代碼覆蓋率分析就有可能得出功能覆蓋率的某些方面的信息。分析工具可以提供以下信息：每個(gè)被評(píng)估屬性的百分比的覆蓋率值設(shè)計(jì)中沒有執(zhí)行或者只是部分執(zhí)行的區(qū)域的列表可進(jìn)行有目的的狀態(tài)覆蓋嘗試改變原始模擬蹤跡，進(jìn)行指導(dǎo)42代碼覆蓋的類型 語句覆蓋：表示多少語句已被執(zhí)行過，或者每個(gè)語句執(zhí)行過的次數(shù)。翻轉(zhuǎn)覆蓋：表示信號(hào)中哪些位已經(jīng)過0

22、1和10翻轉(zhuǎn)。觸發(fā)覆蓋：每個(gè)進(jìn)程是否被敏感表中每個(gè)信號(hào)獨(dú)立地觸發(fā)。分支覆蓋：“if”或 “case”語句中的哪些分支己被執(zhí)行表達(dá)式覆蓋：“if”語句中條件布爾表達(dá)式的覆蓋情況路徑覆蓋：由“if”和 “Case”語句構(gòu)成的所有可能的路徑是否己被驗(yàn)證。變量覆蓋：信號(hào)或地址的覆蓋情況，是翻轉(zhuǎn)覆蓋的擴(kuò)充。FSM代碼覆蓋 43基于模擬的驗(yàn)證衡量方法功能覆蓋率：由用戶定義的、反映在驗(yàn)證過程中被運(yùn)行到的功能點(diǎn)的范圍的衡量方法。功能點(diǎn)可以是對(duì)用戶而言可視的體系結(jié)構(gòu)特點(diǎn)，也可以是主要的微結(jié)構(gòu)特征。通常情況下，這些特征不能從實(shí)現(xiàn)中自動(dòng)生成，因此需要在驗(yàn)證testbench中的一些規(guī)范。功能覆蓋率數(shù)據(jù)一般是一些時(shí)序

23、行為（如總線的交易）和一些數(shù)據(jù)（如交易源、目的和優(yōu)先級(jí)等）的交叉組合。附加覆蓋率信息可以從功能覆蓋率點(diǎn)的交叉引用中得到。比如，在一個(gè)器件的兩個(gè)引腳之間進(jìn)行的數(shù)據(jù)處理的相互關(guān)系，或者在一個(gè)處理器中指令和中斷的關(guān)系等。 44基于模擬的驗(yàn)證衡量方法period1 period2BUG RATETime（effort） ready to ship ship？Bug rate with code coverage45基于模擬的驗(yàn)證的問題RTL模擬： 一個(gè)月 一個(gè)月功能仿真：一天 一個(gè)月電路仿真：一分鐘 一小時(shí)芯片： 一秒 一分鐘Validity Test：108矢量Boot Unix：1010矢量46形

24、式驗(yàn)證 形式驗(yàn)證：利用數(shù)學(xué)方法對(duì)設(shè)計(jì)結(jié)果的功能進(jìn)行驗(yàn)證。由于它依賴于對(duì)設(shè)計(jì)的數(shù)學(xué)分析，因此無需使用驗(yàn)證測試向量。目前包括如下幾種技術(shù)： 模型檢查定理證明形式等價(jià)檢驗(yàn) 47模型檢查模型檢查將設(shè)計(jì)描述及其部份規(guī)范的特性作為輸入，以證明該設(shè)計(jì)是否具有某種特性。其過程是搜索一個(gè)設(shè)計(jì)在所有可能條件下的狀態(tài)空間，尋找不符合某特性的點(diǎn)，如果找到這樣的點(diǎn)，則可證明該特性不正確。 模型檢查不需要設(shè)置任何驗(yàn)證測試，所需驗(yàn)證的特性以隊(duì)列形式用特性說明語言描述。當(dāng)模型檢查工具發(fā)現(xiàn)一個(gè)錯(cuò)誤，工具可從初始狀態(tài)開始，進(jìn)行完全的狀態(tài)跟蹤，直至出錯(cuò)的狀態(tài)。48定理證明在定理證明的過程中特性被表述為數(shù)學(xué)命題，而設(shè)計(jì)則表述為數(shù)學(xué)實(shí)

25、體，該實(shí)體表示為若干公理。證明的過程就是看數(shù)學(xué)命題是否可從公理中演繹得到。如果得到，則該特性存在；否則，該特性則不存在。 定理證明的主要缺點(diǎn)：用戶必須用定理證明器的命令來構(gòu)造證明過程；當(dāng)證明結(jié)論為不成立，只能用人工方法分析其原因，不能自動(dòng)跟蹤。 49 靜態(tài)時(shí)序分析（STA）：發(fā)現(xiàn)使芯片時(shí)序失效和對(duì)芯片性能起決起決定作用的電路關(guān)鍵路徑。 性能驗(yàn)證：時(shí)序分析ClkD1Q1bD2CQ250 在同步時(shí)序電路中，2個(gè)寄存器之間組合電路延遲之和（建立時(shí)間、保持時(shí)間、寄存器間的信號(hào)傳播延遲）決定了最大時(shí)鐘頻率。設(shè)其中： setup=20ns； hold=30ns；not（b）=15ns；and（d）=25n

26、s；則從D1 到 D2 Total delay =20+30+15+25=90nsClkD1Q1bD2CQ2Clk性能驗(yàn)證：時(shí)序分析51性能驗(yàn)證：時(shí)序分析建立時(shí)間（setup）：信號(hào)S1高電平相對(duì)S2上升邊之前應(yīng)保持穩(wěn)定的時(shí)間。保持時(shí)間（hold）： 信號(hào)S1 高電平相對(duì)S2上升邊之后應(yīng)保持穩(wěn)定的時(shí)間。S2holdsetup hold 時(shí)間為從clk到來時(shí)，D Q 的傳輸時(shí)間，Setup為防止時(shí)鐘歪斜等不定因數(shù)S152 長路徑錯(cuò)誤設(shè)其中： setup=20ns； hold=30ns； not（b）=15ns； and（d）=25ns；則從D1 到 D2 Total delay =20+30+1

27、5+25=90ns要求： 時(shí)鐘周期 90ns 頻率 1/90 11MHz如 時(shí)鐘周期 90ns 即發(fā)生長路徑錯(cuò)誤：setup違背性能驗(yàn)證：時(shí)序分析53 短路徑錯(cuò)誤 由于時(shí)鐘歪斜（skew）太大而引起，在一個(gè)周期內(nèi) 信號(hào)穿過兩個(gè)寄存器，從而產(chǎn)生邏輯錯(cuò)誤clk1clk2Q1Q2”Q2性能驗(yàn)證：時(shí)序分析54靜態(tài)時(shí)序分析（STA）STA工作原理：采用窮盡分析方法，提取出所有時(shí)序路徑計(jì)算信號(hào)在這些路徑上的傳播延遲檢查信號(hào)的建立和保持時(shí)間是否滿足時(shí)序要求通過對(duì)最大路徑延遲和最小路徑延遲的分析，找出違背時(shí)序約束的錯(cuò)誤。 STA優(yōu)點(diǎn)：如果采用模擬的方法，由于輸入矢量的局限性，可能無法檢查出某些路徑存在的時(shí)序失

28、效STA不要求輸入矢量，能很快得到分析結(jié)果，節(jié)省了很多的設(shè)計(jì)時(shí)間。 55性能驗(yàn)證：后仿真56集成電路設(shè)計(jì)的驗(yàn)證方法學(xué) 驗(yàn)證規(guī)劃 驗(yàn)證和設(shè)計(jì)分離原則 周密的驗(yàn)證計(jì)劃設(shè)計(jì)驗(yàn)證方法學(xué)：根據(jù)不同性質(zhì)的項(xiàng)目可以采用不同的驗(yàn)證方法學(xué)。抽象級(jí)和模型：定義設(shè)計(jì)的各個(gè)抽象級(jí)，以及相應(yīng)的說明和 實(shí)現(xiàn)，以便決定采用合適的驗(yàn)證技術(shù)。此外，要準(zhǔn)備好驗(yàn)證時(shí)所需的相應(yīng)的合適電路模型。驗(yàn)證技術(shù)和工具：不同層次的驗(yàn)證需要選用不同的技術(shù)及其相應(yīng)的EDA工具。驗(yàn)證測試：不同抽象級(jí)的驗(yàn)證相應(yīng)有不同的測試，關(guān)鍵是要產(chǎn)生各種測試程序、如何應(yīng)用這些測試程序，以及測試程序如何在各層次中移植等。構(gòu)成測試的元素應(yīng)包括：測試激勵(lì)：對(duì)于動(dòng)態(tài)模擬，可

29、以是各種類型的測試向量，而對(duì)于形式驗(yàn)證，則要定義設(shè)計(jì)的特性和約束等。測試檢查器：包括期望的測試響應(yīng)、協(xié)議、黃金模型等。測試評(píng)估：包括能力測度，如運(yùn)行時(shí)間、存儲(chǔ)器規(guī)模等，以及質(zhì)量測度，如功能覆蓋、代碼覆蓋等。驗(yàn)證流程：往往是迭代的和并行的，而非單調(diào)和串行的。此外包括驗(yàn)證的跟蹤，所發(fā)現(xiàn)的設(shè)計(jì)錯(cuò)誤處埋以及驗(yàn)證文檔等。 57驗(yàn)證方法學(xué)：自頂向下的驗(yàn)證方法 (1)系統(tǒng)級(jí)驗(yàn)證：系統(tǒng)的行為由頂層系統(tǒng)說明規(guī)定，系統(tǒng)的行為用行為模擬測試程序進(jìn)行驗(yàn)證。然后系統(tǒng)映射到合適的體系結(jié)構(gòu)，利用IP模塊進(jìn)行硬件和軟件劃分。該體系結(jié)構(gòu)的功能和性能用系統(tǒng)行為模擬中建立的測試程序進(jìn)行驗(yàn)證。系統(tǒng)級(jí)的測試程序還不是時(shí)鐘精度和引線精度

30、上的測試。但系統(tǒng)級(jí)的測試程序應(yīng)當(dāng)能轉(zhuǎn)換為適當(dāng)?shù)母袷?，供硬件RTL模擬和軟件驗(yàn)證使用。(2)SOC硬件RTL驗(yàn)證：通過系統(tǒng)設(shè)計(jì)，得到硬件RTL代碼和測試程序，然后進(jìn)行RTL硬件功能驗(yàn)證，包括Lint檢查、邏輯模擬、代碼覆蓋分析、基于事務(wù)的驗(yàn)證、形式模型檢驗(yàn)等。(3)SOC軟件驗(yàn)證：軟件驗(yàn)證中，軟件和測試文件從軟件設(shè)計(jì)團(tuán)隊(duì)得到，并針對(duì)系統(tǒng)設(shè)計(jì)中得到的軟件設(shè)計(jì)說明進(jìn)行軟件驗(yàn)證。根據(jù)驗(yàn)證要求，軟件驗(yàn)證和軟/硬件集成驗(yàn)證可以采用軟件原型、快速原型、仿真、軟/硬件協(xié)同驗(yàn)證等方法。 58(4)網(wǎng)表驗(yàn)證：RTL設(shè)計(jì)經(jīng)綜合后，得到門級(jí)網(wǎng)表，門級(jí)設(shè)計(jì)驗(yàn)證可采用RTL-門級(jí)形式等價(jià)驗(yàn)證，保證兩者邏輯上的等價(jià)性。接下來由于時(shí)鐘樹和可測試性設(shè)計(jì)掃描鏈的插入，