同步FIFO形式化验证中SystemVerilog断言失效的调试咨询

问题概述 #

使用SymbiYosys对同步FIFO做形式化验证时，数据一致性断言失效，无法理解反例追踪结果，需要排查问题根源、优化断言/约束，同时寻求更高效的失效断言调试方法。

代码核心问题分析 #

先看你代码中的几个关键错误，这些是导致断言失效的直接原因：

1. 复位逻辑顺序错误 #

你的always_ff块中，先执行非复位的指针赋值，再处理复位，这不符合Verilog非阻塞赋值的并行语义，形式化工具会捕捉到复位期间的异常行为。正确的复位逻辑应该优先级最高：

always_ff @(posedge clk) begin
    if (!rst_n) begin
        head_r <= '0;
        tail_r <= '0;
    end else begin
        head_r <= head_nxt;
        tail_r <= tail_nxt;
    end

    if (wr_i)
        mem[head_r] <= data_i;
end

2. 写满约束复制粘贴错误 #

你写的“no write on full”约束完全复用了“no read on empty”的代码，导致形式化工具允许FIFO满时执行写操作，直接覆盖已有数据：

// 错误代码
//no write on full
always @*
    begin
        if(empty_o)
            assume(!rd_i);
    end

// 正确代码
//no write on full
always @*
    begin
        if(full_o)
            assume(!wr_i);
    end

3. 数据一致性断言冗余与缺失 #

原断言中的!$past(wrap_around_bit)是冗余条件，且未约束mem数组的初始值——形式化工具默认会认为mem初始值为任意值，可能导致断言误判。需要添加初始约束：

`ifdef FORMAL
initial begin
    for (int i=0; i<DEPTH; i++) begin
        mem[i] = '0; // 根据需求约束内存初始值
    end
end
// 简化后的断言
always @(posedge clk) begin
    if (f_past_valid && $past(rst_n) && !$past(full_o) && $past(wr_i)) 
        assert(mem[$past(head_r)] == $past(data_i));
end
`endif

失效断言调试优化方法 #

1. 优先分析VCD波形 #

SymbiYosys生成的trace.vcd是最直观的调试工具，用GTKWave打开后逐周期检查：

• 确认复位信号的时序是否正确
• 查看wr_i与full_o的对应关系，是否存在满时写的违规操作
• 跟踪head_r、data_i和对应mem地址的数值变化

2. 拆分复杂断言，添加辅助断言 #

把复杂断言拆成多个简单断言，快速定位问题：

// 辅助断言：验证写操作仅在FIFO非满时发生
always @(posedge clk) begin
    if (f_past_valid && $past(wr_i))
        assert(!$past(full_o));
end

这类辅助断言能帮你快速区分是约束问题还是逻辑实现问题。

3. 强化输入信号约束 #

除了空不读、满不写，还可以添加更合理的输入约束：

• 约束复位信号仅在初始时刻有效，避免持续复位：assume property (rst_n || $past(!rst_n));
• 约束写数据data_i在写操作周期保持稳定，减少反例复杂度

4. 利用SymbiYosys调试工具 #

• 在SBY配置文件中添加debug on，生成更详细的追踪信息
• 使用--trace-depth参数限制反例长度，聚焦关键周期
• 用Yosys的show命令查看形式化工具生成的模型，确认逻辑是否符合预期

内容的提问来源于stack exchange，提问作者user2979872