摘 要

隨著硬件設計復雜度的激增，驗證已被廣泛認為是制約整個芯片設計流程的瓶頸。基于仿真的驗證通常通過生成一系列滿足特定布爾/位向量約束的隨機激勵驗證設計行為。在該驗證方法學中，驗證效率很大程度上取決于產生合法激勵的約束求解器的性能。 ?

本文我們首先討論了字級求解器在求解包含特定操作符(如IF-THEN-ELSE、IMPLIES和布爾OR)的約束時遇到的挑戰。為了克服這一挑戰，我們引入布爾可滿足性(SAT)求解器剪枝原始約束并壓縮字級求解器的搜索空間。試驗結果表明，在包含這些特定操作符的測試用例中，本文提出的混合求解器比原始的字級求解器平均性能提升約50%。

簡 介

近幾十年來，硬件設計復雜性的快速增長對功能驗證提出了巨大挑戰。隨機約束仿真是當今行業中廣泛采用的功能驗證方法之一，其達到覆蓋率目標所需時間的長短，很大程度上依賴于產生隨機激勵的約束求解器的性能與解的分布的好壞。 ? 目前用于產生隨機激勵的約束求解器主要有三種： ?

/ 01 /? 基于二元決策圖（Binary Decision Diagram, BDD）的求解器。 ?
該求解器通過創建BDD獲取約束的所有解，因而可以輕易產生均勻的分布；然而，由于眾所周知的內存爆炸問題，BDD并不適用于過于復雜的約束。 ?

/ 02 /? 基于值域推斷的字級求解器。 ?
該求解器通過推斷壓縮每個變量的可取值域構成的搜索空間，并反復從搜索空間中隨機取值獲取滿足約束的一組解，具有易于實現、天然隨機性等特性；然而，邏輯推理能力的缺失導致其在求解包含特定運算符（如IF-THEN-ELSE，IMPLIES和布爾OR）的約束上效率低下。

? / 03 /? 基于可滿足性模理論（Satisfiability Module Theory, SMT）的求解器。 ?
該求解器擴展自比特級可滿足性（Satisfiability, SAT）求解器，繼承了SAT在邏輯推理上的優勢，同時，得益于其廣泛的應用，SMT求解器在工業界與學術界獲得了極大的關注，成果頗豐；然而，SMT求解器被設計為求得一組解，因此隨機性較差，且求解包含位向量的約束時需將位向量打散為單個比特，性能受限。 ?

以上三種求解器各有優劣，綜合利用第二、第三種求解器的優勢，可在不犧牲易于實現與天然隨機性的情況下進一步提升性能，是一條極具前景的優化隨機約束仿真的路徑。 ?

一些挑戰

如上所述，基于值域推斷的字級求解器的性能很大程度上取決于推斷結果的好壞，當推斷器無法有效壓縮變量的搜索空間時，該字級求解器變得無效。實踐中，我們發現基于值域推斷的字級求解器在求解包含特定運算符（如IF-THEN-ELSE，IMPLIES和布爾OR）時遇到挑戰。例如圖1所示的約束，由于推斷器并不知道ITE的then分支還是else分支需要被滿足，因此推斷器無法壓縮變量a和b的取值空間。此時，通過給變量a、b隨機賦值的方式，很難從龐大的搜索空間中找出僅有的兩組解。 ? 這種挑戰也可被視作是字級求解器缺乏邏輯推理能力的結果。因此，引入SAT求解器，增強字級求解器的邏輯推理能力，便自然成為一種克服該挑戰的方法。

?
圖1. 例1 ?

SAT增強的字級求解器

圖2. 例1的抽象語法樹 ?

圖2是例1的抽象語法樹表示。從圖2中，我們驚喜地發現，位于關系操作符之上的全是布爾操作符，位于關系操作符之下的則全是位向量操作符。因此，約束問題中存在一個清晰的分界線，將原始問題分割成布爾和位向量兩部分。SAT求解器有極強的邏輯推理能力，特別適合求解布爾約束；基于值域推斷的字級求解器能快速求解位向量約束，尤其是包含數學運算符的位向量約束。約束問題的這一獨特結構，使得充分利用不同求解器的優勢求解約束的不同部分成為可能。具體的求解步驟如圖3所示：

?
圖3 求解流程

01

將關系操作符所代表的位向量表達式替換成不同的布爾變量，構建原問題的命題骨架（例1的命題骨架如圖4）；

02

利用SAT求解器產生一系列滿足命題骨架的布爾變量的賦值；

03

隨機選取一組布爾變量的賦值，并用字級求解器求解其所代表的位向量約束；

04

若第三步有解，則返回該解，若無解則返回第三步，選擇另一組賦值。

圖4 例1的命題骨架 ?

試驗結果

為驗證上述求解策略是否有效，我們用純字級求解器（W Solver）和SAT增強的字級求解器（W-SAT Solver）求解了14個測試用例，其用時如下表所示。



對于布爾操作符占主導的test1至test7，由于引入了SAT，W-SAT求解器的性能得到極大提升，最大為79%，平均約50%；對于位向量操作符占主導的test8至test14，由于增加了額外操作，W-SAT的性能略有下降，平均下降約10%，幾乎可忽略不計。 ? 試驗結果表明，SAT增強的字級求解器繼承了字級求解器在求解位向量操作符占主導時在約束上的優勢，同時，求解布爾操作符占主導的約束時，性能也獲得可觀提升，證明了其求解各種約束的有效性。 ?

結論與展望

在保留易于實現與天然隨機性等特性的前提下，相較于純字級求解器，SAT增強的字級求解器在求解布爾操作符占主導的約束時，性能有顯著提升，求解位向量占主導的約束的性能幾無差別，因此能有效處理多種不同約束。 ? 實踐中，我們也發現當約束過于復雜時，SAT求解器產生的大部分布爾變量賦值可能并不滿足原始約束，如何更高效地剔除這些無效的布爾變量賦值，將會是我們下一步研究的重點。