想象你是一座特大城市负责验收路网的总规划师。过去验证一条新路线是否通畅，得安排测试车辆一辆辆开着跑：启动、转弯、刹车、记录结果。每辆车只能走一条确定的路线，跑一万次也只能验证一万条路线，而城市地图上还藏着数不清的交叉口和支路——这正是传统验证的窘境。如今你换了一个思路：不再派车，而是把整张道路图摊开，用彩色标记在图上标注每条路线需要满足的通行条件。比如“这条匝道要求车辆高度不超过 2 米、右转后直行 500 米”，然后一次性问：“存在一辆能满足所有这些条件的车吗？它长什么样？”这张会思考的“地图”，就是符号执行（Symbolic Execution）的缩影。 符号执行把程序输入抽象成符号变量，不预先指定具体数字，而是沿执行路径收集一条条约束条件，再交给“可行性办公室”——约束求解器（Constraint Solver）来判定：这些条件能否同时成立？若能，就抽取一组具体取值作为测试向量；若不能，就说明这条路根本走不通，立刻在图上剪掉。在硬件验证领域，我们正是用这种方法系统性地探寻未覆盖路径、检查断言反例、验证 RTL 设计与门级网表是否等价。它不能包治百病，却把“盲人摸象式试车”升级为“摊开地图做推演”，让验证工程师第一次能以路径为单位审视整个设计空间。

岗位关联

掌握符号执行，能帮你从“试输入、看波形”的实验派升级为“算路径、查约束”的推理派，在覆盖率分析、断言反例生成和形式化等价检查中系统性地寻找边界缺陷——这是走向形式化验证工程化的重要一步。

目录
  1. 可视化演示
  2. 核心原理
  3. 符号状态建模
  4. 路径约束求解
  5. 路径爆炸缓解
  6. 硬件验证应用
  7. 工程落地实践
  8. AI 应用场景
  9. Python 演示
  10. 常见误区
  11. 面试题

可视化演示

动态演示符号执行技术的核心机制，通过入门/进阶/实战/优化四种模式展示关键概念与交互流程。

本节配有交互动效（进入视口后自动加载，约 3KB）。

符号执行技术：符号执行 符号执行基本原理 路径约束求解机制 核心机制可视化 符号执行技术整体架构与关键组件

核心原理

过去验证一条道路是否通畅，最朴素的办法是派测试车实际跑一遍：挂挡、踩油门、看到路口就转弯。好处是结果真实，坏处也明显——一次只能验证一条具体路线。城市道路的转角一旦多起来，测试车的数量再大也覆盖不了全部组合。符号执行却像把整幅道路图摊开在桌面上，用铅笔在地图上推演所有可能的转弯组合；它不指定车是什么型号，而是让“车”成为一个待定的未知量，一次分析就能同时回答许多条路线能不能走通。

从概念上理解，符号执行就是把程序输入从一个具体数值升级成一个符号变量（比如用 α 表示“某个还不确定的值”）。程序执行时不再有一个固定的输入，而是一路累积“到达当前位置需要满足什么条件”。这种状态下，程序位置、变量取值和到达条件三者共同构成一个执行状态。具体执行只能产生一条路径，符号执行却会像树枝分叉一样，在每次判断处拆出多条候选路径。

这三者合在一起，就构成执行树上的一个节点。整棵执行树就是城市里所有可能行程的完整地图：根节点是程序入口，每个分叉是一次条件判断，每条从根到叶的路径代表一种输入可导致的执行过程。回到路网规划的场景——具体执行好比派一辆辆车去实跑，而执行树则是把整座城市的路线可能性压缩在一张图上，看一眼就知道哪些路段有希望开通、哪些交叉口注定封死。

