摘 要

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

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

簡(jiǎn) 介

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

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

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

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

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

一些挑戰(zhàn)

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

?
圖1. 例1 ?

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

圖2. 例1的抽象語(yǔ)法樹(shù) ?

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

?
圖3 求解流程

01

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

02

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

03

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

04

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

圖4 例1的命題骨架 ?

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

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



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

結(jié)論與展望

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