TWI322365B - Design verification system for integrated circuit design and computer program product thereof - Google Patents

Description

>0^ 九、發明說明： 【發明所屬之技術領域】 本發明係關於積體電路設計之領域，且更特定言之，本 發明係關於積體電路設計驗證系統之領域。 【先前技術】 由於近些年來微處理器及其它大規模積體電路之複雜性 增加，故投入設計驗證中之資源在開發及製造此裝置所需 之總資源中佔據日益增大之百分比。實情上，現將驗證具 有多處理能力之高級微處理器之正確功能性成消耗較之實 際設計裝置而言更多的時間、勞動及其它資源。 在歷史上’功能驗證主要由產生大量測試程式或測試實 例’及在-权擬裝置運作之模擬器上運行該等測試程式組 成》設計者及驗證工程師通常在各種隨機及特定測試產生 T之幫助下手動開發此等測試實例。由於積體電路中之電 日日體功月b、暫存斋及其它設備之數目增加故藉由簡單 ，增加模擬之測試的數目來回應習知驗證方法。不幸的 疋，產生看似無限數目之測試為一驗證複雜電路中所有組 件之功能性的低效率且不可靠之方法。 在微處理器開發初期，因為測試空間之尺寸（例如藉由微 處理器可呈現之狀態數目加以量測）相當小，故容忍了功能 驗證系統中之低效率。此外，初期微處理器通常具有較之 現代微處理器而言更少之功能單元，且組件與功能之間的 =互作用被很好地理解及控制。自驗證角度而言，微處理 器中之功能單元之增加之數目係顯著的，此係因為不可再 99024.doc 1322365 忽略或僅藉由習知驗證方法來不精確地驗證功能 的相互作用》 a 採用現代積體電路之多種應用使得不可能預知及計劃將 … 在其上運行之軟體應用類型，且因此在該領域中運用之狀 … 態及相互依賴性相當大且通常為不確定性的。粗略而言， 微處理器之賴空間約等於2n，纟中η表示微處王里器内鎖存 器（狀態儲存裝置）之數目。自此近似應瞭解，隨著鎖存器數 Φ 目增加，微處理器之測試空間按指數規律增加。 其中藉由簡單地增加所模擬之測試的數目來驗證裝置中 增加之複雜性的習知功能驗證方法，正快速變得不可行。 此外，因為在習知驗證過程中模擬器之輸入僅為大量確定 性測試或隨機產生之測試，故必須精心地評估模擬之輸 出，以判定一特定模擬在測試裝置之所需功能性中是否成 功。 添加至執行功能驗證所需之成本及時間的為於設計過程 • 中所做出的不可避免之設計修正。由於新功能性進入，由 於矯正設計缺陷，由於對設計執行综合最佳化以符合時序/ 尺寸約束，及由於添加例如測試邏輯之普遍功能故複雜 積體電路之設計在其開發中通常多次演化（ev〇ive)。無論變 化多小，除非證明變化及其微不足道，否則通常有必要在 每次設計改變時重新執行驗證過程。當迫使有必要重新驗 證之設計變化出現於接近設計階段結束（意即接近”設計定 案（tape out)"、’’芯片驗證（first silic〇n)”或在完成設計之任 何其匕重要步驟中）時，重新驗證設計所需之時間尤其為有 99024.doc 1322365 限的。 因此需要建構一種從事上述設計驗證之測試驗證系統。 【發明内容】 一般而言，本發明涵蓋一用於驗證積體電路設計之模組 化系統及一唯一對應檢查機制。該模組化系統包括一為執 行對應檢查而特別設計之驗證引擎或模組，該對應檢查適 用於在一設計變化之後的使用。結合一模組化驗證系統， 諸如 Baumgartner 等人之題為 Use of Time Step Information in a Design Verification System的同在申請中之專利申請 案，2003年2月20曰申請之美國專利申請案第10/371,002號 (本文中稱為’002申請案）中所揭示之系統，倂入一對應檢查 模組提供一機制，藉由該機制可再次使用執行於一特定設 計之先前型式上的驗證結果以減少在一設計修改之後驗證 設計所需之資源。儘管'002申請案係關於使用及受益於特定 設計（意即無設計變化）内之先前驗證成果，但本發明特定地 延伸此概念，以包含設計變化。 在一實施例中，可藉由有效之對應檢查演算法來建構對 應模組，其中藉由"IMPLIES"邏輯取代習知用於驗證（例如） 一舊設計中之節點與一新設計中之節點之間的對應之 "EX0R"邏輯，該"IMPLIES"邏輯取決於將資料被再次應用 於新設計之先前驗證資料之類型（例如，對於其中在先前設 計中已知一目標或節點被命中之狀況而言為一 IMPLIES邏 輯，及對於其中一節點在一舊設計中未被命中之狀況而言 為另一 IMPLIES邏輯）。與習知基於EX0R之對應模型相 99024.doc 1322365 比，IMPUES邏輯更易於模擬（較少邏輯元件）及評估。 【實施方式】 現轉至圖式，圖1為適於同本發明之—實施例共同使用之 - 設計驗證系統100之所選部分的概念說明。在所描繪之實施 • 射，系統100含有與，002申請案中所述之系統⑽相同之許 多元件。因此’舉例而言’系統100包括一設計驗證構架 102。構架1〇2包括一與藉由系統使用者加以調用之一或多 • 個應用程式101進行通信之介面。構架102係進一步組態成 提供驗證問題至在圖丨中識別為根引擎1〇4之驗證引擎。該 驗證問題it f包括-電路結構之網路清單或另—合適表 示，及一或多個電路網路之將被證明或驳斥的一組期望 值。若狀態中之一狀態或序列在一（多個）指定電路網路上產 生一期望值’則證明該期望值。 構架102產生（對其進行實體化）通常由使用者經由應用 程式101加以界定之—或多個序列中之一組驗證引擎的實 _ 例。該等實體化引學通常以具有一或多個驗證分枝之樹狀 架構進行配置，其中自該等一或多個驗證分枝可分裂出其 它分枝。在此樹結構之頂點處為一自構架102接收驗證問題 之根驗證引擎104。構架1〇2控制分枝中之驗證引擎間的驗 證問題之流程。 如圖1所說明的，構架102係組態成經由應用程式1〇1與使 用者相互作用，以產生一或多個驗證分枝105,該等驗證分 枝中每一者包括在圖i中藉由參考號1〇4、1〇6及ι〇8加以表 示的一或多個驗證引擎之一使用者界定序列。每一驗證引 99024.doc 1322365 擎係組態成模擬積體電路之運作（狀態變化）及評定（assess) 杈型對一或多個屬性之忠實度。可藉由構架ι〇2加以實體化 或加以調用之驗證引擎包括修正引擎1〇6及決笨引擎⑺8。 如其名稱所暗示的，修正引擎106係組態成修正（且推測為 簡化）特定驗證問題，同時決策引擎1〇8用於經修正或未經 修正之驗證問題，以試圖解決問題或提供關於電路模型之 其它資訊。與本申請案對驗證設計變化之強調重點相一 致，根據本發明之一實施例之決策引擎1〇8可包括一對應引 擎，其係设計以驗證特定電路或設計之兩個模型之間的對 應或等效。 構架102將一或多個驗證分枝1〇5令每一者應用於驗證問 題。在每一分枝105内，可藉由—或多個修正引擎1〇6修正 驗證問題，直至最終該分枝以一表示特定分枝上之最末引 擎的”葉（leaf)”引擎終止為止。葉引擎通常為試圖解決驗證 問題之決策引擎108。 在構架102將一驗證分枝1〇5應用於驗證問題之後，葉引 擎通常已為所接收之驗證問題識別至少一反例跡線，或已 證明無反例跡線為可能的，意即已證明該問題為正確的。 假設特定分枝105中之葉引擎成功解決了特定問題（例如該 葉引擎產生至少一反例跡線或證明該問題之正確性），則其 隨後將結果（例如所發現之跡線或"正確"結果）傳遞至其父 引擎（parent engine)(其最初接收驗證問題之引擎）。該父引 擎隨後負責修正所接收之結果，以將任何修正反映至網路 清單上，該網路清單係產生於由該引擎在其將該網路清單 99024.doc 10 傳遞至葉引墼二 所修正之跡始别。因此在修正結果之後，父引擎隨後將 正該傳遞至其自身之父引擎，該父引學進-步修 擎104傳°逖 Μ其初始之修正等等，直至結果自根引 傳谕I口至構架102為止。以此方式，自每-分枝105 相-I至構架102之結果將與藉由構架102產生之網路清單 =處理^問題期間，驗證引擎可學習某些驗證相關之 實情可使其它引擎更簡單地解決-(多個)驗證問 予習了此實情之引擎通常將所學資訊傳播至1父 2子引擎(子引擎為一引擎在其處理問題後將驗證問題 所至的引擎，――葉引擎為驗證分枝中之最末子引擎 不具有子引擎）。每__此等引擎或模組接著將向其個別父 弓I擎及子引擎傳遞所學資訊。以此方式，將在整個樹狀配 置中傳播所學資訊。因此，如圖1所說明的，自根弓丨擎104 傳遞至每—子引擎⑽之資訊可包括驗證問題以及所學之 關於設計之實情。自子引擎106傳遞回至根引擎104之資訊 可包括通過/故障資訊、一或多個反例跡線，及所學實情。 現參看圖2，其描述了設計驗證系統100之一模組化實施 例之額外詳細内容。圖2所說明之系統〗〇〇之元件包括藉由 一些或所有驗證引擎產生時步資訊，及結合使用一對應引 擎而在該等引擎間共用此資訊，該對應引擎使得（例如）自先 前設計提取之驗證資訊及時步資訊能夠以一關於所需運作 資源有效之方式應用至新設計或經修改之設計。 為強調此等元件’圖2描繪了構架102、根驗證？丨擎1〇4 99024.doc 1322365 及識別為引擎1(111)、引擎2(112)、引擎3(113)及引擎4(114) 之一組四個附屬驗證引擎。驗證引擎1〇4及ηι至114係調用 以評定電路模型對可由使用者預定或指定之一或多個屬性 的忠實度。可將每一弓丨擎建構為如上所述之修正引擎或決 策引擎。此外，每-驗證引擎係特^組態成接收及傳輸一 對應於經驗證之設計之形式的所學資訊，其可被隨後引擎 用以簡化或縮短該隨後引擎所執行之驗證。

