# {{DUT}} 功能点与检测点描述

<!--
请基于前面分析好的需求和基础信息，在这里撰写详细的功能分组（Function Group, FG）和对应的断言检测点（Check Point, CK）。
请严格遵守以下标签规范：
1. 每一大类功能使用 FG-XXX 形式的标签，正文中再放置真实的 <FG-...> 标签
2. 具体细化功能使用 FC-XXX 形式的标签，正文中再放置真实的 <FC-...> 标签
3. 对应的断言检测点使用 CK-XXX 形式的标签，正文中再放置真实的 <CK-...> 标签
4. 每个 CK 必须显式标记 (Style: X)，其中 X 必须是 Assume, Comb, Seq, Cover 之一，这将决定最终生成的 SV 断言风格。
5. 注释中的说明文字不要直接写示例角括号标签，避免被解析器误识别。
-->

## DUT 整体功能描述

### 主要功能
<!-- 一句话描述 -->

### 端口接口说明
<!-- 再次确认最重要的关键端口 -->

### 关键参数
<!-- 重要参数 -->

### 状态机与时序
<!-- 简要总结 -->

---

## 功能分组与检测点

### 1. 验证环境约束 (API)

<FG-API>

#### 输入合法性约束

<FC-API-INPUT-CONSTRAINT>

**描述**: 定义 {{DUT}} 输入信号的合法约束条件，确保验证环境不会过约束或欠约束。

**检测点：**
<!-- 格式要求：每个检测点必须写成单行格式 -->
<!-- - <CK-XXX> **(Style: Assume/Comb/Seq/Cover)** 描述文字 -->
<!-- 示例：- <CK-API-INPUT-NO-X> **(Style: Assume)** 输入信号不能为 X 态 -->


---

### 2. 核心功能逻辑

<FG-CORE>

#### 核心状态更新与流控

<FC-CORE-LOGIC>

**描述**: 验证主数据链路或核心功能的正确性。

**检测点：**
<!-- 格式要求：每个检测点必须写成单行格式 -->
<!-- - <CK-XXX> **(Style: Assume/Comb/Seq/Cover)** 描述文字 -->


---

### 3. 可达性证明

<FG-COVERAGE>

#### 状态可达性

<FC-COVER-STATES>

**描述**: 证明关键状态可达到，特别是那些不容易触发的水位、满空标志或溢出等边界，确保验证环境没有配死。

**检测点：**
<!-- 格式要求：每个检测点必须写成单行格式 -->
<!-- - <CK-XXX> **(Style: Assume/Comb/Seq/Cover)** 描述文字 -->

---

## 形式化验证策略总结

### 引擎选择
<!-- 建议使用的形式化引擎，例如 pdrx, bmc -->

### 抽象策略
<!-- 是否需要抽象 -->

---

## 检测点完整性检查清单

### Safety 属性 (Comb / Seq)
<!-- 检查是否涵盖了该有的 Safety -->

### Coverage 属性 (Cover)
<!-- 检查是否涵盖了防假阳性的 Cover -->

### Assumption 属性 (Assume)
<!-- 检查环境约束是否合理 -->

---

## 已知缺陷

| 缺陷ID | 位置 | 描述 | 对应检测点 |
|--------|------|------|------------|
<!-- 这里填写目前已经预判有问题的代码点 -->
