func-spec

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

功能规格与检测点分析工作流 (Functional Spec)

本技能指导如何基于给定的基础信息，细化出该 DUT 应该包含的具体功能检测点，通过 update_spec.py 脚本 写入 .formal_records.yaml。

功能点标签规范、Style 标注规则与高级模式示例参见 Guide_Doc/functions_and_checks.md

步骤

1. 读取基础信息

阅读输入说明、RTL 源码或预生成的文档骨架，理解 DUT 的核心功能。

2. 规划三级标签结构

按照 Guide_Doc/functions_and_checks.md 中的规范，使用 FG-XXX (功能组)、FC-XXX (功能点)、CK-XXX (检测点) 组织层级。

3. 通过脚本写入 YAML

禁止直接编辑 .formal_records.yaml，必须通过 RunSkillScript 调用 update_spec.py：

添加功能组 (FG)

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action add_fg -id FG-API -name "验证环境约束"

添加功能点 (FC)

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action add_fc -fg FG-API -id FC-API-INPUT-CONSTRAINT -desc "定义输入信号的合法约束条件"

添加检测点 (CK)

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action add_ck -fc FC-API-INPUT-CONSTRAINT -id CK-API-INPUT-NO-X -style Assume -desc "输入信号不能为 X 态"

修改条目

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action update -id CK-API-INPUT-NO-X -style Comb -desc "新的描述"

删除条目

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action delete -id CK-API-INPUT-NO-X

管理全局参数 (Parameters)

用于定义 WIDTH 等硬件常量，会自动同步到 SV 模块头和实例化语句中。

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action set_param -id WIDTH -value 64

删除参数：

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action delete_param -id WIDTH

管理白盒观察信号 (Whitebox Signals)

用于在 wrapper.sv 中手动声明一些用于观察内部逻辑的信号。

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action add_signal -desc "logic [WIDTH-1:0] internal_state"

删除信号（需提供完全匹配的声明字符串）：

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py \
  -action delete_signal -desc "logic [WIDTH-1:0] internal_state"

查看当前结构 (Show)

python3 .veriagent/skills/formal/func-spec/scripts/update_spec.py -action show

4. 完成后调用 Check

Checker 会验证 YAML 结构完整性，通过后自动生成 03_{DUT}_functions_and_checks.md 文档。

核心规则

1. 对于每一个状态转移或者核心功能 Seq 检测点，尽最大可能配对提供一个 Cover 检查（证明其可达性）。
2. 在规划阶段严禁编写真实的 SystemVerilog 代码，只写逻辑描述。
3. 必须包含 FG-API（环境约束）和 FG-COVERAGE（可达性覆盖）两个功能组。
4. id 必须以 CK- 开头，使用大写字母和横杠（如 CK-CORE-ARITH-RESULT）。
5. style 必须是 Assume / Comb / Seq / Cover 之一。