在一尤其適用於設計變化之情形中的實施例中，附屬驗 證引擎111至114 t的-個係對應引擎。在此實施例中，除 |〇02申請案中描述之時步f訊及直徑f訊以外，驗證引擎間 共用之資訊包括：指示積體電路之第—模型與該積體電路 之第二模型之間的功能對應的對應資訊。極有可能積體電 路之第-模型表示設計之先前或舊修正，同時第二模型表 示該設計之新修改。對應資訊制於射在舊設計上達成 之驗證結果是否適用於新設計。 每-驗證引擎可接收時步及直徑資訊，且執行—驗證任 務，而無論該驗證任務為轉換任務、決策任務或其組合。 每一此引擎可隨後視所執行之驗證任務改變時步及直彳=資 訊（若適當），且將已更新資訊傳輸至下一引擎。每一驗=引 擎可使用時步及直徑以消除冗餘之驗證處理。冗餘驗^處 理包括在-時步期間檢查先前已經檢查之屬性違背，及勿、 略"大於:’完全驗證設計所需之時步之最大數目的時步二 外，可藉由說明舊設計與新設計之關於處於考量+之驗μ 測試的功能對應來調用對應引擎以再次使用先前驗證成且 99024.doc •12- 1322365 果。因此’舉例而言，若斜 π β ^ 對售6又计之模型所執行之驗證成 果已徹底模擬了 Ν個時步，則一告宁 ' 月疋對應測_試暗示了不需要 驗證新設計之第一 Ν個步帮。以此方 以此方式’對應引擎使得對設 計變化再次使用先前驗證成果。 為說明在本發明揭示内容申 μ谷ΐ所強調之元件，結合圖2所述 之系統_之實施例描述了例示性驗證過程。考慮—設計過 程’其中指；t-設計’且使用嘗中請案中所述之模組化驗 證方法進行廣泛驗證，該模έ 保，·且化驗證方法包括時步、直徑 及其它資訊在各種驗則擎間的傳遞，以最小化驗證設計 所祕之育源。在此廣泛驗證之後，回應自驗證測試所學 之資訊、回應添加額外功能性，^於任何眾多其它原因 而改變該設計。 通常，就大多數鎖存；5 i & Μ 4 # y圣貝仔盗及其匕设汁特徵在先前（舊的）及 經修正（新的）設計中為相同的意義上而言，考量中之設計變 化為微小的。在此等狀況下’自然地假設自功能角度而言 舊設計與新設計很大程度上為相㈣。不幸的是’與引入 -具有功能缺陷或缺點之晶片相關聯的成本如此顯著，以 致晶片製造商必須廣泛驗證甚至微不足道之設計變化。 因此6才又入顯著努力以有效驗證兩個類似但不相同之 设計的功能等效。通常將此類型驗證稱為對應檢查❶如上 所述，習知對應檢查係藉由產生—㈣應訊號加以執行， 其t每-對應訊號反映一複合節點之值(狀態)，該複合節點 為舊設計中之節點與新設計中之對應節點的EX0R之產 物。若將一普通組之刺激物（stimulus)應用於舊設計及新設 99024.doc 1322365 係判定為與舊設計402中之節點404功能地對應，且新設計 412中之節點416係判定為與舊設計402中之節點406功能地 對應。進一步假設先前驗證成果，意即對舊設計402(或對 舊設計402之功能等效處理器）所執行之驗證成果說明了其 中斷言節點404之至少一狀態，同時該等先前驗證成果未顯 示其中斷言節點406之狀態。根據本發明之對應檢查包括使 用第一類型之IMPLIES邏輯408來產生第一複合節點409(亦 稱為第一對應節點）以確認舊設計402之節點404與新設計 412之節點414之間的功能對應，及使用第二類型之 IMPLIES邏輯418來產生第二複合節點419(亦稱為第二對應 節點）以確認舊設計402之節點406與新設計412之節點416 之間的功能對應。 若一者可證明（例如使用對應演算法）不可斷言作為第一 類型IMPLIES邏輯408之輸出的第一複合節點409，則此指 示不存在其中斷言（TRUE)舊設計402之節點404且不斷言 (FALSE)其提出之新設計412之等效節點414的狀態。因為對 舊設計402執行之先前功能驗證工作證明了其中斷言節點 404之一狀態的存在，故肯定對應結果暗示了新設計41 2中 之亦可斷言（TRUE)節點414之狀態的存在。若說明不可斷言 作為第二類型IMPLIES邏輯418之輸出的第二複合節點 41 9，則此結果指示複合設計401中不存在節點416為TRUE 且節點406為FALSE的狀態。因為對舊設計402執行之先前 驗證成果未發現其中斷言節點406之狀態，故在此狀況下之 肯定對應結果暗示了若一者將對新設計4 1 2執行等效驗 99024.doc 15 132230^ 證’則其將不會發現其中斷言節點416之狀態。因此證明 H斷言複合節點（例如彻或419)藉由允許再次使用來自 舊设計402至新設計412之先前驗證工作之結果而節省了總 … ㉟也犄間，5亥等先前驗證工作之結果包括說明可斷言一節 _ . 永不可斷言一節點，或在Ν個時步中不可斷言一節點之 結果。舉例而言，若先前驗證結果徹底驗證了來自一些初 始條件之10個時步且對應引擎說明了兩個設計之功能對 φ 應，則可將先前驗證結果應用於新設計，從而使得不需要 再次驗證新設計之時步〇至9，藉此節省了潛在之可觀驗證 責源。當然，若對應檢查導致斷言一複合節點（4〇9或4ι 9中 任者），則否定對應結果防止了對應先前驗證結果之再次 使用。 現返回至圖2，其描繪了模組化驗證系統i 〇〇之一實施 例，其中所描繪之實施例強調將一對應引擎倂入該系統。 最初，驗證問題130係藉由構架1 〇2加以界定且被提供至根 φ 引擎104。驗證問題BO包括設計之一些形式之描述、處於 考量中之輸入的界定，及待驗證之屬性之界定。待驗證之 屬性可表示為一達成特定狀態之特定節點。設計描述通常 為網路清單、VHDL描述’或該設計之一些其它合適描述。 每一驗證引擎111至114係組態成自另—引擎（父引擎）接 收驗證問題（諸如驗證問題130)，及當被執行或運行時執行 其關於該問題之所界定任務。在所描缯·之實施例中，根引 擎104對於引擎111、113及114而言為父弓丨擎。驗證引擎之 所界定任務可包括：轉換任務，其中以一些方式簡化電路 99024.doc 16 1322365 模型或驗證任務，及決策任務，其中於一些經界定參數（諸 如時步數目）内檢查現有模型。此外，驗證引擎丨丨3之所描 繪之實施例之所界定任務為對應任務（意即驗證引擎113之 所描繪之實施例為對應引擎）。 每一模組化驗證引擎1U至114係進一步組態成將驗證問

