|
眾所周知，功能驗證在芯片的整個(gè)設計周期中占用的時(shí)間最多。盡管目前有許多技術(shù)可用于減少驗證時(shí)間，但最終應當如何選擇？答案并不簡(jiǎn)單明了，而且經(jīng)常令人迷惑并要付出高昂的代價(jià)。 一個(gè)項目中需要使用的工具和技術(shù)必須在設計周期的初期就確定下來(lái)，以便獲得新驗證方法費用預算的準確信息。經(jīng)常有公司因為錯誤估計了運轉這些新型工具和技術(shù)所需的設計和技術(shù)的復雜性而浪費大量的資金和資源。 產(chǎn)品的抽象級越高，越容易設計；同樣的，抽象級越高，越容易犯嚴重的錯誤。一個(gè)架構上的缺陷可能會(huì )導致整個(gè)芯片的損害，而在門(mén)級網(wǎng)表中的連線(xiàn)錯誤可以通過(guò)重制解決。 例如，Verilog為設計者提供了一種相對容易的接口，以便他們在相當抽象的層次上進(jìn)行設計。當設計曾經(jīng)作為制約性的瓶頸時(shí)，Verilog 為設計生產(chǎn)率帶來(lái)了指數增長(cháng)，并且大大推動(dòng)了復雜芯片的發(fā)展。但是如果設計者不了解在復雜的設計周期中語(yǔ)言上的細微差別，就很容易犯錯。在驗證成為瓶頸的今天，同樣的觀(guān)點(diǎn)也適用于許多驗證技術(shù)和語(yǔ)言。 本文將對時(shí)下流行的驗證技術(shù)(形式驗證、隨機、定向、有約束的隨機、斷言、屬性檢驗)與語(yǔ)言(SystemC、C/C++、SystemVerilog、Open-VERA、E等)進(jìn)行全面評述，還將分析在傳統的數字ASIC設計流程中應當在何時(shí)采用何種驗證技術(shù)和語(yǔ)言。 1 驗證瓶頸 盡管事實(shí)表明如今設計生產(chǎn)率的增長(cháng)速度仍然低于芯片復雜度的增長(cháng)速度，然而現在需要面對的瓶頸已不再是設計時(shí)間，而是驗證時(shí)間。最近的統計數據表明，對一個(gè)復雜邏輯芯片而言，整個(gè)產(chǎn)品周期中 60_70% 的時(shí)間都用于驗證工作。如何使用新的工具和技術(shù)對設計中的復雜功能進(jìn)行驗證已經(jīng)成為縮短總體的產(chǎn)品時(shí)間所需要面對的挑戰。 由于以下原因，可以說(shuō)驗證瓶頸在某種程度上是設計抽象級逐步提高造成的結果： 1) 在較高的抽象水平上進(jìn)行設計，易于構建高度復雜的產(chǎn)品功能。設計復雜度的提高造成驗證工作的成倍增加； 2) 在設計、轉換以及映射到最終產(chǎn)品的過(guò)程中，應用更高的抽象級進(jìn)行設計會(huì )帶來(lái)信息損失和解釋錯誤的問(wèn)題。例如，采用HDL級設計并將其轉換到門(mén)級的綜合過(guò)程，需要進(jìn)行驗證以確保轉換的正確性以及使設計意圖完全得到體現。提高抽象級還帶來(lái)了代碼解釋問(wèn)題，在仿真時(shí)要通過(guò)這些代碼對設計進(jìn)行描述，以確保所寫(xiě)的代碼真實(shí)反映了功能規范。 其它影響驗證問(wèn)題的因素還包括： 1) 由于設計中硬件與軟件、模擬與數字等共存而造成的功能復雜度增加； 2) 對系統可靠性的要求增高，使得對驗證工作的要求也增加，以確保在系統環(huán)境下，芯片功能可以順利執行。 統計數據表明，驗證問(wèn)題現實(shí)存在，而且讓公司付出了高昂的成本： 1)由于設計錯誤造成的芯片缺陷：在需要進(jìn)行重制的芯片中，有82%是由于邏輯與功能缺陷設計錯誤。這意味著(zhù)驗證過(guò)程沒(méi)有覆蓋邊角情況，缺陷一直隱藏在設計過(guò)程中直到流片。 2)由于規范錯誤造成的芯片缺陷：在需要進(jìn)行重制的芯片中，有47%是由于邏輯與功能規范不正確或不完整，有32%是由于規范發(fā)生了改變。 3)重用IP和外來(lái)IP的問(wèn)題：所有失敗的芯片中，有14%是由于在重用或外來(lái)的IP中存在錯誤。 4)重制的后果：重制費會(huì )高達10萬(wàn)美元，還會(huì )延誤產(chǎn)品的推出，由于使用這些有缺陷的芯片而導致的系統失敗也會(huì )增加成本。 為了提高驗證生產(chǎn)率，EDA行業(yè)提出了一個(gè)與解決設計瓶頸類(lèi)似的解決方案——抽象化的理念。諸如 Verilog 和 VHDL 等高層次的語(yǔ)言被用于驗證芯片，這些語(yǔ)言包括各種指令如任務(wù)指令和線(xiàn)程指令(fork/join 語(yǔ)句)，以及控制結構(while語(yǔ)句)。這提供了更強的數據控制力，以便對所有邊角設計進(jìn)行充分驗證。然而，這些指令不能被綜合，因此不會(huì )被用作實(shí)際設計代碼的一部分。 隨著(zhù)復雜度與日俱增，能夠驗證具有不同抽象級的復雜設計的新語(yǔ)言被創(chuàng )建出來(lái)，支持這些新的驗證語(yǔ)言的技術(shù)和工具也隨之誕生。 所有這一切意味著(zhù)芯片廠(chǎng)商必須對新的工具作出評估，必須針對這些新的工具和技術(shù)對工程師進(jìn)行培訓，在公司的研發(fā)費用成本結構中必須包括新的工具和資源，公司在總體上必須在短時(shí)間內克服學(xué)習曲線(xiàn)問(wèn)題，另外，還需要對這些工具進(jìn)行風(fēng)險評估，以及考慮新工具與已有技術(shù)的集成和協(xié)同工作的能力。 2 驗證與確認(Validation) 除了驗證問(wèn)題之外，芯片公司還要面對確認時(shí)間問(wèn)題。Kropf將“確認”定義為“通過(guò)檢查實(shí)現行為以獲得對規范的信心的過(guò)程”。在驗證和確認之間，有一種觀(guān)點(diǎn)認為，“確認能夠確保這是正確的設計，而驗證則是確保這個(gè)設計是正確的”；另外一種觀(guān)點(diǎn)認為，“驗證指硅片成為成品之前的測試(Verilog/VHDL 仿真等)，確認指硅片成為成品之后的測試(在實(shí)驗室里測試電路板上的芯片)”。 無(wú)論是確認還是驗證，若要保證硅片滿(mǎn)足規范要求，要完成以下兩個(gè)步驟：1)通過(guò)文件或建模，芯片規范得到了正確的解釋?zhuān)?)以上解釋得到了正確的理解與實(shí)現(一般是通過(guò) HDL)，綜合入硅片，并封裝成為芯片。 本文認為第二步是驗證，第一步是確認。目前業(yè)界流行的設計流程如圖1所示，此流程可保證以上兩個(gè)步驟的要求得以滿(mǎn)足。根據待實(shí)現功能的復雜程度不同，可以跳過(guò)一些步驟或者增加一些步驟。例如，如果某一項設計是純粹面向硬件的，不涉及驅動(dòng)或軟件，那么可以從抽象級3直接跳到抽象級1，鎖相環(huán)設計即為一例。 當設計按照抽象級逐步推進(jìn)時(shí)，要注意必須一直保持等效性，以確保最低層的抽象級能滿(mǎn)足系統規范的要求。例如： 1)當 C 模型被置于一個(gè)系統環(huán)境并能夠滿(mǎn)足規范中所描述的所有系統要求時(shí)，芯片規范(一般是一個(gè)文本文件)與其 C 模型之間就達到了等效。這在實(shí)質(zhì)上是功能等效。 2)通過(guò)比較 C 模型與HDL 實(shí)現的輸出，可以在規范的C 模型與其 HDL 實(shí)現之間建立等效關(guān)系。在沒(méi)有 C 模型的情況下，可使用“期望數據模型”。這在實(shí)質(zhì)上也是功能等效。 3)HDL實(shí)現與門(mén)級(綜合后的)之間通過(guò)應用“邏輯等效性檢驗”可以建立等效關(guān)系。這時(shí)，由于設計采取的形式是純粹的邏輯門(mén)，而且功能能夠被表示為邏輯表達式，因此，這在實(shí)質(zhì)上是邏輯等效。 3 現有驗證技術(shù)及發(fā)展趨勢 目前可使用的驗證方法及技術(shù)如圖2所示。 3.1 動(dòng)態(tài)功能驗證 使用最為廣泛的功能驗證方法是動(dòng)態(tài)的，之所以被稱(chēng)為動(dòng)態(tài)是因為輸入圖形/激勵信號是在一段時(shí)間(幾個(gè)時(shí)鐘周期)內生成并應用于設計的，相應結果會(huì )被用于與參考/黃金模型進(jìn)行比較，以檢驗其與規范之間的一致性。 仿真器通常用于計算所有的信號值，并將其與指定的期望值進(jìn)行比較。目前，有兩類(lèi)可供選擇的仿真器： 1)基于周期的仿真器：這類(lèi)仿真器不管在時(shí)鐘周期內發(fā)生了什么事情，它只是在每個(gè)周期內對單脈沖信號進(jìn)行一次求值，由于執行時(shí)間很短這類(lèi)仿真器的速度通常很快。 2)基于事件的仿真器：這類(lèi)仿真器在時(shí)鐘周期內或者在時(shí)鐘邊界捕獲事件，并在設計中傳播這些事件，直到系統達到穩態(tài)。 3.2 隨機/定向功能驗證 在一個(gè)有時(shí)間限制的仿真過(guò)程中，動(dòng)態(tài)仿真器只能驗證芯片的典型行為，而不能驗證所有可能的行為，這是動(dòng)態(tài)仿真的主要缺陷。出現這個(gè)問(wèn)題的主要原因是對芯片的定向測試是針對已知的測試空間，而不是未知的測試空間進(jìn)行的。即使是僅對已知測試空間的測試也要花費很長(cháng)時(shí)間。例如，假設推出每個(gè)運算數需要一個(gè)時(shí)鐘，為了驗證一個(gè)能對兩個(gè) 32 位操作數進(jìn)行加和運算的簡(jiǎn)單加法器的測試空間就需要 232x232個(gè)時(shí)鐘周期。隨著(zhù)邏輯運算越來(lái)越復雜，驗證空間也會(huì )相應增加。因此出現了隨機動(dòng)態(tài)仿真，通過(guò)為設計提供隨機激勵信號來(lái)增加驗證的測試空間，這樣能夠使驗證覆蓋的功能空間最大化。但當設計規模很大且非常復雜時(shí)，隨機測試空間會(huì )變得無(wú)限。為了解決這個(gè)問(wèn)題，更高級的驗證語(yǔ)言，如 Open-VERA、E 與SVL (SystemC 驗證庫)被推出。這些語(yǔ)言引入了諸如約束隨機激勵信號、隨機激勵信號分配與電抗性測試平臺等概念。伴隨著(zhù)這些語(yǔ)言的運用，出現了一些用于對其進(jìn)行解釋的工具，如VERA、Specman與 OSCI 內核( Concentric System Studio ，CCSS)。 除了引入隨機化功能以外，新的驗證語(yǔ)言和工具還通過(guò)減少公司在構建不同測試場(chǎng)合/方案所花費的時(shí)間，來(lái)提高生產(chǎn)率。例如，測試方案可以采用最高的抽象級來(lái)編寫(xiě)，并能夠通過(guò)采用功能強大的面向對象型結構而擴展至任何較低的抽象級。 當應用動(dòng)態(tài)驗證時(shí)，通常需要估計所覆蓋的、可以量化的功能空間，包括：經(jīng)過(guò)驗證的代碼行數(行覆蓋率)，經(jīng)過(guò)測試的邏輯表達式個(gè)數(表達式覆蓋率)，一個(gè) FSM 設計中能夠達到的狀態(tài)數(FSM 覆蓋率)，在一個(gè)仿真運行中可以雙向變換的端口及寄存器數目(變換覆蓋率)，以及設計代碼中覆蓋的邏輯通道數目(通道覆蓋率)。以上可以使用 Code Coverage 及 Lint 工具來(lái)實(shí)現。 3.3 斷言 設計者將斷言用作一個(gè)占位符，用來(lái)描述與設計相關(guān)聯(lián)的假設及工作特性(包括暫時(shí)的特性)。如果設計滿(mǎn)足或未滿(mǎn)足規范或假設，則斷言將會(huì )在一個(gè)動(dòng)態(tài)仿真過(guò)程中被觸發(fā)。斷言還可在形式/靜態(tài)功能驗證環(huán)境中使用。 3.4 混合功能驗證 在該方法中通常執行動(dòng)態(tài)仿真，仿真結果被用作靜態(tài)驗證的輸入。在靜態(tài)驗證過(guò)程中，在設計中傳播的是邏輯方程式/符號，而不象在動(dòng)態(tài)仿真中那樣傳遞數值。這種方法雖然不像形式驗證詳盡周全，但卻具有比純動(dòng)態(tài)仿真更高的效率。 3.5 靜態(tài)功能驗證 在靜態(tài)功能驗證中，不向設計施加輸入激勵，而是將設計映射在一個(gè)圖形結構中，用雙擇判決圖(BDD)或其他數學(xué)表示方法來(lái)描述所有時(shí)間周期內的設計功能。利用這種圖形結構來(lái)證實(shí)或反駁屬性可以驗證這些數學(xué)表達式，這是通過(guò)順著(zhù)或逆著(zhù)信號流來(lái)傳遞數值，以確定數學(xué)結構中的矛盾式來(lái)完成的。 現有的工具通過(guò)以下兩種方式來(lái)滿(mǎn)足靜態(tài)驗證市場(chǎng)的需求： 1) 使用斷言：這是在模型/設計當中規范并公式化的設計約束(使用SystemVerilog、Open-VERA、Verilog和VHDL等設計/驗證語(yǔ)言)。 2) 使用屬性：這允許使用屬性語(yǔ)言(如PSL和Sugar)對屬性進(jìn)行規范。 3.6 等效性驗證 為了確認門(mén)級表示法與HDL實(shí)現是相同的，需要實(shí)施等效性檢驗，使用匹配點(diǎn)并比較這些匹配點(diǎn)之間的邏輯。檢驗中會(huì )生成一個(gè)數據結構并比較在相同的輸入模式下得出的輸出數值模式，如果這些輸出數值模式不相同，那么表示法(這里指門(mén)級和RTL級)就不是等效的。當表示法中的一個(gè)經(jīng)過(guò)了某種類(lèi)型的變換時(shí)，等效性檢驗有時(shí)會(huì )在兩個(gè)門(mén)級網(wǎng)表或兩個(gè)RTL級實(shí)現之間進(jìn)行。 造成設計表達式差異的一些實(shí)際原因包括： 1) 綜合算法／探索式方法：根據對綜合工具的約束條件(區域、時(shí)間、功率)不同，綜合工具會(huì )對邏輯運算進(jìn)行優(yōu)化，以得到適當的門(mén)級表式。為此，綜合工具將采用探索式方法和邏輯最小化算法。 2) 抽象級：在采用HDL來(lái)實(shí)現設計時(shí)，由于語(yǔ)言的局限性或是缺乏(不具備)對綜合工具如何解釋特定語(yǔ)言結構并將其變換為門(mén)級表式的預測能力，因此，HDL實(shí)現有可能與設計者意圖存在一定的差異。 4 影響驗證技術(shù)的趨勢和力量 4.1 技術(shù)視角 設計錯誤可能出現在模塊接口處或是在模塊內部，它們最終會(huì )集成在一起形成芯片。舉例而言，那些在模塊級沒(méi)有被發(fā)現的缺陷在應用動(dòng)態(tài)仿真時(shí)會(huì )在子系統或系統級上顯露出來(lái)。使用靜態(tài)功能驗證，模塊開(kāi)發(fā)的每一步都會(huì )得到詳盡的驗證，從而確保子系統/系統質(zhì)量和可靠性從根本上得到提高。有人認為，使用靜態(tài)/形式功能驗證，能夠更快地找到更多的缺陷。 另一方面，使用靜態(tài)功能驗證也存在以下缺陷： 1)現有的工具只能在模塊級運行； 2)通常不能處理大型設計(一般只能處理100~150K的門(mén)電路)； 3)不能處理高度復雜的設計； 4)現有的形式驗證工具有時(shí)會(huì )出現時(shí)間無(wú)限的問(wèn)題(這主要是因為它們往往是基于一套探索程序，而不是任一算法)。這意味著(zhù)形式功能驗證在一些情況下可能會(huì )比動(dòng)態(tài)仿真花費更長(cháng)的時(shí)間； 5)設計必須被寫(xiě)為可綜合的RTL形式。 除了上述技術(shù)上的挑戰外，基于斷言的形式功能驗證的兩個(gè)競爭標準(PSL對SystemVerilog)也帶來(lái)了額外的問(wèn)題。目前傾向于將靜態(tài)功能驗證方法用于驗證足夠成熟以備綜合的模塊，動(dòng)態(tài)驗證(隨機和定向)用于嚴格驗證集成前的模塊。 目前，動(dòng)態(tài)仿真還將繼續主宰功能驗證領(lǐng)域，直到形式驗證工具提供一種更成熟的方法。 4.2 語(yǔ)言視角 可以觀(guān)察到這樣一個(gè)趨勢，就是將設計和驗證語(yǔ)言結合在一起。這將極大地促進(jìn)生產(chǎn)率，改進(jìn)系統可靠性以及提高設計質(zhì)量，因為使用多種工具和語(yǔ)言引發(fā)的不明確和誤解問(wèn)題將得到消除。 在這一結合實(shí)現之前，公司要繼續依賴(lài)現有的高級設計語(yǔ)言(Verilog和VHDL)，并選擇是使用專(zhuān)有驗證語(yǔ)言(Open-VERA、E等)，還是過(guò)去流行的Verilog和VHDL 。 SystemC與其他高級設計描述語(yǔ)言在設計流程中扮演著(zhù)重要角色，其中涉及硬／軟件折衷以及在硬件上運行軟件的設計(如SoC)。另外，它們也可用于架構建模及確認，當可以為應用事務(wù)模型的驗證使用架構模型組件時(shí)，也可以使用 SystemC。 5 選擇正確的驗證方法的標準 在當前縮短上市時(shí)間和迫切要求低成本的環(huán)境下，工程師正在設法解決設計復雜性問(wèn)題。那些在新技術(shù)上投入更多研發(fā)精力的公司，其研發(fā)費用的使用更有效率，產(chǎn)品上市時(shí)間更短，公司成長(cháng)更快，盈利更高。另外，公司必須在其特有需求與核心價(jià)值的基礎上評估方法和技術(shù)。在將新技術(shù)引進(jìn)其工具流程時(shí)，它們應當考慮以下問(wèn)題，并做出適當的權衡。 1)在某個(gè)生產(chǎn)線(xiàn)中，公司是市場(chǎng)領(lǐng)先者還是追隨者？ 2)基礎設施、工具和方法是集中式的還是分布式的？ 3)新驗證技術(shù)的評估是針對第一代產(chǎn)品進(jìn)行的嗎？ 4)新驗證技術(shù)對成本和產(chǎn)品上市時(shí)間有何直接和間接影響？ 5)新的工具能否處理不同的設計能力？ 6)工具的易用性如何？ 7)可為新的工具提供什么水平的文檔和支持？ 8)新的工具和方法與公司內部現有的工具和方法之間是否具有互操作性？ 9)新工具的投資回報率(ROI)如何？(包括在服務(wù)、培訓、咨詢(xún)、計算和人力資源方面的投資) 10)新的工具是否能夠支持處于多個(gè)不同地理位置的設計？ 11)公司需要考慮的問(wèn)題中，最為重要的問(wèn)題之一可能是：我們雇用的設計師和驗證工程師是否對新的工具抱有成見(jiàn)？(即設計師不愿意學(xué)習和接受新的技術(shù)) 公司在做出關(guān)于工具、語(yǔ)言和方法的決策時(shí)可以采用以下介紹的簡(jiǎn)單權衡方法。 5.1 產(chǎn)品視角 主要從事存儲器芯片或存儲器密集型(相對于邏輯密集型而言)芯片生產(chǎn)的公司訝SRAM和DRAM公司可能根本不需要進(jìn)行大量的邏輯驗證。這些芯片大多是定制的。雖然這些產(chǎn)品中有些規模會(huì )很大，但它們的邏輯復雜性并不高，因而不支持在公司內部配備大量邏輯驗證工具的計劃。不過(guò)，存儲器密集型設計在其他方面提出了挑戰，例如布線(xiàn)、工藝變化以及功率等。 那些制造純ASIC芯片，在芯片上不運行任何軟件的公司可能無(wú)須在硬件或是軟件實(shí)現上進(jìn)行權衡或是實(shí)施測試以捕獲運行于硬件之上的軟件。例如，只具有硬件的SERDES芯片所要求的驗證和建模方法與同時(shí)具有硬件和軟件的SoC是不同的。 對于擁有多種產(chǎn)品線(xiàn)的大公司來(lái)說(shuō)，驗證方法必須滿(mǎn)足各種產(chǎn)品的不同要求。 5.2 系統視角 過(guò)去，邏輯芯片供應商不負責對芯片是否滿(mǎn)足參考系統的功能和性能要求進(jìn)行驗證，而如今的系統廠(chǎng)商在批量訂貨之前都要求芯片供應商實(shí)施系統參考驗證。這就要求芯片公司在一個(gè)它們不熟悉的附加抽象級上對芯片進(jìn)行建模和驗證，這需要架構模型、參考模型、復雜應用級的測試以及精細的測試平臺配置。面對這些不同類(lèi)型的挑戰，公司有兩種選擇，一是采用現有的語(yǔ)言、技術(shù)和方法，這將耗費大量的時(shí)間和精力；另一種就是采用新技術(shù)(如VERA、Specman等)。此外，芯片供應商還必須確保所使用的參考模型和驗證套件是在一個(gè)與客戶(hù)的相應模型和套件兼容的環(huán)境中完成的，例如，應用客戶(hù)的軟件開(kāi)發(fā)套件(SDK)和仿真器也能夠進(jìn)行同樣的測試。 5.3 方法學(xué)視角 在芯片集成之前，可以將靜態(tài)功能驗證與動(dòng)態(tài)仿真結合起來(lái)，在一個(gè)高置信度水平上驗證模塊級的功能。通過(guò)確認動(dòng)態(tài)仿真正在持續驗證功能空間的主要邊角，可以有效地實(shí)施系統級驗證。 首先執行隨機仿真可以在驗證的初始階段發(fā)現大量的缺陷，然后對隨機模擬加以約束以確定測試空間已經(jīng)被完全覆蓋的做法或許相對容易一些。應考慮在功能覆蓋度量上對約束驅動(dòng)型驗證進(jìn)行細化。功能覆蓋率這一術(shù)語(yǔ)被用于描述對被覆蓋的功能空間進(jìn)行量化的參數，相反地，代碼覆蓋率則被用于量化一個(gè)給定的測試套件對已實(shí)現的設計進(jìn)行覆蓋的程度。定向仿真隨后可被用于在驗證周期末期覆蓋邊角測試空間。 斷言和屬性可在靜態(tài)功能驗證期間起作用(在模塊級上)，并可在動(dòng)態(tài)仿真環(huán)境中被重用(在模塊級和系統級上)。如果模塊轉變?yōu)镮P，那么斷言和屬性也是有用的，因為斷言將在IP被重用時(shí)持續不斷地檢查其屬性。 6 結語(yǔ) 隨著(zhù)時(shí)間的推移，具有更小特征尺寸(90nm 和 65nm)的器件將投產(chǎn)。目前，公司正在致力于解決諸如布線(xiàn)、串擾和軟錯誤的設計問(wèn)題。一旦這些設計瓶頸得到了解決且隨著(zhù)芯片廠(chǎng)商在越來(lái)越小的芯片上封裝越來(lái)越多的邏輯，驗證問(wèn)題的出現就是意料中的事了。新型工具和方法的不斷引進(jìn)提高了設計生產(chǎn)率。提高設計(SystemC和SystemVerilog)和驗證(Open-VERA、E 和 SystemC)的抽象化程度以滿(mǎn)足日益增長(cháng)的復雜度要求是不可避免的。目前從SystemVerilog 的推出能夠看到設計和驗證語(yǔ)言的融合趨勢。 驗證持續扮演著(zhù)重要角色，它能夠提高產(chǎn)品質(zhì)量，使硅芯片一次成功，從而間接影響總體的產(chǎn)品時(shí)間。SystemC 和建模語(yǔ)言將繼續為邏輯密集型產(chǎn)品提供架構驗證。通過(guò)使用屬性、斷言以及推出形式驗證工具，生產(chǎn)率得到了進(jìn)一步提高。但目前工程師仍舊依賴(lài)并信任動(dòng)態(tài)仿真，因為它能夠驗證大型和高度復雜的設計。最終的趨勢可能是：形式驗證占據主要地位，動(dòng)態(tài)仿真仍用于完整性檢查。 |
