解读

面试官抛出“断言合成”这一关键词，核心想确认三件事：

1. 你是否真正理解“形式化”与“仿真”在验证理念上的差异；
2. 能否把设计意图（自然语言/时序图/协议表）自动翻译成SVA/PSL，而不是手写一条条assertion；
3. 是否清楚国内主流流程（SpyGlass-VC-Formal、Synopsys VC-Formal、Cadence IFV、国产FPV工具）里“合成”这一步到底谁来干、怎么干、干完怎么签收。
   回答时切忌只背定义，要落到“谁给谁合成、输入是什么、输出是什么、如何确保sound & complete、如何与动态验证协同”这四个落地场景。

知识点

1. 形式化验证三要素：数学模型（Kripke结构）、属性语言（SVA/PSL）、算法（BMC、IC3、Pdr）。
2. 断言分类：安全属性（safety）、活跃属性（liveness）、连接属性（connectivity）、死锁（deadlock）。
3. 合成输入：RTL、协议文档、时序图、接口表格、设计规约（Word/Excel）、已有仿真covergroup。
4. 合成方法：
   a. 模板法（Pattern-based）：把协议拆成“请求-响应”“握手”“FIFO”“仲裁”等模板，工具自动套SVA骨架；
   b. 机器学习法：用LSTM/GNN从大量手写断言库学习，再对陌生RTL做token-to-assertion映射；
   c. 语义解析法：先把协议表转成时间自动机（TBA），再反向生成SVA。
5. 合成输出：SVA/PSL文件、覆盖率报告、假通过率（false-positive）列表、复杂度（state/bit）评估。
6. 质量门：
   • 一致性检查（Consistency）：同一接口多套协议不能互斥；
   • 完整性检查（Completeness）：用mutation或covercheck确保没有漏掉关键场景；
   • 可证明性检查（Provability）：state爆炸指数<1e6，否则退回重写。
7. 国内项目落地痛点：
   • 协议表更新频繁→断言版本管理；
   • 状态机隐含约束→需designer补充assume；
   • 工具license昂贵→先用“轻量级FPV”做模块级，再集中到子系统。

答案

断言合成就是把“人看得懂”的设计规约自动变成“工具看得懂”的SVA/PSL断言，并保证在形式化验证里可解。
具体分四步：

1. 规约结构化：把协议文档拆成“信号列表+时序关系+异常处理”三张表，用脚本转成JSON或XML，作为合成器输入。
2. 模板匹配：在预置的“协议模式库”里检索最贴近的模板（如AXI-write、APB-read、FIFO-full-handshake），把端口名、宽度、延迟参数做一对一替换，生成初版断言。
3. 约束求解：对初版断言跑一遍轻量级BMC（k=10），若出现counter-example，判断是设计bug还是断言过约束；若是后者，自动放宽延迟窗口或拆分多周期路径，再迭代。
4. 签收确认：
   • 用mutation在RTL里注入100个典型bug，要求合成断言能抓到≥95个；
   • 与仿真covergroup做cross-check，确保没有重叠也没有空白；
   • 输出文档：assertion_list.sv、fpv_setup.tcl、complexity_report（state<1e6、proof-time<2h）。
     最终把这三件套交给形式验证工程师，即可在 nightly regression 里跑JasperGold或VC-Formal，实现“零平台、穷举场景”的验证目标。

拓展思考

1. 如果协议表本身有二义性（如“ready可拉低1~3周期”写成“1或3”），合成器如何提示设计人员澄清？
   答：在JSON schema里增加“delay_type=range|exact”字段，若检测到range宽度>1且未标注“允许任意”，则报warning并生成assume(ready |-> ##[1:3] ready)两条候选，让设计师选其一。
2. 面对超大状态空间（如256-bit加密核），合成器如何降维？
   答：先用“数据无关性”分析，把payload信号标记为“don’t-care”，只保留ctrl-path；再引入“抽象解释”把256-bit切割成8-bit slice，分别证明后合并。
3. 国内自主FPV工具（如某芯原、某华大）尚未支持PSL，如何把合成结果迁移？
   答：在合成器后端加“方言转换”插件，统一输出最小公共子集的SVA，禁用local variables、禁用rose/fell，保证在任何国产工具都能直接compile。