使用 SymbiYosys 对状态机进行形式验证未给出预期结果

Question

我正在尝试使用 SymbiYosys 验证用 verilog 编写的非常简单的状态机。它失败了，我无法弄清楚我做错了什么，并且需要一些帮助来解决它。我有一个传入的请求信号，状态机将循环通过 LED 将它们一一点亮，然后再熄灭。

归纳步骤中发生的情况是输出信号设置为零，并且基于

o_led

的

state

断言失败。

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：

在上图中，您可以看到 o_led 如何为零，即使状态尚未达到其最高值。

我的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;

    // As soon as we start the sequence, stay busy until we finish.
    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

// Verification code.
`ifdef  FORMAL
    reg f_past_valid;
    initial f_past_valid = 0;
    always @(posedge i_clk)
        f_past_valid = 1'b1;

    initial assume(!i_req);
    // No overlapping requests.
    always @(posedge i_clk)
    if (busy)
    begin
        assume(!i_req);
    end

    always @(posedge i_clk)
    begin
        // At some point, we should be busy and then not busy.
        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

Answer 1

Yosys 正在为驱动器

o_led

的值的案例开关合成一个ROM，您似乎遇到了https://github.com/YosysHQ/yosys/issues/3378中描述的问题。

基本上，这是 yosys 中现有的错误，涉及 SMT 求解器中如何表示 ROM 内存。作为解决方法，您可以在 sby 文件的

memory_map -rom-only

部分末尾添加

[script]

，如下所示：

[script]
read -formal cascade.v
prep -top cascade
memory_map -rom-only

使用

abc pdr

引擎而不是

smtbmc

似乎也适用于这种情况。