符号状态: (pc,σ,s)\displaystyle 符号状态:\ (pc, \sigma, s)
  1. 路径条件 pcpc 表示从程序入口到当前状态所必须满足的所有分支约束之和，是判断路径可达性的核心依据。
    pc=c1∧c2∧⋯∧cn\displaystyle pc = c_1 \land c_2 \land \cdots \land c_n
  2. 符号存储 σσ 是一个映射表，把当前可见变量映射到它们的符号表达式，例如 x 被映射成 α、y 被映射成 α+1。
    σ={x1↦e1, x2↦e2, …}\displaystyle \sigma = \{ x_1 \mapsto e_1,\ x_2 \mapsto e_2,\ \ldots \}
  3. 程序计数 ss 指向下一条待执行指令，描述“这辆车现在停在地图的哪个路口”。
    s=next_instruction\displaystyle s = \mathit{next\_instruction}

符号状态建模

规划师在图上一旦开始推演，就要给每条道路做记号。符号执行同样如此：进入程序时，我们把输入变量 x、y 换成彩色符号 α、β，之后的每个算术操作都会生成新的符号表达式。比如执行 y = x + 1，σ 中就多了 y → α + 1；执行 z = x * 2，σ 中就多了 z → α * 2。这一步被称为符号化输入映射，它让程序状态不再依赖具体数字，而是依赖符号之间的关系。

当程序遇到 if (expr) 这样的条件分支时，符号执行的特别之处就显现了：我们同时向两个方向探索。真分支要求表达式成立，所以把 expr = 0 追加进当前路径条件；假分支要求表达式不成立，就追加 expr ≠ 0。这些条件像路线沿途的“通行章”一样不断累积，最终到达某个状态时，路径条件就是这个状态曾经走过的所有分支约束的合取。

路径条件累积得越多，地图上这条路径的“通行资格”就越明确。但路网推演最怕的是路径数量失控——于是有状态合并策略：把多条从地图上看走向相近、约束可以求并的路线合并成一个状态，用“要么满足条件 A、要么满足条件 B”的写法替代两条路径。合并后的状态更粗，却能大幅减少需要维护的地图张数。这就像规划师发现两条支路最终并入同一主干道时，干脆把两条支路画成同一条虚线，先保证主干道的分析顺畅。

pc真=pc∧(expr=0),pc假=pc∧(expr≠0)\displaystyle pc_{真} = pc \land (expr = 0), \qquad pc_{假} = pc \land (expr \neq 0)
  1. 分支表达式求值expr 是当前 if 语句中的条件表达式，它由符号存储 σ 给出，可能本身就是一个包含符号变量的复杂表达式。
    expr=eval(σ,condition)\displaystyle expr = eval(\sigma, condition)
  2. 真分支约束当条件为真时，路径条件必须额外满足 expr 等于 0，于是得到 pc 与等式的合取。
    pc真=pc∧(expr=0)\displaystyle pc_{真} = pc \land (expr = 0)
  3. 假分支约束当条件为假时，路径条件必须满足 expr 不等于 0，两个分支合在一起就覆盖了判断两侧的全部可能性。
    pc假=pc∧(expr≠0)\displaystyle pc_{假} = pc \land (expr \neq 0)

路径约束求解

地图上画出了许多条候选路线，但哪些路线真的存在可行的车辆？这就是“交通可行性办公室”——约束求解器的职责。符号执行把每条路径的约束条件打包成一组数学问题，递交给求解器；求解器回答“可满足”或“不可满足”。可满足意味着存在一组具体输入能走通这条路径，求解器会进一步返回这组输入的具体取值；不可满足则说明这条路径在现实中不可能存在，可以直接从地图上剪掉。

求解器给出的“通行证”正是符号执行生成测试向量的依据：拿到具体取值，验证工程师就可以在真实仿真环境中复现这条路径。相应地，反例生成是它的另一项绝活——如果我们要证明某个属性永远成立，只要找到一条让属性失败的可行路径，求解器返回的模型就是最有价值的反例。这就像一个交警在图纸上发现某条匝道几何上不可能右转，无需真车试驾就能确定方案必须修改。

