模拟功能模型和晶体管电路的一致性是模拟混合信号验证里一块老硬骨头。这篇论文速读想聊的MSDV方法核心就一句话怎么用形式化的手段证明你写在系统级的功能模型和真正拿去流片的晶体管级网表在行为上是一致的。文章会从问题定义、方法链路、工程落地三个层面拆适合正在做AMS验证、或者被“模型和电路对不上”坑过很多次的设计验证工程师。我先说结论这不是要把仿真全扔掉而是在仿真之外给一个更接近“全域答案”的证明。1. 先把问题钉死什么才算模拟功能模型与晶体管电路“一致”1.1 从建模层级说起芯片设计里有一条经典的抽象链系统架构模型 - 功能模型行为级通常用硬件描述语言描述连续信号 - 晶体管级网表 - 版图寄生网表。功能模型存在的理由很朴素速度。整颗芯片的系统级验证如果全用晶体管级网表跑仿真时间会膨胀到没人能接受功能模型把大量的非理想细节压掉只保留端口行为仿真速度快几个数量级系统架构师才能在上面跑算法、调参数、做权衡。问题恰恰就出在这条抽象链上。功能模型大多是设计师“写”出来的不是从电路里“证”出来的。设计师凭经验把增益、带宽、摆率、输出范围填进一个理想化描述里可这个模型是不是真的在任何输入下都能复现晶体管电路的响应没有人能打包票。更常见的场景是电路改了几版模型没跟上工艺角变了模型里的常数还是老参数版图寄生提取之后电路特性已经偏移功能模型却依旧岁月静好。等到系统级验证跑出问题你根本分不清是模型错还是电路错。我见过最典型的翻车案例是一个带隙基准模块。功能模型里写的是理想齐纳管特性系统级仿真全通过结果前端把模型交给后端做混合信号协同仿真一跑就发现25%的偏差最后排查了两周问题出在模型忽略了启动电路的瞬态行为。这类问题靠人肉对版本、对注释、对波形效率极低而且根本不可规模复用。1.2 “一致”是个可量化的命题不是口号论文里最值得先读的部分就是把“一致”定义成数学命题。大概可以写成这样对于定义在输入域 U 内、时间窗口 [0, T] 上的任意激励 u(t)若晶体管电路输出 y_tr(t) 与功能模型输出 y_mod(t) 满足‖ y_tr(t) - y_mod(t) ‖ ≤ ε(t)则称两者在参数 (U, T, ε) 下一致。这三个要素一个都不能少。输入域 U 不是全空间而是规格书里规定的正常工作范围时间窗口 T 把稳态和瞬态分开处理误差容限 ε(t) 允许输出有界偏差而不是要求“绝对相等”——模拟世界里绝对相等既不现实也无必要。把这个定义吃透你就能理解整篇论文的走向它不是发明了一个新概念而是把工程直觉翻译成了可计算、可判定的形式。后面所有方法本质上都在为这个命题找证明路径。2. 传统仿真验证为什么回答不了这个问题2.1 仿真的本质是抽样而连续空间无法被抽样覆盖很多工程师的直觉是我跑了典型角、慢角、快角又做了500次蒙特卡洛还不够吗答案是不够而且这在方法学上是必然的。仿真验证的本质是在输入空间里取有限个样本点。哪怕是覆盖了工艺角的极端组合输入波形仍然是一条或一组有限轨迹。模拟电路的输入空间、参数空间、时间轴都是连续的有限样本在形式化意义上覆盖率是零。你跑了1000次仿真全过不能保证第1001次输入组合不翻车——尤其是那些需要特定输入时序才会触发的动态故障抽样法很难全面触达。蒙特卡洛解决的是工艺偏差的统计分布问题它告诉你“大概率是好的”但给不出“在所有条件下都安全”的边界承诺。对于安全关键、功能关键模块——比如电源管理里的过压保护、传感器接口里的比较器——这种概率性答案显然不够硬。2.2 形式化方法补的正是“抽样覆盖不了”的位置形式化验证的思路完全不一样它对输入域 U 内的所有输入做全称量化对时间窗 [0, T] 内的所有时间点做遍历判定对参数变化范围做有界约束求解。这本质上是把“是否存在一条导致不一致的输入轨迹”变成可判定的数学问题。但对模拟电路做形式化难处也是公认的没有有限状态空间可以遍历系统是非线性微分方程器件模型还带各种温度、工艺相关的高维参数。直接套数字验证那套二叉决策图或SAT求解完全行不通。这也是为什么直到现在模拟形式化验证在工业界落地依然偏少——不是没人想干是数学上太硬。这篇论文的价值是在“中等规模电路 有界时间窗 分段线性近似”这个合理范围内把这个难题做成了可用的工程方法。它不是万能的但把适用范围讲得很清楚这本身就是一种负责。3. 方法链路拆解四步搭出证明流程3.1 第一步把晶体管电路变成可计算的数学对象要证明一致先得把晶体管电路翻译成数学上可操作的对象。论文的做法是从标准网表出发用改进节点分析法MNA提取电路方程得到一个微分代数方程组DAE把每个晶体管用分段线性PWL模型近似。这里有个关键策略不追求全局精确。晶体管在大范围输入下是非线性的但绝大多数模拟模块在正常工作范围内只工作在线性区或饱和区的一个局部区域。把器件模型在“关注的运行区域”内做分段线性近似每段误差上界是可以计算的。这意味着后续所有结论都带了一个“区域内有效”的标签——这是工程上极其重要的起手式。我特别想强调这个“区域”意识。做模拟验证的人经常被非线性吓住但形式化验证恰恰不需要征服所有非线性只需要在你关心的那个运行域内把问题线性化然后严格证明边界。3.2 第二步把功能模型转成参考规范第二步是把功能模型形式化成验证的“参考契约”。功能模型通常有两种形态一种是闭式方程比如理想运放的 Vout A(V − V−) 加限幅另一种是框图形式的微分方程组。论文的做法是把这两种形态都统一转成一组约束输入输出关系约束、动态响应约束、输出范围约束。再结合前面定义里的误差容限 ε(t)就生成了一条“容忍管”——以功能模型输出为中心上下各偏 ε(t) 的通道。后续要证的命题变成晶体管电路的所有可能输出轨迹都落在这条容忍管里。这个转换的妙处在于它把两个系统谁对谁错的问题转化成一个几何包含关系的问题。谁当参考不重要重要的是参考的边界必须清晰、可计算。3.3 第三步可达集合包含判定核心步骤来了。对晶体管系统论文用区间分析或齐诺多面体zonotope传播来计算它的可达集合从初始状态集合出发按时间步进每一步把系统方程作用到当前集合上得到下一时刻的可能状态集合不断传播到 T 时刻。每一步传播得到的集合本质上是“在这个时间点上晶体管电路可能处于的所有输出状态”。然后用包含判定检查这些集合是否始终落在容忍管之内。如果是命题得证输出一份证明证书如果不是就提取一条反例轨迹说明“在哪一刻、什么输入下、偏差了多少”。这里我必须提醒一句可达集合是保守的。也就是说它算出来的是一个包含所有真实行为的超集。如果超集都在容忍管里真实行为一定也在但如果超集越界不代表真实电路一定越界——可能是近似太粗这就引出了第四步。3.4 第四步反例驱动的抽象精化循环碰到“超集越界但不确定真伪”的情况论文走的是经典的CEGAR路线反例引导的抽象精化。流程是先跑一次包含判定拿到潜在反例分析反例判定它是真实反例还是近似误差导致的伪反例如果是伪反例就细化抽象——把PWL分段分得更细、把时间步长缩短、把区间划分加密然后重新判定。这个循环看起来简单实际操作里是调参的艺术。分段数、步长、区间粒度三个参数互相牵制分段粗则计算量小但伪反例多步长小则精度高但状态集合爆炸快区间划分直接影响后续判定的保守性。论文给的策略是先粗后细每轮只收紧一个维度尽量用理论上的误差上界做预判而不是盲目细化。我在复现这条链路时最大的感受是形式化验证和仿真不是替代关系反而很像调试循环——每次细化抽象都相当于在问“这个问题是在电路里还是在模型近似里”。这个问题的答案恰恰是验证工程师最想要的中间产出。4. 工程落地的关键参数和流程4.1 先摸清适用边界不管论文写得再漂亮落地前必须知道自己站在哪里。按论文的实验数据和我自己的复现经验这套方法适合结构规模在几百晶体管以内的模拟模块比如运算放大器、比较器、带隙基准、滤波器的核心单元、锁相环里的分频和鉴相子模块。超出这个规模直接做全域可达集合是不现实的状态集合会指数膨胀。大模块的思路是分层拆解先证明每个子模块的一致性再把子模块的已验证功能模型组合起来验证组合后的系统。这跟数字验证里的“自底向上”、“组合爆炸”是同一套方法论只是数学工具换成了连续系统版本。4.2 容忍度、输入域和时间窗怎么定参数选择是我觉得论文里着墨不多、但工程上最考验判断力的部分。以我手头一个缓冲器验证为例电源电压5V输入范围按规格书定为0.5V到4.5V输出满摆幅约±4V。功能模型规定阶跃响应在2μs内完成建立建立精度0.1%即输出与最终值偏差不超过4mV。于是 ε(t) 可以分段定义2μs之后取4mV2μs之前可以放宽到50mV。时间步长按仿真精度的经验取1ns整个窗口就是2000步。这个参数的物理含义很直接你把验证的“法律条文”定清楚了。ε 太紧会有大量伪反例证明跑不出来ε 太松证明出来也没意义覆盖不住实际应用需求。一般做法是先拿几条典型仿真波形做参照把 ε 放在波形噪声底之上、规格要求之下的区间里再折中选值。4.3 一套可复现的基础流程我把落地的流程整理成六个步骤照着做基本可以跑通导出晶体管级网表确认工艺角和数据手册输入域。用MNA提取电路方程在目标运行区域内对器件模型做分段线性化记录每段误差上界。把功能模型的方程转成参考约束按规格定义 ε(t)。初始化时间步长、区间划分、分段数三组参数。运行可达集合包含判定失败则提取反例。分析反例来源走CEGAR循环细化抽象直到出证明证书或确认真实不一致。整个流程里第5、6步是核心循环也是最耗机器时间的部分。工具层面网表解析可以用商用EDA自带接口求解和集合运算可以接到开源SMT求解器和区间运算库上。这部分论文给了详细的算子定义照着实现不难。提示别一上来就跑最大规模的模块。选一个你最有把握的简单模块比如单级放大器先把整个流程跑通建立证明参数的直觉再逐步扩大。5. 常见坑与排查实录这条链路我踩过的坑比论文方法论本身更有参考价值。我整理成一张表后面每个坑再说几句。现象可能原因排查方向可达集合指数膨胀时间步长过小或区间划分过密先粗化参数确认反例是否消失伪反例反复出现PWL分段太粗器件模型误差超界细化器件分段而不是加密时间步证明通过但实际电路偏差大输入域定义与规格书不一致核对功能模型和电路各自的输入域约定ε 定太紧导致永远不收敛误差容限低于模型固有误差用仿真波形噪声底校准 ε反馈环路导致集合震荡固定点存在性未处理增加稳态区间分析先证DC工作点不同版本的网表描述不一致网表抽取脚本或工艺角选择问题统一网表生成流程加校验和第一个坑最常见。我刚跑时喜欢把时间步长压到0.1ns追求“精确”结果状态集合从第100步开始爆炸机器内存直接打满。后来改成1ns步长、先粗算再精算问题立刻缓解。记住形式化验证要的是上界不是精确值过度离散化只会害了自己。第二个坑和第一个刚好相反。有时反例反复出现我以为时间精度不够狂缩步长毫无作用后来才发现是器件PWL段数太少模型误差上界早就超出了 ε。换了个思路保持步长不变把晶体管模型在运行域内多切几段伪反例一次清空。第三个坑特别隐蔽。功能模型设计师习惯把输入范围写成“0到VDD”但晶体管电路实际规格因为共模输入范围限制只保证0.3V到4.2V。两边输入域对不上你证明出来的结果自然没有意义。所以流程第1步和第2步之间一定要加一道核对手续。第五个坑涉及环路。带反馈的电路可达集合传播容易在环路里来回震荡。论文的处理方法是对DC工作点先做同伦连续法求解确认固定点存在且唯一再做动态传播。这一点强烈建议不要省略否则你会被一堆毫无意义的震荡反例折磨到怀疑人生。6. 我的实践体会和还能往哪走把MSDV这套流程在几个真实模块上跑过之后我最大的体会是它改变了我对验证职责的理解。以前做模拟验证默认活法是“仿真覆盖 人肉判断”默认问题就是“没测到”。现在有了形式化一致性证明验证工作开始变“契约化”——设计模型的人必须把输入域、容忍度写清楚电路实现的人必须把运行区域和误差上界算明白。这两边一碰很多问题在架构阶段就暴露了而不是等到流片回来再救火。在具体工程里我现在的做法是混合验证对核心模块做形式化一致性证明拿一套证明证书归档对周边非关键模块继续用仿真加严苛用例做压力测试。形式化负责“没有反例”仿真负责“覆盖各种边角”。两种手段不是二选一而是各守一道防线。最后再说一个我判断的扩展方向。这套方法只验证当前版本的电路和模型但真实场景里电路会改版、工艺角会漂移、老化效应会积累。论文结尾其实也提到了一个想法把验证抽象复用起来——每轮改版只重算受影响的分区而不是全量重跑再把温度、老化参数也纳入形式化模型生成随温度变化的证明证书。这块要是做成了模拟验证的工作模式会往前再走一大步。我自己已经在尝试把版图后提取的寄生参数并入PWL模型虽然计算量明显上涨但证明结论对后端更可信了。有条件的团队值得往这个方向再挖一挖。