菜单
基于 basic_info.clock_reset 与 extra_config.tcl 渲染 wrapper/checker/formal.tcl。
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
基于 SOC 职业分类
UCAgent是基于大语言模型的自动化任务执行AI代理，支持通用工作流配置和执行。本技能提供配置文件编写规范、自定义Checker开发指南、--emulate-config配置校验工具使用方法，帮助用户快速创建、验证和运行各类任务工作流。
通过脚本把 DUT 基本信息写入 .formal_records.yaml 的 basic_info 字段，并由系统自动渲染 02 基本信息文档。
从 analysis 中提取 RTL_BUG 属性，LLM 通过脚本将 Bug 详细信息写入 .formal_records.yaml。
自动解析环境分析文档和 wrapper.sv，为每个 RTL_BUG 生成 Python 测试函数框架，LLM 填写引脚驱动和断言逻辑。
提取和分析被测模块(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.
| name | formal-env-config |
| description | 基于 basic_info.clock_reset 与 extra_config.tcl 渲染 wrapper/checker/formal.tcl。 |
本技能用于维护 .formal_records.yaml 中与 Stage 5 渲染相关的配置。
本阶段的事实来源分为两部分：
.formal_records.yaml.basic_info.clock_reset：DUT 的真实时钟/复位定义.formal_records.yaml.extra_config.tcl：FormalMC 运行参数核心规则：
tests/{DUT}_formal.tcltests/{DUT}_wrapper.svRunSkillScript 调用 update_extra_config.py 修改 YAMLformal.tcl、wrapper.sv、checker.sv 都是派生产物，Checker 通过后系统会自动 full refresh 重建执行说明：
RunSkillScript 调用技能脚本python3 环境具备所有依赖常用命令：
python3 .ucagent/skills/formal/env-config/scripts/update_extra_config.py -action show
python3 .ucagent/skills/formal/env-config/scripts/update_extra_config.py -action set -path clock_reset.clock_signal -value "clk_i"
python3 .ucagent/skills/formal/env-config/scripts/update_extra_config.py -action set -path clock_reset.reset_signal -value "rst"
python3 .ucagent/skills/formal/env-config/scripts/update_extra_config.py -action append -path tcl.extra_commands -value '"set_prove_time_limit 3600"'
字段清单：
clock_reset.clock_signal：DUT 实际时钟端口名；无时钟设计填空字符串clock_reset.clock_count：时钟个数；组合逻辑可填 0clock_reset.clock_type：单时钟、多时钟或无时钟clock_reset.reset_signal：DUT 实际复位端口名；无复位设计填空字符串clock_reset.reset_type：同步/异步 + 高/低有效描述tcl.timeout：TCL 运行超时设置tcl.extra_commands[]：附加 TCL 命令最小骨架：
basic_info:
clock_reset:
clock_signal: ""
clock_count: ""
clock_type: ""
reset_signal: ""
reset_type: ""
extra_config:
tcl:
timeout: ""
extra_commands: []
推荐填写顺序：
basic_info.clock_reset 已经完整填写 DUT 真实时钟/复位事实。tcl.timeout，保证运行预算与设计复杂度匹配。tcl.extra_commands[]。写入约束：
clock_reset.clock_signal 与 clock_reset.reset_signal 必须来自 Stage 2 的明确填写。def_clk、def_rst、default clocking 或 disable iff。clk 和 rst_n；如果 DUT 实际端口不同，会在 wrapper/checker 内部自动生成别名映射。tcl.extra_commands[] 只放补充命令，不要重复模板默认已经生成的基础 setup。clock_reset 或 extra_config.tcl 后，应以 full refresh 生成出的 formal.tcl、wrapper.sv、checker.sv 为准。