本文节选自ISEDA2023入选论文《A SAT Enhanced Word-Level Solver for Constrained Random Simulation》。
摘 要
随着硬件设计复杂度的激增，验证已被广泛认为是制约整个芯片设计流程的瓶颈。基于仿真的验证通常通过生成一系列满足特定布尔/位向量约束的随机激励验证设计行为。在该验证方法学中，验证效率很大程度上取决于产生合法激励的约束求解器的性能。
本文我们首先讨论了字级求解器在求解包含特定操作符(如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求解器产生的大部分布尔变量赋值可能并不满足原始约束，如何更高效地剔除这些无效的布尔变量赋值，将会是我们下一步研究的重点。
