Formal verification of synchronous FIFO with failing SystemVerilog assertion

Question

I am trying to verify Synchronous FIFO using SymbiYosys formally. However, I am unable to make sense of the failing counterexample trace. Should I add more assertions or constrain the existing failing assertion on data consistency? I am looking for better ways to analyze failing assertion

module fifo 
    #(
    parameter WIDTH = 8,
    parameter PTR_BITS = 2
    )
 (
    input  logic             clk,
    input  logic             rst_n,

    input  logic             wr_i,
    input  logic [WIDTH-1:0] data_i,

    input  logic             rd_i,
    output logic [WIDTH-1:0] data_o,

    output logic             empty_o,
    output logic             full_o
);

localparam DEPTH = 2**PTR_BITS;

logic [WIDTH-1:0] mem [DEPTH];
// logic [PTR_BITS-1:0] head_r, head_nxt, tail_r, tail_nxt;
logic [PTR_BITS:0] head_r, head_nxt, tail_r, tail_nxt; // addition bit to detect full/empty condition

logic wrap_around_bit;

always_ff @(posedge clk) begin
    head_r <= head_nxt;
    tail_r <= tail_nxt;

    if (!rst_n) begin
        head_r <= '0;
        tail_r <= '0;
    end

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

always_comb begin
    head_nxt = head_r;
    tail_nxt = tail_r;

    if (wr_i)
        head_nxt = head_nxt + PTR_BITS'(1);

    if (rd_i)
        tail_nxt = tail_nxt + PTR_BITS'(1);
end

assign wrap_around_bit = head_r[PTR_BITS] ^ tail_r[PTR_BITS];

assign data_o = mem[tail_r];
assign empty_o = head_r == tail_r;
// assign full_o = head_r == (tail_r - PTR_BITS'(1));
assign full_o = (head_r[PTR_BITS-1:0] == tail_r[PTR_BITS-1:0]) && wrap_around_bit;

`ifdef FORMAL

initial assume(!rst_n);

reg f_past_valid;

initial f_past_valid = 0;

always @(posedge clk)
    f_past_valid <= 1'b1;

//empty
always @*
    begin if(head_r == tail_r)
        assert(empty_o);
    end

//full
always @*
    begin if( (head_r == tail_r) && wrap_around_bit)
        assert(full_o);
    end

//no read on empty
always @*
    begin
        if(empty_o)
            assume(!rd_i);
    end

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


/* THIS PROPERTY FAILS
// Check in the next clock cycle to ensure memory has been pdated
always @(posedge clk) begin
    if (f_past_valid &&  $past(rst_n) && ($past(full_o) == 0) && $past(wr_i) && !$past(wrap_around_bit)) 
        assert(mem[($past(head_r))] == $past(data_i));
    end

`endif
endmodule

Here is the Symbi-Yosys Log excerpt

SBY 13:24:36 [fifo] engine_0.basecase: ##   0:00:00  BMC failed!
SBY 13:24:36 [fifo] engine_0.basecase: ##   0:00:00  Assert failed in fifo: fifo.sv:101 ($auto$verificsva.cc:1726:import$117)
SBY 13:24:36 [fifo] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 11..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 10..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 9..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 8..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 7..
SBY 13:24:36 [fifo] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 6..
SBY 13:24:36 [fifo] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 13:24:36 [fifo] engine_0.basecase: ##   0:00:00  Writing trace to Yosys witness file: engine_0/trace.yw
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 5..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 4..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 3..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 2..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 1..
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Trying induction in step 0..
SBY 13:24:36 [fifo] engine_0.basecase: ##   0:00:00  Status: failed
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Temporal induction failed!
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Assert failed in fifo: fifo.sv:101 ($auto$verificsva.cc:1726:import$117)
SBY 13:24:36 [fifo] engine_0.induction: ##   0:00:00  Writing trace to VCD file: engine_0/trace_induct.vcd

Are there better ways to debug failing assertions?

Answer 1

It seems the problem was increasing the size of head_r to detect full condition. As soon as I reverted the full_o to be

assign full_o = head_r == (tail_r - PTR_BITS'(1));

Here is the complete code

    module fifo 
        #(
        parameter WIDTH = 8,
        parameter PTR_BITS = 1
        )
     (
        input  logic             clk,
        input  logic             rst_n,
    
        input  logic             wr_i,
        input  logic [WIDTH-1:0] data_i,
    
        input  logic             rd_i,
        output logic [WIDTH-1:0] data_o,
    
        output logic             empty_o,
        output logic             full_o
    );
    
    localparam DEPTH = 2**PTR_BITS;
    
    logic [WIDTH-1:0] mem [DEPTH];
    logic [PTR_BITS-1:0] head_r, head_nxt, tail_r, tail_nxt;
    // logic [PTR_BITS:0] head_r, head_nxt, tail_r, tail_nxt; // addition bit to detect full/empty condition
    
    logic wrap_around_bit;
    
    always_ff @(posedge clk) begin
        head_r <= head_nxt;
        tail_r <= tail_nxt;
    
        if (!rst_n) begin
            head_r <= '0;
            tail_r <= '0;
        end
    
        if (wr_i)
            mem[head_r] <= data_i;
    end
    
    always_comb begin
        head_nxt = head_r;
        tail_nxt = tail_r;
    
        if (wr_i)
            head_nxt = head_nxt + PTR_BITS'(1);
    
        if (rd_i)
            tail_nxt = tail_nxt + PTR_BITS'(1);
    end
    
    // assign wrap_around_bit = head_r[PTR_BITS] ^ tail_r[PTR_BITS];
    
    assign data_o = mem[tail_r];
    assign empty_o = head_r == tail_r;
    assign full_o = head_r == (tail_r - PTR_BITS'(1));
    // assign full_o = (head_r[PTR_BITS-1:0] == tail_r[PTR_BITS-1:0]) && wrap_around_bit;
    
    `ifdef FORMAL
    
    initial assume(!rst_n);
    
    reg f_past_valid;
    
    initial f_past_valid = 0;
    
    always @(posedge clk)
        f_past_valid <= 1'b1;
    
    //empty
    always @*
        begin if(head_r == tail_r)
            assert(empty_o);
        end
    
    //full
    always @*
        begin if( (head_r == tail_r -1)/* && wrap_around_bit*/)
            assert(full_o);
        end
    
    //no read on empty
    always @*
        begin
            if(empty_o)
                assume(!rd_i);
        end
    
    //no write on full
    always @*
        begin
            if(full_o)
                assume(!wr_i);
        end


// Check in the next clock cycle to ensure memory has updated
always @(posedge clk) begin
    if (f_past_valid &&  $past(rst_n) && ($past(full_o) == 0) && $past(wr_i) ) 
        assert(mem[($past(head_r))] == $past(data_i));
    end

`endif
endmodule