SAT(pc): x↦c∈Z;UNSAT(pc): 该路径不可达\displaystyle SAT(pc):\ x \mapsto c \in \mathbb{Z}; \qquad UNSAT(pc):\ \text{该路径不可达}
  1. 可满足判定求解器检查路径条件 pc 是否存在至少一组整数赋值使所有约束同时成立，这是路径可行性的“门禁”。
    ∃ c: pc(c)=true\displaystyle \exists\, c:\ pc(c) = \mathit{true}
  2. 模型抽取若可满足，求解器返回一组具体值，如 x = 6，这些值可以直接作为测试输入或反例。
    model={x↦6,y↦7}\displaystyle \mathit{model} = \{ x \mapsto 6, y \mapsto 7 \}
  3. 不可满足剪枝若求解器证明不存在这样的赋值，路径终将不可达，搜索器会放弃该分支，不再继续向下探索。
    ∀ c: pc(c)=false⇒剪枝\displaystyle \forall\, c:\ pc(c) = \mathit{false} \Rightarrow \text{剪枝}

路径爆炸缓解

城市路口越多，可行路线的数量就越疯狂：一个路口分 2 条支路，两个路口就有 4 种走法，三个路口就有 8 种……这种几何级数增长被称为“路径爆炸”。一棵深度很浅的树都能膨胀到天文数字，根本没法逐条展开。规划师必须承认：这座城市的每一条小路都去推演一遍是不现实的，必须学会抓大放小、合并同类项。

面对路径爆炸，业界发展出四类“交通管制”手段。深度优先搜索配合启发式策略，先沿最有希望的目标方向深入，避免在浅层横冲直撞。剪枝与抽象是核心利器：求解器判定不可达的路径直接丢弃；对变量取值范围采用区间抽象，把连续空间粗化为区间，用较低精度换取更快判定。状态合并把走向相似、条件可以求并的路径状态融合成一个，减少并行状态数。并行化执行则把不同分支分配给多个计算节点同时求解，用算力对抗爆炸。这就像规划师在图上主动划掉死胡同、把支路并入干道、再派多支勘测队分头行动，才能在大规模路网中保持分析可控。

N(k)=∑i=0kbi=bk+1−1b−1\displaystyle N(k) = \sum_{i=0}^{k} b^{i} = \frac{b^{k+1}-1}{b-1}
  1. 分支因子 bb 表示每个判定点平均产生的分支数量，通常取 2，因为大多数条件判断只有真、假两个方向。
    b=每个判定点的分支数‾\displaystyle b = \overline{\text{每个判定点的分支数}}
  2. 深度 kk 表示从程序入口到当前状态经历的判定次数，它决定执行树的层级数。
    k=判定点数量\displaystyle k = \text{判定点数量}
  3. 几何级数求和路径总数是从 0 层到第 k 层的所有节点求和，结果随 k 呈指数级膨胀，这正是路径爆炸的数学来源。
    N(k)=bk+1−1b−1≈O(bk)\displaystyle N(k) = \frac{b^{k+1}-1}{b-1} \approx O(b^{k})

硬件验证应用

道路图纸最终要交付给城市验收，硬件验证正是芯片设计流程中的“道路验收环节”。一个 RTL 模块可能有成千上万个状态，随机仿真像随机派车出门，覆盖率基线一高就寸步难行。符号执行则让验证团队换一种打法：把 RTL 中的输入信号变成符号变量，让执行树自动延伸进每一个分支，然后直接问“哪些路径还没被覆盖？”“哪些路径会触发断言失败？”

符号执行在硬件验证中的三个主要落点从此清晰。覆盖驱动验证：覆盖率报告中哪条分支缺口最大，就把哪条分支的路径条件交给求解器生成定向向量，精准补盲。断言属性检查：把断言（如 never x == y && busy）转换成对该路径/状态的可达性查询，若存在可行路径到达非法状态，求解器即生成反例。RTL 等价验证：同一设计在综合前后的实现，被转换成两个符号执行模型，从相同的初始状态出发，检查是否存在某输入使两个模型的输出或状态分道扬镳。等效于规划师拿着两张不同版本的城市地图，要求每一栋楼在两张图上都能从同一路线到达——任何偏差都是必须修正的设计缺陷。

