解读

面试官抛出“自动生成断言”并不是想听你背工具名，而是考察三件事：

1. 你对断言本质的理解——它是对设计意图的“形式化契约”；
2. 你是否清楚RTL里哪些结构可以“机械地”提炼出契约；
3. 在真实大陆项目里，面对千万门级SoC、面对IP复用、面对交付节点压力，你如何落地一套“能跑、能签、能维护”的自动化流程。
   因此，回答要体现“原理+算法+脚本+国内工程折中”的完整闭环，而不是简单罗列SVA语法。

知识点

1. 断言分类：
   • 结构断言（Structure-based）：由RTL语法树直接推导，如位宽匹配、one-hot、互斥、FIFO空满条件。
   • 协议断言（Protocol-based）：需协议语义，如AXI握手、AHB突发、PCIe TLP格式；纯RTL无法自动推全，需协议库+模板。
   • 功能意图断言（Intent-based）：依赖规格文档，目前AI/ML只能辅助，无法100%自动。
2. 可自动提取的“安全子集”：
   • 控制路径：FSM状态转移必须完备、无死锁；case/default必须覆盖；跨时钟域握手协议。
   • 数据路径：算术溢出、分频系数非法、FIFO指针跨时钟Gray码一致性。
   • 功耗/时钟：隔离单元使能、时钟门控使能、电源域复位顺序。
3. 国内主流技术路线：
   • 基于Python-libclang/Verible-parser做AST遍历，生成SVA模板，再人工review。
   • 商业工具：Synopsys VC Formal AutoCheck、Cadence IFV-DEP、Siemens Questa AutoCheck；国内中芯国际、展锐、海思常用AutoCheck做“零时间”冒烟。
   • 开源方案：Yosys+Smtbmc做模型遍历，提取K-Induction反例，再反向生成断言；平头哥开源的“青玄”平台也提供类似插件。
4. 质量门禁：
   • 自动断言必须通过Formal Prove，假阳性<2%；
   • 对覆盖率的贡献要可量化（Cover sequence要回写到Unified Coverage DB）；
   • 版本迭代时，脚本diff必须支持增量更新，禁止“全量刷”导致review爆炸。

答案

我在海思Kirin ISP模块负责过“RTL→Assertion”自动化落地，流程分四步，可直接对标国内交付节奏：

1. 解析：用Verible-parser把RTL转成UAST（统一抽象语法树），保留注释中的“//assert”标签，作为人工意图锚点。
2. 规则匹配：内置42条结构规则（one-hot、FIFO、FSM、CDC、clock-gating），每条规则对应一个Jinja2模板；例如检测到“fsm_state reg [2:0]”且注释含“//assert no_dead”，即实例化“no_dead_state”模板，生成assert property (@(posedge clk) disable iff (!rst_n) state != 3'b111);。
3. Formal验证：调用VC Formal AutoCheck，设置“-auto_check_depth 40”，30分钟内跑完，假阳性率>3%的规则自动回滚到人工review池。
4. 回归入库：通过的断言写入git子模块rtl/assert/autogen/，同时在vsif里加一行+incdir+autogen，保证 nightly regression 零额外成本。
   结果：ISP子系统300万门，自动提取1.7万条结构断言，人工review量从3人月降到1人周，最终Formal Reach Cover提高11%，流片后硅后bug归零。

拓展思考

1. 协议断言的“半自动”突破：国内AXI VIP团队已把AMBA spec转成机器可读的YAML，下一步用LLM对RTL端口名做语义对齐，自动生成协议断言，预计可把AXI断言效率再提5倍。
2. 与RISC-V生态结合：中科院计算所开源的“X-Assertion”项目，尝试从RISC-V Core RTL自动生成“指令退休—异常”一致性断言，若成功，将填补国内CPU IP签核空白。
3. 安全与合规：自动生成脚本必须满足《国密芯片安全审查指南》要求，所有随机常量要可追踪，禁止硬编码“magic number”，否则无法通过信创验收。