一種用于隨機(jī)約束仿真的SAT增強(qiáng)的字級求解器

首屆EDA國際研討會（International Symposium of EDA，ISEDA）已在南京落下帷幕。作為國內(nèi)領(lǐng)先的系統(tǒng)級驗(yàn)證EDA解決方案提供商，芯華章受邀出席并深度參與活動各環(huán)節(jié)，不僅受邀參展、發(fā)表主題演講、參與圓桌論壇，并貢獻(xiàn)專業(yè)文章入圍ISEDA2023論文評選，全方位展示了公司在EDA驗(yàn)證領(lǐng)域的深厚積累和專業(yè)洞察。

本文節(jié)選自ISEDA2023入選論文《A SAT Enhanced Word-Level Solver for Constrained Random Simulation》。

摘 要

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

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

簡 介

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

目前用于產(chǎn)生隨機(jī)激勵的約束求解器主要有三種：

/ 01 /? 基于二元決策圖（Binary Decision Diagram, BDD）的求解器。

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

/ 02 /? 基于值域推斷的字級求解器。

該求解器通過推斷壓縮每個變量的可取值域構(gòu)成的搜索空間，并反復(fù)從搜索空間中隨機(jī)取值獲取滿足約束的一組解，具有易于實(shí)現(xiàn)、天然隨機(jī)性等特性；然而，邏輯推理能力的缺失導(dǎo)致其在求解包含特定運(yùn)算符（如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è)計(jì)為求得一組解，因此隨機(jī)性較差，且求解包含位向量的約束時需將位向量打散為單個比特，性能受限。

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

一些挑戰(zhàn)

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

這種挑戰(zhàn)也可被視作是字級求解器缺乏邏輯推理能力的結(jié)果。因此，引入SAT求解器，增強(qiáng)字級求解器的邏輯推理能力，便自然成為一種克服該挑戰(zhàn)的方法。

圖1. 例1

SAT增強(qiáng)的字級求解器

圖2. 例1的抽象語法樹

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

圖3 求解流程

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

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

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

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

圖4 例1的命題骨架

試驗(yàn)結(jié)果

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

對于布爾操作符占主導(dǎo)的test1至test7，由于引入了SAT，W-SAT求解器的性能得到極大提升，最大為79%，平均約50%；對于位向量操作符占主導(dǎo)的test8至test14，由于增加了額外操作，W-SAT的性能略有下降，平均下降約10%，幾乎可忽略不計(jì)。

試驗(yàn)結(jié)果表明，SAT增強(qiáng)的字級求解器繼承了字級求解器在求解位向量操作符占主導(dǎo)時在約束上的優(yōu)勢，同時，求解布爾操作符占主導(dǎo)的約束時，性能也獲得可觀提升，證明了其求解各種約束的有效性。

結(jié)論與展望

在保留易于實(shí)現(xiàn)與天然隨機(jī)性等特性的前提下，相較于純字級求解器，SAT增強(qiáng)的字級求解器在求解布爾操作符占主導(dǎo)的約束時，性能有顯著提升，求解位向量占主導(dǎo)的約束的性能幾無差別，因此能有效處理多種不同約束。

實(shí)踐中，我們也發(fā)現(xiàn)當(dāng)約束過于復(fù)雜時，SAT求解器產(chǎn)生的大部分布爾變量賦值可能并不滿足原始約束，如何更高效地剔除這些無效的布爾變量賦值，將會是我們下一步研究的重點(diǎn)。