Ccov=∣Pexplored∩Ptarget∣∣Ptarget∣\displaystyle C_{cov} = \frac{|\mathcal{P}_{explored} \cap \mathcal{P}_{target}|}{|\mathcal{P}_{target}|}
  1. 目标路径集合P_target 是由覆盖率标准（如分支覆盖、条件覆盖、状态覆盖）所定义的“必须到达”的路径集合。
    Ptarget={待覆盖路径}\displaystyle \mathcal{P}_{target} = \{ \text{待覆盖路径} \}
  2. 已探索路径集合P_explored 是符号执行实际展开并验证过的路径集合，它们满足各自路径条件下可到达。
    Pexplored={已验证可行路径}\displaystyle \mathcal{P}_{explored} = \{ \text{已验证可行路径} \}
  3. 覆盖率计算覆盖率就是已探索路径与目标路径的交集大小除以目标路径总数，衡量验证工作推进的程度。
    Ccov=∣Pexplored∩Ptarget∣∣Ptarget∣\displaystyle C_{cov} = \frac{|\mathcal{P}_{explored} \cap \mathcal{P}_{target}|}{|\mathcal{P}_{target}|}

工程落地实践

图纸画得再精美，最终还得变成工地上的施工计划。符号执行从论文走向芯片验证流程，需要解决工具、性能和协作三方面问题。工具链的选型就像选择地图软件：是集成到现有验证环境，还是独立运行；是搭配 SMT 求解器处理线性算术，还是需要支持位向量和数组的理论。团队往往从一个小模块试点，度量求解时间、路径数量、覆盖率增量这三个数字，再决定是否推广。

性能调优的策略总结起来是四个字：限深、合并、换元。设置最大探索深度或执行时间预算，超出即停止；将相似路径状态合并，减少 m 的大小；针对问题特征选择更快的求解器或理论域，压缩每个 t_j。与此同时，符号执行并不取代仿真，而是与随机回归形成互补：仿真快速粗扫全局面，符号执行在覆盖率卡住时定点攻坚。验证团队和设计团队也要建立协作机制——验证工程师发现问题路径后，设计团队要能迅速确认这是真实缺陷还是环境约束过紧。最终，符号执行像一支训练有素的勘测队：有限预算、明确主次、按图索骥，把昂贵的算力花在最可能藏缺陷的道路上，让硬件验证从“盲跑”进化成“按图推演”的精确工程。

Ttotal=∑j=1mtj\displaystyle T_{total} = \sum_{j=1}^{m} t_j
  1. 单次求解耗时t_j 表示对第 j 条路径的约束进行求解所花费的时间，这是符号执行性能的基本单元。
    tj=第 j 条路径的求解时间\displaystyle t_j = \text{第 } j \text{ 条路径的求解时间}
  2. 求解次数m 是需要受理的路径数量，它由搜索策略和剪枝效率共同决定。
    m=受理路径总数\displaystyle m = \text{受理路径总数}
  3. 总时间预算总耗时是所有路径求解时间的累加，工程上必须为它设定上限，否则路径爆炸会吞噬整个验证周期。
    Ttotal=∑j=1mtj\displaystyle T_{total} = \sum_{j=1}^{m} t_j

AI 应用场景

覆盖率盲区定向补盲

阶段：覆盖率分析与测试生成

解决的问题：传统随机仿真在覆盖率到达 80% 后，边际收益急剧下降，剩下 20% 的边界路径往往藏有最严重的 Bug。验证工程师只能靠经验手写定向用例，效率低且容易遗漏。

具体案例：某芯片团队的 RTL 模块分支覆盖率卡在 87%，随机回归跑了三天没有进展。团队将未覆盖分支的路径条件输入符号执行引擎，自动生成 120 条定向测试向量，重新仿真后分支覆盖率升至 96%，并顺带发现了一个只有在特定总线握手时序下才会触发的死锁缺陷。

断言反例自动生成

阶段：形式化属性验证

解决的问题：设计团队写下若干断言属性（如“总线占用期间地址不允许变化”），但用手工构造反例极其耗时，常常要数天才能定位一个反例。

