ALU 07｜SVA、复位、反例验证与回归

SVA、复位、反例验证与回归

返回 ALU 任务总览。

任务：连接断言模块

alu_assertions 是模块类型，checks 是 top 中的实例名。它的 result 输入要接到同一个接口实例的输出：

alu_assertions checks (
  .clk(clk),
  .rst_n(vif.rst_n),
  .req_valid(vif.req_valid),
  .rsp_valid(vif.rsp_valid),
  .result(vif.result)
);

若找不到字面短语“alu_assertion checks”，先分别核对模块名、实例名和文件名，不要把它们当成一个标识符。

任务：读懂 |=> 与三条属性

property p_valid_response;
  @(posedge clk) disable iff (!rst_n)
    req_valid |=> rsp_valid;
endproperty
 
property p_no_spurious_response;
  @(posedge clk) disable iff (!rst_n)
    !req_valid |=> !rsp_valid;
endproperty
 
property p_result_hold;
  @(posedge clk) disable iff (!rst_n)
    !req_valid |=> $stable(result);
endproperty

这些是当前工程的关键片段；源码还为每条 property 命名了 assert 并在失败时 $fatal。|-> 检查同一次采样，|=> 检查下一次采样。DUT 在上升沿用非阻塞赋值更新 rsp_valid/result，SVA 在该沿采样到的是更新前的值；下一上升沿采样才能看到上一沿寄存的响应。因此本例用 |=>。$stable(result) 比较相邻两次采样的结果；复位期间用 disable iff (!rst_n) 取消这些正常运行断言。

任务：避免复位释放竞态

top 的 reset_dut() 将 rst_n 异步拉低，短暂等待后以 !== 检查 rsp_valid===0 且 result===0，保持两个上升沿，再在下降沿拉高 rst_n，避开 DUT 的上升沿采样竞争。运行中先让 6+9 产生 15，再调用复位任务，可以检查复位不是只在初始零状态下“看起来有效”。这里的 $fatal 消息应描述“复位输出未清零”，不能误写为“复位未释放”。

任务：用反例验证断言能抓错

“正常仿真不报错”只说明当前激励没有违反断言；反例验证要故意制造违规波形并核对目标断言名称。以下三次实验各自重新启动仿真，并以当前测试时序为前提。在 sim 目录、已编译 work.tb_top 后，使用实际的 Questa 可执行文件运行：

# 请求后没有响应：45 ns 触发 a_valid_response
vsim -c -sv_seed 12345 work.tb_top -do "onfinish stop; run 41ns; force -freeze /tb_top/vif/rsp_valid 1'b0; run -all; quit -f"
 
# 没有请求却出现响应：55 ns 触发 a_no_spurious_response
vsim -c -sv_seed 12345 work.tb_top -do "onfinish stop; run 41ns; force -freeze /tb_top/vif/rsp_valid 1'b1; run -all; quit -f"
 
# 空闲后结果改变：55 ns 触发 a_result_hold
vsim -c -sv_seed 12345 work.tb_top -do "onfinish stop; run 46ns; force -freeze /tb_top/vif/result 8'h00; run -all; quit -f"

第一笔请求在 35 ns 上升沿采样。45 ns 的空闲采样是后两条属性的起点。若在 41 ns 就把 result 固定为零，45 与 55 ns 可能都读到零，$stable 反而不失败；因此在 45 ns 采样之后的 46 ns 改值。force 不改源代码，只作用于该次仿真。命令里的 quit -f 可能使退出码不足以表示断言失败，必须检查输出中是否出现预期的断言名、时间和 Fatal。反例实验不是正常回归通过。

任务：三种子回归与证据边界

当前 run.do 在编译后，对种子 12345 67890 24212 逐个执行：

foreach seed {12345 67890 24212} {
  vsim -onfinish stop -sv_seed $seed work.tb_top
  run -all
  quit -sim
}
quit -f

run.bat 调用回归脚本，解析每轮摘要并保存日志。本机实测三轮均为 PASS=37 FAIL=0，合法操作码覆盖率 100%。每个种子都需独立运行；连续写几个 vsim 却只写一次 run -all 不构成多种子回归。

三种子通过仍不能证明没有错误：样本有限；随机约束排除了非法码，故需定向测试；覆盖率只数六种合法 op；参考模型与 DUT 也可能犯相同错误。准确结论是“这些需求和样本下未发现错误”。其它报错先按 运行与编译排错 的顺序定位。