摘 要

隨著硬件設(shè)計復(fù)雜度的激增，驗證已被廣泛認(rèn)為是制約整個芯片設(shè)計流程的瓶頸?；?a target="_blank">仿真的驗證通常通過生成一系列滿足特定布爾/位向量約束的隨機激勵驗證設(shè)計行為。在該驗證方法學(xué)中，驗證效率很大程度上取決于產(chǎn)生合法激勵的約束求解器的性能。 ?

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

簡 介

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

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

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

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

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

一些挑戰(zhàn)

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

?
圖1. 例1 ?

SAT增強的字級求解器

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

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

?
圖3 求解流程

01

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

02

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

03

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

04

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

圖4 例1的命題骨架 ?

試驗結(jié)果

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



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

結(jié)論與展望

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