具体案例：形式化验证工程师将断言取反后，用符号执行从初始状态开始搜索到达非法状态的路径条件；求解器返回一组输入序列，仿真器立即复现了断言违例波形。原本预计一周的反例调试，缩短到半天完成，设计师也因此确认了状态机缺少一条边界转移。

RTL 与门级网表等价检查

阶段：综合前后等效性确认

解决的问题：RTL 经过逻辑综合、扫描链插入和时钟树综合后，网表与原始设计可能因优化引入行为差异。逐节点比对在大型设计上计算量巨大，而只做随机对比又无法证明等价。

具体案例：EDA 工具团队用符号执行分别对 RTL 和网表建立符号状态模型，从相同初始条件同步执行；在一款 DSP 核心的综合网表检查中，工具在 40 分钟内找到一条导致输出高阻态不一致的路径，定位到某条扫描链 DFT 逻辑在测试模式下改变了数据通路。

Python 演示

python74 行
# 符号执行微型演示：# 用符号变量表示输入，沿分支累积路径条件，# 最后用区间求解器判断每条路径是否可达。 class Sym:    """符号变量：支持构造比较约束"""    def __init__(self, name):        self.name = name     def __gt__(self, v):        return ('gt', self.name, v)     def __lt__(self, v):        return ('lt', self.name, v)  def feasible(conds):    """区间求解器：检查所有约束的取值区间是否相交"""    lo = -10**9    hi = 10**9    for op, _name, val in conds:        if op == 'gt':            lo = max(lo, val + 1)        elif op == 'lt':            hi = min(hi, val - 1)        elif op == 'ge':            lo = max(lo, val)        elif op == 'le':            hi = min(hi, val)    return lo <= hi, (lo, hi)  def negate(op):    """分支取反：把 gt 转成 le，把 lt 转成 ge"""    return {'gt': 'le', 'lt': 'ge', 'ge': 'lt', 'le': 'gt'}[op]  x = Sym('x')# 程序片段：if x > 5:#                 if x < 3:  ...   (不可达)#                 else:      ...#           else: ...# 每条分支用 (比较符, 符号变量, 常量, 真分支pc, 假分支pc) 表示prog = [    ('gt', x, 5, 1, 4),    ('lt', x, 3, 2, 3),    ('halt',),    ('halt',),    ('halt',),]  def explore(pc, conds):    """符号执行引擎：到达中止点时调用求解器判定可达性"""    if pc >= len(prog) or prog[pc][0] == 'halt':        ok, rng = feasible(conds)        if ok:            print('路径可达，x 的可行取值区间:', rng)            return 1        print('路径不可达，剪枝')        return 0    op, var, val, t_pc, f_pc = prog[pc]    left = explore(t_pc, conds + [(op, var.name, val)])    right = explore(f_pc, conds + [(negate(op), var.name, val)])    return left + right  def main():    reached = explore(0, [])    print('符号执行最终覆盖可达路径数:', reached)  if __name__ == '__main__':    main()
目的：用约 80 行实现一个可运行的微型符号执行器，演示路径条件累积与约束求解剪枝的核心思想。
  1. def feasible(conds)约束求解器的简化实现，通过检查取值区间是否相交判断整条路径是否可满足。
  2. def negate(op)分支取反逻辑，生成条件判断为假时对应的约束。
  3. prog = [...]用元组描述程序的指令序列，每条分支记录真/假两个跳转目标。
  4. def explore(pc, conds)符号执行递归引擎，遇到 halt 指令后调用求解器，否则向真、假两个分支继续探索。
  5. left = explore(t_pc, conds + [(op, var.name, val)])递归进入真分支时，把原判断条件追加到路径条件中。
  6. right = explore(f_pc, conds + [(negate(op), var.name, val)])递归进入假分支时，把取反后的判断条件追加到路径条件中。
  7. if ok: print('路径可达...')求解器判定可达性后输出具体取值区间，对应真实场景中生成测试向量。

常见误区

误区我以为把输入换成符号，程序跑一遍就能自动拿到所有路径和答案，不需要做任何取舍。