題傳遞至另-引擎（其子引擎），且#其子引擎完成其驗證處 理時自該子引擎接收回驗證結果。驗證結果可包括反例跡 線、對永不可斷言一節點之完全證明、所學事情，及/或所 驗證之時步及設計直徑評估。每一引擎lu至114隨後將接 收之驗證結果傳遞回至其父引擎。在所描繪之實施例中， 引擎對於引擎⑴而言為子引擎，同時如所描繪之引擎 ⑴及114不具有子引擎1此，引擎1U係組態成接收與已 藉由引擎112加以處理之驗證問題有關的資料，且將所接收 之資料向上傳遞回至根引擎丨〇4。

如先前所建議的，在引擎113為對應引擎之實施例中，祀 引擎HM及-或多個引擎⑴、112及114可各自經組態成^ 其相互傳遞驗證問題時在彼此之間傳遞時步及直捏資$。 類似地，將時步及直徑資訊自子引擎傳播至其父：擎：在 此實施例中，一或多個驗證引擎包括-直徑評估引擎。如 犧申請案所描繪的，直徑評估引擎為謹慎地評估（意即， 问估）時步數目之上界的引擎，須完全列舉該等時步以正 驗證設計。完全列舉係指模擬電路可呈現之每—可能狀： 的過裎。當驗證引擎評估電路在一時步中可 〜 能狀態時，完全列舉該時步。 之——可 99024.doc 除直徑資訊以外，根引擎104及一或多個引擎111 ' 112及 Π4可經組態成完全列舉一預定數目之時步的積體電路模 型。此外，根引擎104及驗證引擎lu至114中每一者係組態 成相互傳播直徑及時步驗證資訊。因此，每一驗證引擎係 組態成接收時步及直徑資訊，其可將該等時步及直徑資訊 用以簡化其所執行之驗證。推測地，每一驗證引擎'，改良” 時步及/或直徑資訊，或對其不予理會。時步資訊中之改良 • 為所驗證之時步數目之增加，然而直徑資訊中之改良為所 '平估直彳坐之減少，此係因為需要增加所驗證時步之數目及 減少所需時步之最大數目的評估。 每一驗證引擎可使用時步及直徑資訊以最小化驗證資 源。作為一實例，若所驗證之徹底時步數目超出所評估之 直徑，則可推斷一電路屬性為正確的。徹底驗證之時步的 數目可包括前向時步分量及後向時步分量。在此狀況下， 僅需要徹底驗證時步分量中的一個超出所評估之直徑。當 •則徹底搜尋演算法時，發生驗證資源減少之另一實例。 該演算法不需要在已檢查之時步期間（意即，在具有小於時 步前向資訊及時步後向資訊中較大者之值的時步期間）檢 查指定屬性之真或假因此’若已向前徹底驗證6個時步， 同時已向後徹底驗證10個時步，則隨後y擎不需要在時步〇 至9期間驗證電路屬性。 返回至圖2所描繪之特定實施例，構架1〇2傳輸一驗證問 題，其中DIAMETER係評估為VERY LARGE (例如2R)，且 前向（FWD)及後向（BCK) TIME STE#數係初始化為〇。由 99024.doc -18- 1322365 於調用了系統100中每一引擎，故其將在内部適當地更新其 之此等三個參數之記錄。當一引擎隨後將問題傳遞至子引 擎時，父引擎將向子引擎傳播該等參數之當前值。類似地， 當一引擎自其子引擎接收到驗證資料（包括此等三個參數） 時，其將適當地更新其之此等資料内部值（意即，若該值小 於其先前保持之值，則記錄藉由子引擎加以報告之 DIAMETER，且若彼等值大於其先前保持之值，貝丨J記錄藉 由子引擎加以報告之FWD及BCK TIME STEP)。該引擎將隨 後將此等參數之任何改良（較低DIAMETER、較高FWD或 BCK TIME STEP)向上傳播至其父引擎（所描繪實例中之根 引擎1 04)。最終，構架102將該等參數之最佳判定值歸檔。 若執行一隨後運行，則該執行將以所歸檔之參數值作為初 始值而開始。 在圖2所描繪之強調在設計變化情形下之驗證的實施例 中，最左側驗證分枝301 (該分枝包括引擎111及112)表示系 統之第一”運行”，其係關於一特定設計（亦稱為舊設計）之第 一修正而執行。中間驗證分枝302表示該系統之第二運行。 分枝302為一包括對應引擎113之對應驗證分枝，在將設計 之第一修正變為該設計之第二修正（新設計）之後調用該對 應引擎11 3。中間驗證分枝302之目的為判定關於舊設計所 達成之驗證結果是否適用於新設計，且較佳使用比簡單地 對新設計再次執行驗證分枝301所需之資源顯著較少之驗 證資源而產生此判定。最右側驗證分枝303表示該系統之第 三運行，該第三運行期間達成額外驗證（除藉由最左側驗證 99024.doc -19- 300 分枝301達成之範圍以外的驗證範圍） 可將圖2所描緣之過程定性描述如下。通常，一者將使用 (例如），_申請案中所述之系統對設計執行廣泛驗證。所有 此"先前"驗證工作係藉由分枝3〇1在圖2中#以表示。隨後 將此驗證之結果(時步資訊、跡線、正確性之證明等等)歸 標。在設計變化後’-者將執行藉由分枝術加以表示之" 對應檢查”，且試圖證明對應邏料何斷言I若此證明 成功/可將先前驗證結果自舊設計直接應用於新設計。 更特定言之’在對應檢查證明不可斷言相關聯之對應邏輯 時’可將舊結果再次應用於任何節點。關於所有其它對應 邏輯（意即，未被結論性地證明為不可斷言之對應邏輯）而 言，舊結果不可被再次應帛。在對聽查完成之後，分枝 3〇3表示較佳使㈣如搬巾請案巾所述之系統對新設計執 行之額外驗證檢測。 假設（例如）驗證引擎U1為一在6個時步中對舊設計執行 有限後向徹底搜尋的轉換引擎。執行後向搜尋以試圖在其 轉換期料^屬性之不正確。假設未在6料步内解決問 題，則來自驗證引擎lU之電路模型輸出連同INF〇2〇1 一起 被傳遞至其子引擎’即驗證弓丨擎112。此處，INF〇2〇i指示 後向時步之最大數目為6’ _前向❹之數目及直徑仍分 別保留其預設（初始）值，〇及2 R。 引擎2(112)可為在20個時步中執行有限前向搜尋之驗證 引擎。當執行此驗證處理時，引擎2(112)藉由在其列舉時步 0至5期間不檢查屬性違背而利用ΙΝρ〇 。若引擎（1 η)不 99024.doc •20- 1322365 能在其20個時步内證明或驳斥一屬性，則其藉由以2〇作為 前向時步數目而更新時步資訊，且將此資訊作為INF〇 2〇2 傳遞回至引擎1(111)，其中1?貿1)為2〇,3(；^為6，且所評估 之直徑仍為2R。引擎1(111)將INF〇 2〇3傳播回至根引擎 104，其中 INFO 203 與 INFO 202相同。

