# FSM验证需求与规划

## 1. 验证目标

根据`FSM/README.md`中的描述，本次验证的目标是确保Mealy FSM（按键脉冲生成）的功能正确性。具体包括以下几点：

1. **状态转换验证**：验证状态机在`IDLE`和`PRESSED`状态之间的正确转换。
2. **按键检测验证**：验证当`key_in=0`（按键按下）时，状态机能否正确响应。
3. **脉冲输出验证**：验证在`PRESSED`状态下，`pulse_out`是否仅在一个时钟周期内为高电平，实现单次触发。
4. **复位功能验证**：验证在`reset`信号为高电平时，状态机能否正确回到`IDLE`状态。
5. **Mealy特性验证**：验证输出`pulse_out`确实依赖于当前状态和输入`key_in`。

## 2. 功能理解

FSM的功能是实现按键消抖与单次触发脉冲生成。其核心逻辑如下：

- **输入信号**：
  - `clk`：时钟信号。
  - `reset`：异步复位信号，高电平有效。
  - `key_in`：按键输入信号，0表示按下（低电平有效）。
  
- **输出信号**：
  - `pulse_out`：输出脉冲信号，高电平有效，单次触发。

- **状态机设计**：
  - `IDLE`：空闲状态，等待按键按下。
  - `PRESSED`：按下状态，检测到按键按下后产生脉冲并返回空闲状态。

## 3. 风险点分析

在设计测试用例时，需要特别关注以下几个风险点：

1. **状态转换错误**：状态机可能无法正确地从`IDLE`转换到`PRESSED`，或者从`PRESSED`转换回`IDLE`。
2. **脉冲输出持续时间**：`pulse_out`可能在一个时钟周期以上保持高电平，或者未能在一个时钟周期内变为低电平。
3. **复位功能失效**：在`reset`信号为高电平时，状态机可能无法正确回到`IDLE`状态。
4. **按键抖动处理**：如果设计中未考虑按键抖动，可能导致多次触发脉冲输出。
5. **Mealy特性验证不足**：输出`pulse_out`可能未正确依赖于当前状态和输入`key_in`。

## 4. 验证计划

为了系统地验证上述功能，将按照以下步骤进行：

1. **状态转换测试**：
   - 测试从`IDLE`到`PRESSED`的转换。
   - 测试从`PRESSED`到`IDLE`的转换。
   
2. **按键检测测试**：
   - 测试在`IDLE`状态下，`key_in=0`时是否能正确触发状态转换。
   
3. **脉冲输出测试**：
   - 测试在`PRESSED`状态下，`pulse_out`是否仅在一个时钟周期内为高电平。
   
4. **复位功能测试**：
   - 测试在任意状态下，`reset=1`时状态机是否能正确回到`IDLE`状态。
   
5. **Mealy特性测试**：
   - 测试`pulse_out`是否依赖于当前状态和输入`key_in`。

通过以上测试，确保FSM的功能符合设计要求。