正解符号执行不会自动穷尽一切。路径爆炸使完整枚举在现实程序中几乎不可能，必须配合搜索深度限制、时间预算、剪枝和状态合并。它更像规划师摊开地图推演，而不是一台全知机器；能系统地探索大量路径，但一定要人工设置探索策略。

为何常见：教学演示通常展示小规模例子的完整执行树，给人“一次得到全部结果”的错觉，忽略了大规模状态空间的组合爆炸。

误区求解器说不可满足，可能只是它没算对，我应该继续往下探索，说不定后面还能走通。

正解不可满足是数学上的结论：不存在任何输入能让当前路径条件同时成立。既然没有具体输入能到达该状态，继续向下探索只会浪费算力。工程实现会把该分支直接丢弃。就像规划师已经证明某条路几何上无法接通，就没有必要再铺路。

为何常见：初学者常把求解器当成“猜答案的工具”，没理解它给出的是可满足性判定，而不是概率性建议。

误区符号执行是软件漏洞挖掘、CTF 里用的，硬件验证靠跑仿真就行，两者没什么关系。

正解符号执行同样适用于 RTL 等硬件描述。它可以检查状态机可达性、断言反例、网表等价性，还能为覆盖率目标生成定向测试向量。硬件电路本质上也是由分支条件构成的执行逻辑，只不过“输入”变成了信号，“路径”变成了时序状态转移。

为何常见：符号执行最常见的技术文章都围绕软件漏洞和模糊测试，硬件验证领域的成功案例相对少被提及，导致认知偏差。

误区合并会把两个不同条件揉在一起，损失精度，那我不合并，全部展开是不是更可靠？

正解全部展开在规模稍大的设计上会立刻触发路径爆炸，导致没有结果。合并是一种有损压缩，换来的却是可行性。工程上要在“精度”和“能跑完”之间取平衡：先展开后合并，或采用抽象域（区间、位向量区间）把精确条件粗化为可判定形式，保证分析在预算内跑完。

为何常见：人们习惯性地认为“精确”必然优于“近似”，忽略了验证任务的核心约束是时间和内存有限。

误区符号执行这么强，能枚举路径，直接取代 UVM 仿真和随机测试就行了。

正解符号执行在大型复杂设计上仍然受限于求解效率和路径爆炸，它更适合精准攻坚：覆盖盲区定向补盲、断言反例生成、等价检查。随机仿真速度快、易扩展、无需求解开销，仍然是覆盖率基线的主要来源。实践中两者互补：仿真粗扫全局，符号执行定点深挖。

为何常见：新技术出现时容易被过度宣传，尤其符号执行“系统化探索”的说法听起来像是穷举，而穷举似乎天然优于随机。

面试题

Q1. 符号执行的核心思想是什么？

单选题 · easy

  • A.随机生成输入不断执行程序
  • B.用符号值替代具体输入并探索多条路径← 正确答案
  • C.依赖真机测试大量用例
  • D.安排人员逐行阅读源代码

答案：B。符号执行把输入变量当作符号而非具体数字，通过路径条件和约束求解同时探索多条分支。随机执行、真机测试和代码走读都只能处理单一路径或单一视角，无法像符号执行那样并行推演所有可能路径。

Q2. 在符号执行状态三元组 (pc, σ, s) 中，pc 表示什么？

单选题 · mid

  • A.程序计数器寄存器数值
  • B.路径条件，是分支约束的合取← 正确答案
  • C.求解器返回的可满足模型
  • D.当前指令的操作码组合

答案：B。pc 是 path condition，即从程序入口到达当前状态所累积的全部分支约束的合取；程序计数器另有其名，不属于状态三元组的核心组成部分。σ 负责变量到符号表达式的映射，s 描述当前指令位置。

Q3. 路径条件不可满足时通常怎么处理？

单选题 · easy

  • A.继续深入执行直到条件变为可满足
  • B.将这条路径剪枝，不再向下探索← 正确答案
  • C.无条件为该路径生成一个测试向量
  • D.把所有符号变量转成随机数再次执行

