1. 先分清这个“VC Formal”到底是不是你以为的那个“VC”1.1 名词祛魅它和 Visual C、vCenter 不是一回事“VC Formal 实例”这几个字扔进搜索引擎出来的结果大概率会让人一头雾水先是 Microsoft Visual C 运行库的修复教程再是 VMware vCenter 的集群告警甚至还夹着微信模板消息里miniprogramState formal的跳转配置说明。你会以为要么是工具装坏了要么是自己搜错了关键词。其实都没错只是此 VC 非彼 VC。在数字芯片验证这个圈子里VC Formal 是 Synopsys 的形式化验证工具全称里包含“Formal”的意思是它跟纯粹靠跑仿真打激励的验证方式完全不同。它做的是数学层面的证明给你一段 RTL、一组用 SVASystemVerilog Assertions写的属性它在所有可达状态空间里搜索看看有没有违反这条属性的路径。有就给你一个反例没有就告诉你这条属性已经被证明成立。这种“证明”思维和“跑一万个用例没出错”的思维差着整整一个维度。动态仿真再充分也只能覆盖你写得出、跑得完的那部分场景形式化验证虽然不能把整个 SoC 级别设计直接甩给它但对关键模块的某些核心属性它给的是完备性保证。这也是为什么验证团队里经常有人说仿真在找 bugformal 在断案。我自己最开始接触 VC Formal 的时候也犯过迷糊把文档里的 VC 当成 Visual C顺手就去查运行库怎么装。直到同事拍我肩膀说这个工具不吃那套环境你装的是芯片验证工具链这才反应过来。所以如果你是因为“VC Formal”这个缩写点进来的建议先确认一下自己到底找的是哪个领域的工具别搞混了再往后看。1.2 什么项目会真正用到 VC FormalVC Formal 不是用来做整个芯片端到端验证的。像大型 SoC 这种上千万门的规模直接铺 formal求解器第一天就会给你脸色看。但它特别适合当中段验证的尖刀部队常见的使用场景我列在下面模块级属性验证比如 FIFO 控制器的溢出、下溢、读空写满时序状态机的非法状态跳转仲裁器的公平性总线桥的读写一致性。寄存器通路验证验证寄存器的读写属性是否和 spec 一致复位值是否匹配硬件和软件视角能不能对上。连接性检查SOC 集成阶段验证各个模块的端口信号连接是否正确时钟域交叉以后信号能不能正确采样。数据通路验证比如浮点运算、压缩加速器里的数据转换逻辑这类设计行为很规律特别适合形式化去穷举。CDC 结构性检查做同步结构、握手协议属性验证这个方向很多团队已经做成 regression 的一部分。在这些场景里VC Formal 的优势是能在 RTL 阶段就发现深层次 bug而不是等验证环境全部搭好、回归跑了几千个用例后才暴雷。功耗、时序、面积这些前端问题它不管但功能正确性它能管。很多 IP 级验证团队已经把 formality 属性库作为交付项之一没有通过 formal 证明的模块sign-off 都不能算完整。1.3 为什么网上搜出来的结果看着熟又对不上再回到搜索结果的事。微信小程序那边有个miniprogramState参数取值里确实有formal表示跳转的是正式版小程序VMware vCenter 经常会弹“主机和 vc 之间的时间已同步”的集群告警Windows 上修 VC 环境大多指的是 Microsoft Visual C Redistributable。这些搜索词里的“VC”和“formal”都是独立的通用词唯一的共同点是它们碰巧纠缠在了一起。加上“VC Formal”这个工具本身的用户集中在验证工程师圈子里普通互联网内容极少。这就导致搜索时看到的结果特别分裂。我写这篇文章就是想把一个能直接抄作业的“vc formal实例”摆出来让想上手的人不用再去翻一大堆文档拼凑信息。2. 我的实例选型为什么拿一个 FIFO 控制器来说事2.1 从项目需求里挑一个“状态空间友好”的设计形式化验证最怕的就是状态爆炸。一个模块的状态空间大小取决于内部寄存器数量、输入端口数量、组合逻辑复杂度。如果一上来就拿一个跨时钟域的千级触发器模块练手先不说跑不跑得完光是你就很难判断反例是设计 bug 还是断言写歪了。所以我选了一个非常经典、行为规律、状态空间足够小的同步 FIFO 控制器。FIFO 控制器在每一个数字芯片里几乎都会出现读指针、写指针、空满标志、almost_full/almost_empty 这些信号大家都不陌生。它虽然简单但非常考验时序边界什么时候能写、什么时候能读、读写同时发生时空满信号怎么变这些边界条件正好是形式化验证最拿手的地方。用这个例子能把 formal 的价值讲得很清楚也方便后面排查和收敛。如果你在公司里真正负责一个模块的验证选第一个 formal 用例时也应该照这个思路来优先选状态逻辑清晰、输入端口不多、行为边界明确的模块。不要贪大先跑通一条完整链路建立形式化验证的信心和流程再逐步扩大范围。2.2 我给它定义的 RTL 规格和需要证明的性质这个例子里我设计了一个参数可调的同步 FIFO深度 16位宽 32。核心逻辑分三部分写指针递增、读指针递增、根据指针差值和读写事件产生空满标志。为了贴近真实设计我额外加了两件事一是在写满之后屏蔽写使能二是读写同时使能且 FIFO 已经为满的时候屏蔽读使能避免指针产生非预期跳变。代码可以精简成下面的样子完整的可综合代码比这个长但关键行为全在这里module fifo_ctrl #( parameter DEPTH 16, parameter ADDR_WIDTH 4 )( input logic clk, input logic rst_n, input logic wr_en, input logic rd_en, input logic [31:0] wr_data, output logic [31:0] rd_data, output logic w_full, output logic w_empty, output logic w_almost_full ); localparam ALMOST_FULL_TH DEPTH - 4; logic [ADDR_WIDTH:0] usedw; // 额外位用来存深度 logic [ADDR_WIDTH-1:0] wr_ptr, rd_ptr; assign w_full (usedw DEPTH); assign w_empty (usedw 0); assign w_almost_full (usedw ALMOST_FULL_TH); always (posedge clk or negedge rst_n) begin if (!rst_n) begin wr_ptr 0; rd_ptr 0; usedw 0; end else begin case ({wr_en !w_full, rd_en !w_empty}) 2b10: usedw usedw 1; 2b01: usedw usedw - 1; default: usedw usedw; endcase if (wr_en !w_full) wr_ptr wr_ptr 1; if (rd_en !w_empty) rd_ptr rd_ptr 1; end end endmodule这里usedw用 5 bit 存深度计数比较巧妙的一点是表现完“同时读写”时深度不变表现完“只写”时深度加一条件里提前判断空满就不会出现负值或者超过深度的情况。真正要证明的性质不是这条实现代码本身而是它的对外行为是否符合规范。2.3 动态仿真与 formal 的分工别把一个工具当万金油有人可能会问这个 FIFO 这么简单仿真跑个几百个用例不也能查出来吗为什么非得用 formal道理在于覆盖完备性。仿真里的每一笔激励都是你主观构造的哪怕你写了随机约束也只能保证你约束到的场景被访问过。但 “FIFO 在写满那一拍如果同时来了读使能写指针到底会不会推进” 这种边界随机跑一圈不可能保证每个时序组合都被覆盖。VC Formal 的做法不一样它把所有可达状态都纳入求解范围只要这条属性在某一拍被违反它就能顺着状态转移把反例找出来。这是一种确定性的穷举不是概率上的采样。所以在项目里的正确分工是formal 用来证明那些可以被严格定义的、数量适中的关键属性动态仿真用来做大量交互场景的长时间回归和上层数据一致性检查。formal 不替代仿真仿真也别硬撑着去追求边界完备性两个工具互相配合才是效率最高的验证策略。3. 可复现的工程骨架目录、脚本与形式化约束3.1 一套能一次跑通的目录结构很多人第一次用 VC Formal拿到手就急着写断言结果连编译环境都没理顺后面每一步都在跟路径和加载顺序搏斗。我习惯先把工程目录划好再动手写任何代码。formal_fifo/ ├── rtl/ │ ├── fifo_ctrl.sv │ └── fifo_ram.sv ├── bind/ │ └── fifo_bind.sv ├── props/ │ └── fifo_props.sv ├── scripts/ │ ├── setup.tcl │ ├── properties.tcl │ └── run_fv.sh ├── logs/ └── reports/RTL 单独放、属性文件单独放、绑定文件单独放这个习惯帮我省掉过很多次“改了属性文件结果把验证源文件搞脏”的烦心事。重点说下bind文件它是 SystemVerilog 里非常实用的构造可以把断言模块用小钩子绑到被测设计上而不需要修改原始 RTL 一行代码。3.2 编译与建立设计的 Tcl 脚本要点VC Formal 的命令行启动方式随版本略有差异但核心流程是稳定的读文件、elaboration、设置时钟复位、建立设计、跑属性。我用的精简 Tcl 脚本骨架大概长这样set TOP formal_fifo read_file -sv -top $TOP {rtl/fifo_ctrl.sv rtl/fifo_ram.sv} read_file -sv {props/fifo_props.sv} read_file -sv {bind/fifo_bind.sv} elaborate -top $TOP # 给求解器指定时钟复位信号 set_clock clk set_reset rst_n -low # 建立设计后读取属性列表 create_property_sets add_property_set -set main_props -file props/fifo_props.sv -bind bind/fifo_bind.sv # 跑证明并输出报告 prove -property_set main_props report_properties -output reports/fifo_props.rpt report_proofs -output reports/fifo_proofs.rpt脚本里每一项都有讲究。-top指定顶层模块VC Formal 会以这个模块的接口作为边界未被约束的输入端口在 formal 里会被当成自由信号可以任意取值这一步非常关键set_clock告诉工具哪个是时钟信号形式化工具的“时间”和仿真的 timeunit 不是一回事它理解的是时钟沿转移关系set_reset -low说明复位是低有效工具会从复位释放后的状态开始展开。如果你跑的不是同步设计或者有多个时钟域可别直接照抄这三行还要把异步域的处理逻辑单独列出来。我见过不少初学者在跨时钟设计上强行用单一时钟约束结果求解器给出的反例全是“另一个时钟域的输入端任意翻转”导致的假失败非常误导。3.3 时钟复位约束最容易让形式化求解器“疯掉”的地方再展开说下时钟复位的处理。VC Formal 不是真的在仿真你的时钟波形它默认所有内部寄存器都是从某个抽象初始状态开始在每一个时钟沿上做状态迁移。如果你不告诉它复位信号何时有效它会默认寄存器初始值可以是任意 0/1 组合这意味着设计可能从“复位还没释放、内部状态完全未知”的节点开始搜索很多断言会因为这种任意初值而失败。标准做法是显式声明复位信号和复位极性同时给一个“复位释放若干拍后再评估断言”的假设assume property ((posedge clk) disable iff (!rst_n) $rose(rst_n) |- ##2 1b1);这种写法的意思是复位信号从低变高的那一刻开始至少再等两个时钟周期我才开始检查属性。CPU 里各种单元在复位释放后都需要一个稳定窗口才能进入正常工作状态在仿真里你可能靠环境序列控制但在 formal 里必须用显式假设否则求解器会在复位释放后的第一个可用周期就去挑战你的属性产生大量没有工程意义的反例。4. 属性编写SVA 断言在 VC Formal 里的正确打开方式4.1 从仿真断言到形式化断言的思维切换平时在 testbench 里写断言背后是“我发这拍激励下一拍采信号”这是把一个具体时刻的行为钉死。形式化验证里写断言面对的是所有可能序列它不是在检查某一个时刻而是在整棵状态树上检查这个表达式是否恒真。所以写 formal 属性的时候必须从“这一拍的这个路径对不对”跳到“任意合法序列下这个行为模式都成立”。这个思维切换是最难的。很多人第一次写 formal 断言时总是忍不住手贱去写具体的wr_en值或者rd_en值结果把通用属性写成了具体的测试向量既跑不出反例也证明不了什么。正确写法是把输入当成自由变量属性里只描述不变量和时序关系。4.2 实例中三条关键 SVA 的语义拆解回到 FIFO 实例我挑了三条最有代表性的属性。第一条是“写满时不能再写入”property p_no_write_when_full; (posedge clk) disable iff (!rst_n) w_full |- !wr_en; endproperty这条的含义是出现了w_full高电平则同一拍以及后续拍都不能出现wr_en有效。用|-表示重叠蕴含也就是前提成立的当前拍就检查结论。它保证了 FIFO 不会在满状态下继续写数据造成覆盖这是数据完整性里最核心的一条。第二条是“空状态下读使能会被屏蔽”property p_no_read_when_empty; (posedge clk) disable iff (!rst_n) w_empty |- !rd_en; endproperty如果设计自身已经把rd_en在空状态下屏蔽掉了这条属性会立即证明成功。可它依然重要因为从模块外部接口看总线主设备可能根本不知道 FIFO 现在是空是满它发了一个读请求如果控制逻辑漏了屏蔽就会把无效数据输出出去。第三条稍复杂一点是“almost_full 信号在达到阈值后必须拉高”property p_almost_full_assert; (posedge clk) disable iff (!rst_n) (usedw ALMOST_FULL_TH) |- w_almost_full; endproperty这条看着像句废话因为 RTL 里assign w_almost_full (usedw ALMOST_FULL_TH)是组合逻辑所以每次拍都会是同一结果。真正的调试价值在别处如果设计者把usedw的寄存器更新逻辑和w_almost_full的组合判断写在不同模块该拉高的信号延迟了一拍才拉高这条属性就会在边界拍抓到反例。这就是 formal 的价值——它能把组合路径上的延迟和不一致揪出来而普通仿真往往因为激励序列碰巧没跑到这个边界而放过。4.3 cover 属性就是你的形式化用例“验收单”做形式化验证光证明还不够你还要回答另一个问题这条特性到底有没有被刺激到如果一条断言被证明成立但设计里从来没有任何合法序列能让该相关信号翻转那证明成功也可能是因为你根本没抓住这个功能点。这时候需要 cover 属性。比如我想确认“从空到满的整条增长路径确实可被走到”cover property ((posedge clk) disable iff (!rst_n) w_empty w_full);这个属性有问题前面是 empty后面是 full中间完全没有时间关系。正确写法应该是“从 empty 到 full 至少需要经历 DEPTH 个写时钟周期”cover property ((posedge clk) disable iff (!rst_n) w_empty ##[1:$] w_full);这里##[1:$]表示在将来的任意一个时钟周期FIFO 能够从空走到满。如果这条 cover 属性查不到 witness只有两个原因要么写满的条件永远不可能满足要么设计里存在卡死状态。不管哪种都值得你回头查设计而不是自我安慰说“证明全过了就行”。formal 的证明结果和覆盖报告是一起看的拿到报告时会先扫一眼证明列表然后再扫覆盖列表两边都对得上才算这个模块真的验证干净了。4.4 不要让求解器做“不可能完成”的运算有一类坑特别隐蔽属性本身没写错但由于表达式过于复杂导致求解器一直跑不出结果。最典型的是把内部状态变量深度引用到断言里比如把两个内部 FIFO 的深度差值嵌进一个属性里还会同时描述跨多拍的复杂行为。VC Formal 的求解器虽然聪明但它不是神任何形式化工具的算力都有上限。我的经验是保持属性足够“原子”。一条属性只描述一个行为模式不要把一个复杂的时序流程用超长前缀和超长后缀塞在一起。如果属性太长先拆成若干个子属性每个子属性覆盖流程里的一个关键闭环。这不仅让求解器好过排查反例时也更清楚是哪一步出了问题。5. 反例排查从 Falsified 到修设计或修约束的完整链路5.1 拿到反例先做三件事VC Formal 跑完后报告里如果一个属性显示Falsified你手里会得到一个反例波形。这个波形是求解器从某个初始状态开始、逐步推进到违法状态的一条路径。别急着去改 RTL先按顺序做三件事。第一件事打开反例波形看起点状态是什么确认起点是否在合法初始状态空间内。很多反例是从“寄存器初值为全 0 以外的奇怪组合”开始的。这种反例需要对照你的 reset 假定看清它是不是在复位释放后立刻发生的。第二件事看反例路径上输入信号的变化是否合理。VC Formal 把所有外部输入都当作自由变量它会故意挑那些“现实中接受不到”的输入组合来尝试突破约束。如果你的 mock 模块或者上层接口逻辑在反向 Y 处给了特定约束VC Formal 可能没识别你设计者心里的约束因此给出了一个“理论上合法、实测里非法”的序列。第三件事把反例波形导入现有的仿真环境里回放一遍。VC Formal 能以fsdb或者vpd格式导出波形用波形对比工具打开看看同样的输入序列跑动态仿真时是不是真的会触发同样的失败。这一步就是传说中的“形式化与仿真互相佐证”能过滤掉一大半假反例。5.2 一次 almost_full 断言失败的真实排查过程我实际跑这个 FIFO 例子时就故意在usedw更新逻辑里埋了一个延迟两拍的错误模拟设计者写出来的 FSM 在接近满阈值时没有立刻拉高信号的情况。结果p_almost_full_assert果然报Falsified。当时反例波形里usedw在某一拍已经等于 13而 ALMOST_FULL_TH 是 12w_almost_full仍然保持低电平直到两拍之后才拉起来。排查过程是这样的先看反例起点内部寄存器初始状态是复位后的合法状态排除初始状态问题再看输入信号反例里只拉了写使能没有读使能输入序列完全合法最后回放波形发现问题是出在控制逻辑在usedw跨越阈值时没有直接组合判断而是把判断结果寄存了。这个案例说明断言本身没写错设计确实存在边沿延后行为和 spec 里“达到阈值后立刻拉高”的要求不符。修复方式也简单把w_almost_full改成组合逻辑或者把寄存两拍改成组合判断。修完重跑同一组属性一条报 failure其他全部证明通过。5.3 收紧形式化求解空间的技巧assume、cut、abstraction如果跑了半天工具一直停在Inconclusive或者超时你又很确信设计功能没问题那大概率是约束给得太松。VC Formal 领域有一个口头禅formal 里 80% 的时间不是写断言而是在跟约束作斗争。约束给得太宽求解器会探索大量无意义的状态约束给得太紧又会把真实的反例路径剪掉。三种常用手段我按优先级列出来约束外部输入合法性的assume语句优先到位。比如写使能信号来自上游 AXI 主设备你可以假设写请求有效时写数据必须稳定assume property ((posedge clk) wr_en | $stable(wr_data));。对无关紧要的内部逻辑做 abstract 或 cutpoint把状态空间切掉一块。比如一个 128 位的计数器如果只关心它是否计数到某个阈值可以把它替换成一个抽象的 “equivalent class” 模型求解器状态数会指数级下降。把超时属性拆成 BMC 深度限制下的验证。先跑一个较短的 bound比如 20 拍确认在这个深度内没有反例再逐步加大深度。这样做不是最终证明但能在压力下快速积累信心也能寻找反例的蛛丝马迹。这些手段都不是玄学背后都在做同一件事丢掉和当前属性无关的状态自由度让求解器把算力集中在真正需要证明的空间上。6. VC Formal 环境与运行期常见的那些坑6.1 编译检查过一跑就 Fatal 的典型原因实际项目中VC Formal 的报错有一大半不是验证逻辑出问题而是环境或者工程组织出了问题。最常见的几种路径错乱Tcl 脚本里用了相对路径但在别的目录启动工具导致read_file找不到源文件。我的经验是脚本入口处先cd到工程根目录所有路径用变量拼出来别裸写相对路径。文件重复读同一个模块或者同一个属性文件被read_file读了两次工具直接报重定义错误。属性文件之间互相 include 时特别容易踩。bind 模块名冲突bind 的目标模块和属性模块在多个文件里被重复定义elaboration 失败。给每个 bind 模块起名时加上前缀区分比如fifo_bind、fifo_props不要用通用名bind_module。没指定-top或者指定错了 top工具可能把多个顶层并行编译状态空间立刻翻倍性能肉眼可见地崩。还有一种隐蔽情况工具启动之后session 保存和恢复目录不是同一个工作目录导致日志只写到了临时目录。排错时第一件事就是看 log 文件而不是盯着 console 输出。console 经常只打一层报错摘要真正的原因分析都在 log 里。6.2 从“修复vc环境”这个热搜词说开去环境异味与运行期状态网上搜“修复vc环境”的人绝大多数是 Windows 下 Visual C 运行库依赖坏了程序一启动就弹窗。但 VC Formal 主要是跑在 Linux 服务器上的 EDA 工具它吃的环境依赖不是 VC 运行库而是操作系统底层的 library 版本、license 服务、文件锁、共享内存这些。我自己踩过一个大坑是服务器时间漂移。虽然 VC Formal 本身不强制要求跟 license 服务器保持严格同步但一些版本在验证许可时会对时钟偏差做宽限检查。如果时间偏差太多启动直接报 license 失败或者弹一个莫名其妙的内部错误。那次我排查了很久最后发现是物理机上的 NTP 服务没起来时间比真实时间慢了十分钟。所以如果工具突然从能用到不能用的症状我的第一反而不是翻属性文件而是检查系统时间和 license 进程状态。环境干净和设计正确一样重要。做一个 formal 工程时尽量固定工具版本和服务器镜像不要随手升级 OS 小版本。EDA 工具链对底层环境非常敏感一个动态库版本的小变化可能让一个原本 5 分钟收敛的工程突然跑两个小时还出不来结果。6.3 哪些“VC”词是来捣乱的顺手再说几个容易被搜索引擎搅进来的词。Windows 下装 Visual C Redistributable 修复的是运行库VMware vCenter 的“主机和 vc 之间的时间已同步”讲的是管理集群时钟微信模板消息跳转小程序时设置的miniprogramState的formal表示正式版状态。它们和 Synopsys VC Formal 的关系就像“苹果”既可以是水果也可以是公司名语境不同东西完全不一样。如果你和我一样是数字验证工程师下次搜“VC Formal”时看到这些结果直接略过就好。真正的 VC Formal 内容通常藏在 Synopsys 的 SolvNet 文档、验证工程师博客、行业大会上而不是搜索引擎第一屏的“运行库修复攻略”里。7. 把形式化用例沉淀成可以复用的资产7.1 断言文件模块化从 FIFO 抽出的通用属性很多团队做 formal 是一次性的项目结束断言文件就丢在角落里吃灰。但如果你稍微花点时间把属性整理成模块化结构下个项目复用起来的价值会成倍放大。拿我这个 FIFO 来说p_no_write_when_full、p_no_read_when_empty这两条看似老生常谈却在几乎每个带 FIFO 的模块里都通用。把它写成一个公共断言文件用参数区分空满阈值和 FIFO 深度就能直接复用到下一个 FIFO 实例上。module fifo_common_assertions #( parameter type fifo_t logic, parameter int FIFO_DEPTH 16 ) ( input logic clk, input logic rst_n, input logic wr_en, input logic rd_en, input logic w_full, input logic w_empty ); p_no_write_when_full: assert property ((posedge clk) disable iff (!rst_n) w_full |- !wr_en); p_no_read_when_empty: assert property ((posedge clk) disable iff (!rst_n) w_empty |- !rd_en); endmodule带小程序的另一个经验是给断言起名带上层级序号。直接用p_xxx的命名方式在上一级综合报告里能清楚地看到每个属性属于哪个模块而不是几十个assert_1、assert_2挤在一起报告一长就完全没法看。7.2 批量回归与报告解析形式化验证同样需要进回归。每次 RTL 有更新就把所有属性集合重跑一遍输出结果和上一次做 diff。VC Formal 的报告中属性状态通常有Proven、Falsified、Inconclusive、Not_Tried几种。我的回归脚本里加了一个简单的解析逻辑看到Falsified就立刻把 session 锁住生成反例路径然后命令行调用发一封信给相关开发者。这样设计提交一进来如果触发了 regress 失败相关负责人几秒钟内就能收到通知。跑批量任务时还经常遇到并发问题。多个 formal 任务同时开license 资源的冲突首当其冲。我在工程里强制规定每个任务用独立的工作目录和独立的 session 名不共享临时目录否则经常出现 session 锁文件互相覆盖的诡异问题。7.3 从 property 到覆盖率驱动的 formal sign-off走到最后一步你会发现 formal 验证的价值不是给你一个“全部证明通过”的绿点而是给你一张跟 spec 对应的功能覆盖地图。每一条属性代表一个功能行为每一个 cover 代表一个行为场景把这些都整理成一张表对应到验证计划里就能清楚地告诉项目组这项功能的正确性是被数学证明覆盖的那些行为是被动态仿真覆盖的两条证据链加在一起才算真正的验证闭环。我个人比较推荐的方式是项目开始时先写一份 formal 验证计划表把 spec 的每一条 critical requirement 列出来旁边标上对应的断言文件、覆盖点、模式要求。项目进行中不断维护这张表等流片前的 formal review 会上这张表比任何口头汇报都有说服力。这也是为什么我坚持认为formal 用例不是一次性测试代码它应该是一个模块长期演进的完整“行为档案”。最后再分享一个小技巧。每次写新断言之前先问自己一句如果这条断言被违反了电路的实际行为会是什么答得上来这条断言才有意义答不上来说明你对这个模块的行为边界还没想清楚写出来的断言大概率不是太宽就是太紧。形式化验证逼着你把设计行为想透彻这可能是它带给工程师最大的额外收获。