实验：计数器复位、回绕与不变式验证

实验对象与观察条件

初值设为 3，在第一个上升沿^{i上升沿 时钟从 0 变为 1 的瞬间。它不同于表示整个 CLK=1 区间的电平。了解更多}复位^{i复位 将状态恢复为规定初值的控制。必须同时规定其同步或异步性质，以及相对于其他控制的优先级。了解更多}。之后按 0、1、2、3、0 推进。即使复位信号已经有效，时钟边沿到来之前数值仍保持不变。

开始之前

准备 Digital Design Studio 的 Desktop 项目及正常运行权限。将各示例分别保存到独立文件夹中的 rtl/top.sv。

SystemVerilog 源码

module top (
    input logic clk,
    input logic rst,
    output logic [1:0] count
);
    // Active-high synchronous reset: sampled only at the rising clock edge.
    always_ff @(posedge clk)
        if (rst) count <= 2'b00;
        else count <= count + 2'b01;
endmodule

运行方法

在 New analysis 中选择 Two-state single-clock v1。Clock port 设为 clk，周期为 1000ps。使用以下设置完成 Preflight，再执行 Run RTL simulation 并比较结果。

输入激励

[
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  }
]

每列记录一个上升沿的观察结果。输入取自边沿前，名称带 after 的状态取自更新后。列的排列表示采样顺序，并非描绘物理传播延迟^{i传播延迟 从输入变化到输出稳定为正确值所需的时间。逻辑表达式等价与时间特性是两回事。了解更多}。E0~E4 分别是 500、1500、2500、3500、4500ps 的上升沿。除了最终值，也要比较所有中间 count 列。

比较结果

5 cycles · count=00。检查在 500、1500、2500、3500、4500ps 时，是否依次为 00 → 01 → 10 → 11 → 00。

本实验使用 0/1 单时钟 RTL，不包含 #delay、initial 或 X/Z 测试平台。学习完成标记只记录学习进度，不代表实际仿真结果。

逐边沿计算预期状态

初始寄存器^{i寄存器 存储多位状态的电路。本课程中的同步寄存器在时钟边沿存储指定输入。了解更多}值为 3，但第一个上升沿优先执行复位。不要将初始化与复位混为一谈。

在不复位的区间，每个边沿都必须满足以下关系。

若只确认最终值 00，即使中途经过错误值也可能通过。应分别检查完整状态序列与复位优先级。

每次只改变一个实验条件

• 将初值改为 00，第一次复位后的状态序列仍应相同。由此检查复位是否独立于初值。
• 将 Reset cycles 改为 2，前两个上升沿的 count 都应为 00，之后开始递增的时刻推迟一个边沿。
• 若扩展为三位，回绕周期应为八次递增。不要只改声明，也要检查常量位宽、初始寄存器数组和运行长度。

推广到模 10 设计

四位存储能表示 0 到 15，因此仅递增不会在 9 之后变成 0，必须另行定义下一状态函数。

此定义规定：处于未使用状态 10~15 时，若 enable 有效则返回 0。也可选择其他恢复策略，但规格与验证模型必须使用同一策略。