在產生一設計變化之後，根引擎1〇4隨後將舊設計之快照 (snapshot包括於INFO 204甲）傳遞至對應引擎！^。資訊 204可包括用以指示哪些目標或節點在舊設計中被命中，指 示展示舊設計上所命中節點的任何可用除錯跡線（kb% trace) ’扎不哪些節點未被命中之資料，及用於未命中節點 之範圍資料。資訊204進-步包括新設計之模型，且可能包 括為驗證分枝3(H中舊設計而判定之任何時步及直徑資訊。 如以下參看圖4進-步描述的，對應引擎113之一實施例 使用舊設計快照及新設計m產生—包㈣設計及新 設計之複合模型。該複合模型包括經料㈣Μ個設計 之對應目標或節點之間的不—致之對應訊號。對應引擎⑴ 隨後傳回-指㈣由驗證分枝3㈣成之驗證結果對於新 設:而言是否有效之結果_⑽5)。若驗證引擎ιΐ3判定 先前驗證結果有效’則判定於驗證分技3(Π中之包含任何時 步及直經資訊的先前結果被轉遞至驗證分枝3〇3且被其使 口村不贫明之部分建馗 祕、 構為—組電腦可執行指令（竟即朝 «£)，該等電腦可執行指令件儲 ^ f儲存於電腦可讀媒體上，諸如 動悲或靜態RAM元件、非揮 卞訌圧課體，诸如磁碟、 99024.doc 丄 w 軟碟& §己憶體、磁帶等等。在此—實施例中> 當執行軟體之各種部分時，該等各種部分執行® 2所描徐之 積體電路設計驗證處理’其包括如中請案中所述之料 驗證處理。關於本發明對驗證設計變化之強調重點而言， 軟體可包括對應驗證軟體，當被執行時，該對應驗證軟體 執行圖4之流程圖中所描繪之對應驗證過程或方法500。 一在所描繪之實施例中，過程5〇〇包括作為預備步驟之對— 没汁之第-修正（舊設計）執行（步驟5〇2)設計驗證。此處理 表丁圖2中所把緣之驗證處理3〇 1。驗證處理產生驗合登并 果5〇4。此後，藉由對舊設計執行一或多個修正來產生該： 計之第二修正（新設計）。隨後編譯（步驟506)新設計並清除 新設計之所有驗證資料。 在所描繪之對應驗證方法5〇〇實施例中，對新設計模擬 (步驟綱）發現於舊設計驗證期間之任何除錯跡線以達成一 些快速範圍。在假設兩個設計大體上類似且功能上等效或 接近之情況下，命中舊設計上節點的除錯跡線可能命中新 設計上之對應節點。若命中此等節點，則模擬先前設計除 錯跡線在發現新設計上之命中節點方面為有效的。若另一 方面-或多個舊設計除錯跡線未產生命中節點，則先前設 計驗證之模擬在驳斥^個設計之間的對應方面為有效的。 若舊除錯跡線之模擬解決了所有節點，如步驟51〇中所判 定的’則將舊驗證結果應用於新設計（步驟511)。若在步驟 508之後-或多個節點仍未解決’則產生一包括舊設計及新 設計之複合翻（步㈣2)1複合模型可在對應節點上使 99024.doc -22- 1322365 用如對等效檢查傳統使用的EXOR邏輯，或在一較佳實施例 中，將使用IMPLIES邏輯，而非對於對應檢查所使用的 EXOR邏輯。 • _旦產生了複合模型，則當對新設計模擬舊除錯跡線 時，可基於步驟508中所達成之範圍而進行一些模型簡化。 具體言之，可自電路模型移除（步驟514)在步驟5〇8中於新設 計中被命中之任何舊設計節點（因為已說明在新設計中命 Φ 中節點之能力）。此外，複合設計之簡化可藉由自該複合設 計消除（步驟516)任何舊設計節點加以達成，其中由於該等 舊設計節點之逐增驗證將為無意義的，故其不達成驗證範 圍。 在複合模型簡化之後，為簡化之後仍保留之所有目標產 生或建置（步驟5 1 7)複合目標。每一複合目標係設計以指示 舊όχ s·}·中之節點或目標與新設計中之對應節點或目標之間 的功能差異。可藉由傳統EXOR邏輯建構複合目標。或者， # 如圖5所描繪的，複合目標之產生（5 1 7)可使用如以上關於圖 3所述之IMPLIES邏輯，以產生複合或對應訊號。在此實施 例中’步驟517包括使用一藉由圖3中之參考號408加以表示 之OLD AND NOT (NEW)類型之IMPLIES邏輯為在舊設計 中被命中之在步驟516之後仍保留之任何節點而產生（步驟 5 18)—複合節點。其次，使用一藉由圖3中之參考號418加 以表示之NOT (OLD) AND NEW類型之IMPLIES邏輯為在 舊設計中未命中之在步驟5 16之後仍保留之任何節點而產 生（步驟520)—複合節點。 99024.doc •23- 1322365 返回圖4,在產生了對應目標之情況下，隨後執行對應驗 證（步驟522)。較佳地，使用有效對應檢查演算法來執行使 用複合模型之對應驗證。當就所存器數目或電位狀態而言 之複合設計401 (圖3)尺寸基本上為舊設計或新設計尺寸之 - 兩倍時，存在能有效解決對應問題之演算法。例如各種已 知之組合等效檢查演算法能夠極有效地執行等效檢查。當 舊設計與新設計極為接近等同時，此尤其正確，舊設計與 參 新没計極為接近等同在當設計變化傾向於微小時的成熟設 計情形下通常為適當假設。 在對應檢查問題完成之後，可將已證明為不可達到（意即 永不斷言訊號）之任何對應訊號（諸如來自圖3之IMplieS邏 輯408、418之輸出訊號）、與舊設計中之訊號有關之任何舊 驗證結果應用（步驟524)至新設計中之對應訊號。以此方 式’方法500能夠判定一設計之兩個型式之間的等效。因為 方法500之較佳實施例使用較典型用於習知對應模型之 • EXOR^輯而言更不複雜且更容易的IMPLIES邏輯，故方法 5〇〇更佳能夠解決對應問題。 热習受益於此揭示内容之此項技術者可明顯看出本發明 涵蓋一種用於驗證積體電路之設計的方法及系統。應瞭 解’在詳細描述及圖式中所展示及描述之本發明形式係僅 作為目前較佳實例。希望將以下申請專利範圍廣泛理解成 包含所揭示較佳實施例之所有變化。 【圖式簡單說明】 圖1為說明根據本發明之一實施例之概括設計驗證流程 99024.doc -24· 1322365 的方塊圖； 圖2為概念化設計驗證系統’其中特定驗證資訊被輸送至 模組化驗證引擎及自該模組化驗證引擎輸送特定驗證資 ' 訊’以簡化或縮短驗證過程； - 圖3说明了用於本發明之對應檢查技術之一實施例中的 IMPLIES 邏輯； 圖4為說明根據本發明之一實施例之對應檢查過程的流 | 程圖；且 圖5說明了根據本發明之一實施例之圖4流程圖的詳細内 容。 雖然本發明易受各種修正及替代形式之影響，但在圖式 中以實例之方式對其特定實施例加以展示，且將在本文中 進行詳細描述。然而應瞭解，本文所呈現之圖式及詳細描 述並非用以將本發明侷限於所揭示之特定實施例，相反 地，本發明將涵蓋位於藉由附加申請專利範圍加以界定之 • 本發明精神及範疇内的所有修正、等效物及替代物。 【主要元件符號說明】 設計驗證系統 101使用者/應用程式 102設計驗證構架 104根引擎 105驗證分枝 106修正引擎 108決策引擎 99024.doc •25· 1322365

