使用SymbiYosys验证状态机未达预期，请求问题排查

我用SymbiYosys验证Verilog编写的简单状态机，验证失败无法定位问题。该状态机接收请求信号后，会控制LED逐个亮起再逐个熄灭。

验证异常详情 #

感应步骤出现异常：输出信号o_led被置为0，所有基于state的o_led断言全部失败，相关日志如下：

SBY 16:51:34 [cascade_prf] summary: engine_0 (smtbmc) returned pass for basecase
SBY 16:51:34 [cascade_prf] summary: engine_0 (smtbmc) returned FAIL for induction
SBY 16:51:34 [cascade_prf] summary: counterexample trace [induction]: cascade_prf/engine_0/trace_induct.vcd
SBY 16:51:34 [cascade_prf] summary:   failed assertion cascade._witness_.check_assert_cascade_v_90_45 at cascade.v:90.10-90.31 in step 0

从VCD截图可见，state尚未达到最大值时，o_led已被置为0。

SymbiYosys配置文件 #

[tasks]
prf
cvr

[options]
prf: mode prove
cvr: mode cover

[engines]
smtbmc

[script]
read -formal cascade.v
prep -top cascade

[files]
cascade.v

运行命令 #

sby -f cascade.sby

Verilog模块代码 #

`default_nettype none


module cascade(i_clk, i_req, o_led);
    input wire i_clk;
    input wire i_req;

    output reg [5:0] o_led;

    initial o_led = 6'h0;

    wire busy;

    reg [3:0] state;
    initial state = 4'b0;

    // 启动序列后保持忙碌直到完成
    assign busy = (state != 0);

    always @(posedge i_clk)
    begin
        if (i_req && !busy)
            state <= 4'h1;
        else if (state >= 4'hb)
        begin
            state <= 4'h0;
        end
        else if (state != 0)
            state <= state + 1'b1;
    end

    always @(state)
    begin
        case(state)
            4'h1: o_led = 6'b00_0001;
            4'h2: o_led = 6'b00_0010;
            4'h3: o_led = 6'b00_0100;
            4'h4: o_led = 6'b00_1000;
            4'h5: o_led = 6'b01_0000;
            4'h6: o_led = 6'b10_0000;
            4'h7: o_led = 6'b01_0000;
            4'h8: o_led = 6'b00_1000;
            4'h9: o_led = 6'b00_0100;
            4'ha: o_led = 6'b00_0010;
            4'hb: o_led = 6'b00_0001;

            default:
                o_led = 6'b00_0000;
        endcase
    end

// 验证代码
`ifdef  FORMAL
    reg f_past_valid;
    initial f_past_valid = 0;
    always @(posedge i_clk)
        f_past_valid = 1'b1;

    initial assume(!i_req);
    // 禁止重叠请求
    always @(posedge i_clk)
    if (busy)
    begin
        assume(!i_req);
    end

    always @(posedge i_clk)
    begin
        // 覆盖"从忙碌转为空闲"的场景
        if (f_past_valid)
            cover(!busy && $past(busy));
    end

    always @(*)
    assert(busy != (state == 0));

    always @(posedge i_clk)
    if (f_past_valid && $past(busy) && $past(state) < 4'hb)
    begin
        assert(state == ($past(state) + 1));
    end

    always @(state)
    begin
        case(state)
            4'h0: assert(o_led == 6'h0);
            4'h1: assert(o_led == 6'h1);
            4'h2: assert(o_led == 6'h2);
            4'h3: assert(o_led == 6'h4);
            4'h4: assert(o_led == 6'h8);
            4'h5: assert(o_led == 6'h10);
            4'h6: assert(o_led == 6'h20);
            4'h7: assert(o_led == 6'h10);
            4'h8: assert(o_led == 6'h8);
            4'h9: assert(o_led == 6'h4);
            4'ha: assert(o_led == 6'h2);
            4'hb: assert(o_led == 6'h1);

            default:
                assert(o_led == 6'b00_0000);
        endcase
    end

    always @(*)
        assert(state <= 4'hc);

`endif

endmodule

问题排查与修复方案 #

1. 核心问题：组合逻辑的不可预测性
   你使用always @(state)驱动o_led，属于纯组合逻辑。在形式化验证的归纳步骤中，工具会假设state可以在时钟周期内跳变到任意合法值（只要不违反已有约束），但你的状态转移仅在时钟沿更新state，未约束state在时钟周期内的稳定性。工具可能生成反例：同一时钟周期内state先被设为非0值，随后跳变到默认值，导致o_led被覆盖为0。

2. 修复方案：将o_led改为时序逻辑驱动
   把驱动o_led的组合逻辑改为时钟沿触发的时序逻辑，确保o_led仅在时钟沿更新，与state保持同步：

   always @(posedge i_clk)
   begin
       case(state)
           4'h1: o_led <= 6'b00_0001;
           4'h2: o_led <= 6'b00_0010;
           4'h3: o_led <= 6'b00_0100;
           4'h4: o_led <= 6'b00_1000;
           4'h5: o_led <= 6'b01_0000;
           4'h6: o_led <= 6'b10_0000;
           4'h7: o_led <= 6'b01_0000;
           4'h8: o_led <= 6'b00_1000;
           4'h9: o_led <= 6'b00_0100;
           4'ha: o_led <= 6'b00_0010;
           4'hb: o_led <= 6'b00_0001;
   
           default:
               o_led <= 6'b00_0000;
       endcase
   end
   

3. 额外优化：约束state的合法范围
   现有断言state <= 4'hc过于宽松，状态机实际最大状态为4'hb，可修改为：

   always @(*)
       assert(state <= 4'hb);
   

   同时确保状态转移逻辑不会让state超出预期范围，避免工具生成无意义反例。

4. 验证修复效果
   修改后重新运行sby -f cascade.sby，归纳步骤应能通过，所有断言可正常验证。

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