XS-MLVP

通过脚本把 DUT 基本信息写入 .formal_records.yaml 的 basic_info 字段，并由系统自动渲染 02 基本信息文档。

从 analysis 中提取 RTL_BUG 属性，LLM 通过脚本将 Bug 详细信息写入 .formal_records.yaml。

自动解析环境分析文档和 wrapper.sv，为每个 RTL_BUG 生成 Python 测试函数框架，LLM 填写引脚驱动和断言逻辑。

基于 basic_info.clock_reset 与 extra_config.tcl 渲染 wrapper/checker/formal.tcl。

提取和分析被测模块(DUT)的功能规格和形式化检测点

Internal support skill for formal verification workspaces. This folder carries shared Python helpers and templates used by other formal skills and is not intended for direct user invocation.

通过脚本把验证规划写入 .formal_records.yaml 的 planning 字段，并由系统自动渲染 01 规划文档。

通过脚本把最终总结写入 .formal_records.yaml 的 summary 字段，并由系统自动渲染 05 总结文档。

从 analysis 中提取 RTL_BUG 属性，LLM 通过脚本将 Bug 详细信息写入 .formal_records.yaml。

自动解析环境分析文档和 wrapper.sv，为每个 RTL_BUG 生成 Python 测试函数框架，LLM 填写引脚驱动和断言逻辑。

提取和分析被测模块(DUT)的功能规格和形式化检测点

环境分析技能。Checker 已自动解析日志并生成骨架，LLM 仅需通过脚本填写分析详情。

在 YAML 中编写 SVA 属性检测代码

指导解释覆盖率报告并优化未覆盖死角的技能

RTL源码静态Bug分析阶段专属技能,用于指导 static_bug_analysis.md 文件的编写以及格式规范