111 附屬驗證 引 擎 112 附屬驗證 引 擎 113 附屬驗證 引 擎 114 附屬驗證 引 擎 130 驗證問題 201 INFO 202 INFO 203 INFO 204 INFO 205 INFO 301 驗證分枝 302 驗證分枝 303 驗證分枝 401 複合設計 402 舊設計 404 節點 406 節點 408 第一類型 IMPLIES 邏 輯 409 第一複合 A-Ar 即 點 412 新設計 414 節點 416 節點 418 第二類型 IMPLIES 邏 輯 419 第二複合 Λ/r 即 點 99024.doc -26

Claims (1)

1322365 第094103528號專利申請案 -_文申請專利範圍替換本(98年8月）_* ^ 十、申請專利範圍： 1. 種積體電路設計之設計驗證系統，其包含： 第驗引擎，其係組態成模擬一積體電路之一第 設計之運作’及評定賴型在其運作之N個時步期 屬性之忠實度； ，B . 用於記錄及傳播該N值之構件； 對應引擎，其係組態成判定該積體電路之該第― 6十與5玄積體電路之該第二設計之間的功能對應；及 j應該對應引擎判定該第—設計之至少―節點與該第 一设計之—對應節點之該功能對應而使用該所傳播之N =減少在該積體電路之該第二設計之隨後分析期間所 耗費之貧源的構件，其中該隨後分析驗證在大於N 期間該第二言免計對該屬'!·生之忠實度。 y 2. 如請未項1之系統，其中使用該傳播之N值以減少所耗費 :::包r藉由該第一驗證引擎達成之驗證結果應用 詨第一：：。十中之每一節點’該節點係判定為具有對於 〇设計中之一個別節點的功能對應。 3. =求項2之系統，其中該對應引擎組態成判定該第一設 對二ΓΓ與該第二設計中之一對應節點之間的功能 」產生—複合模型，該複合模型包括-具有一藉 ~第一設計中之該節點及該第_ 曰 夕灿吁 Λ弟—6又叶中之該個別節點 ;二以判定之狀態的複合節點，及監視該複合節 設計；6亥複合節點之斷言否定了該第-設計與該第二 〇又。之該等節點之間的該功能對應。 99024-980826.doc 1 if Γ ‘一 .υ ί一一 ---------------' 4.如請求項3之系統，其中該對應引擎係進一步組態成使用 一舊設計之任何除錯跡線模擬一新設計，且藉由消除該 新設計中之在該模擬期間被命中之任何節點，及移除對 應於舊設計節點之任何複合節點來簡化該複合模型，其 中對於該等舊設計節點而言未達成驗證範圍。 5 .如請求項4之系統，其中判定該第一設計中之一節點與該 第二設計中之該對應節點之間的功能對應包括當將一普 通組之輸入應用至該第一設計及該第二設計時，產生一 具有一獨佔值之EXOR節點或產生該第一設計中之該節 點及該第二設計中之該節點的產物。 6. 如請求項4之系統，其中該第一設計中之該節點係展示為 藉由該第一驗證引擎加以命中，且進一步其中判定該第 一設計中之一節點與該第二設計中之該對應節點之間的 功能對應包括當將一普通組之輸入應用至該第一設計及 該第二設計時產生一 IMPLIED節點，當且僅當該第一設 計中之該節點為ASSERTED且該第二設計中之該對應節 點為NOT ASSERTED時，該IMPLIED節點被斷言。 7. 如請求項4之系統，其中該第一設計中之該節點未展示為 藉由該第一驗證引擎加以命中，且進一步其中判定該第 一設計中之一節點與該第二設計中之該對應節點之間的 功能對應包括當將一普通組之輸入應用至該第一設計及 該第二設計時產生一 IMPLIED節點，當且僅當該第二設 計中之該節點為ASSERTED且該第一設計中之該對應節 點為NOT ASSERTED時，該IMPLIED節點被斷言。 99024-980826.doc

8 · 種用於驗證一積體雷玫々-»·4· 办n,„ 檟粒電路之设计之電腦程式產品，嗜程 式產品包含一電腦可讀媒體，其包含： ^ ^ 第一驗證引擎碼構件，其模擬一積體電路之―第― 計之運作，及評定該模型在其運作之關時步期間對—屬又 性之忠實度； @ δ己錄及傳播該ν值之碼構件； 對應碼構件，其用於判定該積體電路之該第一 該積體電路之-第二設計之間的功能對應；& 〜、 回應該對應碼構件判定兮笛 ^ 第-〜J 十之至少—節點與該 弟一 6又计之一對應節點之間 值换夕工門的5玄功旎對應，而使用該所 傳播之N值以減少在該積 ^ ^ ^ ^ 电峪之该第一设汁之隨後分 間所耗費之資源的碼構件，其中該隨後分析驗證在 $ ^之時步期間該第二設計對該屬性之忠實度。 值以減=8之電月自私式產品’其中該用於使用該傳播之N 驗：引^所耗費之資源的碼構件包括用於將藉由該第-==構件達成之驗證結果應用至該第二設計中之 定為且有對碼構件’其中該第二設計中之每-節點係判 心對於該第一設計中之—個別節點的功能對應。 項9之電腦程式產品’其中該用於減少所耗費之資 源·的碼構件包括者列兴乂 I ' 田+ 時步中該積體電路之 故計之狀態時’省略屬性違背檢查。 11·如請求項8之電 中之―式產。σ ’其中該用於判定該第-設計 Τ之即點盥該筐-洲斗士 、苐一 6又计中之一對應節點之間的功能對 構件包括用於產生1合節點之碼構件，該複合 99024-980826.doc 節點具有一藉由該第一設計中之該節點及該第二設計中 之該對應節點之狀態加以判定的狀態。 1 2.如請求項11之電腦程式產品，其中該第一設計中之該節 點係展示為藉由該第一驗證引擎碼構件加以命中，且進 一步其中該用於判定該第一設計中之一節點與該第二設 計中之該對應節點之間的功能對應之碼構件包括用於當 將一普通組之輸入應用至該第一設計及該第二設計時產 生一 IMPLIED節點之碼構件，當且僅當該第一設計中之 該節點為ASSERTED且該第二設計中之該對應節點為 NOT ASSERTED時，該IMPLIED節點被斷言。 1 3.如請求項11之電腦程式產品，其中該第一設計中之該節 點未展示為藉由該第一驗證引擎碼構件加以命中，且進 一步其中該用於判定該第一設計中之一節點與該第二設 計中之該對應節點之間的功能對應之碼構件包括當將一 普通組之輸入應用至該第一設計及該第二設計時產生一 IMPLIED節點，當且僅當該第二設計中之該節點為 ASSERTED且該第一設計中之該對應節點為NOT ASSERTED時，該IMPLIED節點被斷言。 1 4.如請求項11之電腦程式構件，其中該用於判定該第一設 計中之一節點與該第二設計中之該對應節點之間的功能 對應之碼構件包括當將一普通組之輸入應用至該第一設 計及該第二設計時，產生一具有一獨佔值之EXOR節點或 產生該第一設計中之該節點及該第二設計中之該節點的 產物。 99024-980826.doc 1322365 年月修正替換頁 ' 1 5. —種積體電路設計之設計驗證系統，其包含： 用於產生一積體電路之一第一設計與該積體電路之一 第二設計之一複合設計的構件； 其中該複合設計包括至少一具有一藉由該第一設計中 之一節點及該第二設計中之該對應節點之狀態加以判定 之狀態的對應節點； 其中該對應節點呈現一關於該第一設計及該第二設計 0 中之該等節點的IMPLIED關係，其中當該第一設計中之 該節點呈現一在一先前驗證中被驗證之狀態，同時該第 二節點中之該對應節點未展現一在一先前驗證中被驗證 之狀態時，該對應節點被斷言；及 用於試圖判定該對應節點是否能夠被斷言之構件。 1 6.如請求項1 5之系統，其中當且僅當該第一設計中之該節 點為TRUE且該第二設計中之該對應節點為NOT (TRUE) 時，該對應節點被斷言。 ^ 1 7.如請求項1 5之系統，其中當且僅當該第一設計中之該節 點為NOT (TRUE)且該第二設計中之該對應節點為TRUE 時，該對應節點被斷言。 1 8.如請求項1 5之系統，其進一步包含用於自一經組態成模 擬該第一設計之至少一第一節點之行為的第一驗證引擎 接收一驗證結果之構件，及用於當該對應節點經判定為 ' 不能被斷言時將該驗證結果應用至該第二設計中之一第 一節點的構件。 19.如請求項18之系統，其中該第一驗證引擎驗證在N個時步 99024-980826.doc 1322365 皐8.戽·條正替換頁1 中該第一設計之該第一節點之該行為。 20.如請求項19之系統，其中將該驗證結果應用至該第二設 計之該第一節點包括忽略在該第一 N個時步期間該第二 設計之該第一節點之屬性檢查。 99024-980826.doc 6- 1322365 第094103528號專利申請案 中文圖式替換頁(97年3月） 十一、圖式： 97年3.月7』日修正替換頁 100

決策引擎 108 決策引擎 1 2 驗證分枝 105 j „ <驗證分枝罱 1 105 99024-970327.doc