答案：B。不可满足意味着不存在任何具体输入能让程序到达该状态，继续探索只会浪费算力。工程实现中直接丢弃该分支。随机数替换会破坏符号执行的确定性，也不解决约束冲突问题。

Q4. 约束求解器在符号执行中的主要职责是什么？

单选题 · mid

  • A.把符号表达式翻译成汇编指令
  • B.判断路径条件是否可满足并生成取值← 正确答案
  • C.计算被测程序的总执行时长
  • D.将多条执行路径合并成同一状态

答案：B。求解器回答路径条件可满足性（SAT/UNSAT），可满足时返回一组具体模型值用于构造测试输入或反例。翻译汇编、统计时长和状态合并都不是求解器的职责，状态合并且搜索策略层完成。

Q5. 下列哪些属于缓解路径爆炸的有效手段？

多选题 · hard

  • A.对不可满足路径先行剪枝← 正确答案
  • B.合并满足等价条件的路径状态← 正确答案
  • C.任意降低所有约束求解精度
  • D.发起启发式搜索优先探索目标路径← 正确答案

答案：ABD。剪枝直接删除不可达分支；状态合并把多条相似路径凝成一条；启发式搜索引导探索方向，避免无差别遍历。任意降低求解精度会增加误判，既不安全也不属于工程上推荐的缓解手段。

Q6. 符号执行中“符号存储”σ 的作用是什么？

单选题 · mid

  • A.记录程序运行时间快照
  • B.把符号变量映射到其符号表达式← 正确答案
  • C.保存每条路径的执行日志
  • D.存放随机测试向量及预期值

答案：B。符号存储映射变量名到符号表达式，例如 x→α、y→α+1，执行过程中不断更新以描述当前状态。它不保存时间快照或执行日志，也不存放测试向量——那些是求解器输出层的数据。

Q7. 在覆盖率驱动验证中，符号执行的核心价值是什么？

单选题 · hard

  • A.彻底消除覆盖率统计过程的开销
  • B.为未覆盖路径生成针对性定向输入← 正确答案
  • C.完全替代所有随机仿真回归
  • D.保证总覆盖率恒为百分之百

答案：B。随机仿真在覆盖率高位时边际收益低，符号执行能从覆盖率缺口反向推导路径条件，再经由求解器生成定向输入补充盲区。但它无法消除覆盖率统计开销，也不能保证覆盖率永远到 100%，更不替代随机仿真的快速粗扫作用。

Q8. 硬件验证中符号执行的典型应用包括哪些？

多选题 · mid

  • A.为 RTL 覆盖率目标生成定向向量← 正确答案
  • B.生成断言属性的路径反例← 正确答案
  • C.综合前后做形式等价性检查← 正确答案
  • D.优化物理布线的拥塞程度

答案：ABC。符号执行从设计代码提取路径约束，用于覆盖率定向补盲、断言反例生成，以及 RTL 与门级网表的等价性比较。物理布局布线属于后端物理设计问题，与程序路径的符号分析无关。

Q9. 若平均分支数为 b、判定深度为 k 且不做剪枝，执行路径总数增长趋势是？

单选题 · extreme

  • A.线性量级增长
  • B.呈几何级数的爆炸式增长← 正确答案
  • C.只随深度对数增长
  • D.固定常数不随深度变化

答案：B。路径总数等于 1 + b + b² + … + b^k 的几何级数，近似为 O(b^k)，随深度指数爆炸。这正是“路径爆炸”一词的数学来源，也是符号执行必须结合剪枝、合并与搜索策略的原因。

Q10. 工程落地时符号执行需要重点权衡的实践包括哪些？

多选题 · hard

  • A.设置搜索深度与求解时间预算← 正确答案
  • B.与随机仿真结合形成覆盖率互补← 正确答案
  • C.通过状态合并限制并发路径数量← 正确答案
  • D.忽略求解器开销直接全量求解

答案：ABC。工程化首先要控制时间成本，所以设置深度和时间预算；仿真粗扫加符号执行精准补盲是常见互补组合；状态合并压缩路径数量以对抗爆炸。忽略求解器性能会让路径爆炸迅速失控，因此排除。