skid buffer proved by smtbmc but fail by abc pdr

[jimmysitu]

Hi, Dan

I try to use the formal assertion you mention in your blog and prove an other skid buffer from Altera(Intel) on github

Then I get a induction fail with smtbmc engine, it fails at Rule #3: After the last transaction, valid_o should become idle The trace_induct.vcd give a fail trace which seems start with an impossible initial state. backup_valid would never valid when there is no valid_o and valid_i. But when I change the engine to abc pdr, it PASS.

I have no idea why different proof engine gets different result, could you help explain that?

Attached ready_skid.v with formal property and .sby file BTW, I mask Rule #1 since this skid buffer has a different reset behavior

// Copyright 2008 Altera Corporation. All rights reserved.  
// Altera products are protected under numerous U.S. and foreign patents, 
// maskwork rights, copyrights and other intellectual property laws.  
//
// This reference design file, and your use thereof, is subject to and governed
// by the terms and conditions of the applicable Altera Reference Design 
// License Agreement (either as signed by you or found at www.altera.com).  By
// using this reference design file, you indicate your acceptance of such terms
// and conditions between you and Altera Corporation.  In the event that you do
// not agree with such terms and conditions, you may not use the reference 
// design file and please promptly destroy any copies you have made.
//
// This reference design file is being provided on an "as-is" basis and as an 
// accommodation and therefore all warranties, representations or guarantees of 
// any kind (whether express, implied or statutory) including, without 
// limitation, warranties of merchantability, non-infringement, or fitness for
// a particular purpose, are specifically disclaimed.  By making this reference
// design file available, Altera expressly does not recommend, suggest or 
// require that this reference design file be used in combination with any 
// other product not provided by Altera.
/////////////////////////////////////////////////////////////////////////////

// baeckler - 11-06-2008
// pipeline for ready / valid data

module ready_skid #(
    parameter WIDTH = 16
)
(
    input clk,arst,

    input valid_i,
    input [WIDTH-1:0] dat_i,
    output reg ready_i,

    output reg valid_o,
    output reg [WIDTH-1:0] dat_o,
    input ready_o   
);

reg [WIDTH-1:0] backup_storage;
reg backup_valid;

// duplicate control registers to mitigate
// high fanout loading.
reg internal_valid_o /* synthesis preserve */;
reg internal_ready_i /* synthesis preserve */;

`ifndef FORMAL
// simulation only sanity check
always @(posedge clk) begin
    if ((ready_i != internal_ready_i) || 
        (valid_o != internal_valid_o)) begin
        $display ("Error: Duplicate internal regs out of sync");    
    end
end
`else
always @(posedge clk) begin
    assert(ready_i == internal_ready_i);
    assert(valid_o == internal_valid_o);
end
`endif

always @(posedge clk or posedge arst) begin
    if (arst) begin
        ready_i <= 1'b0;
        internal_ready_i <= 1'b0;
        valid_o <= 1'b0;
        internal_valid_o <= 1'b0;
        dat_o <= 0;
        backup_storage <= 0;
        backup_valid <= 1'b0;
    end
    else begin
        ready_i <= ready_o;
        internal_ready_i <= ready_o;

        if (internal_valid_o & ready_o) begin
            // main data is leaving to the sink
            if (backup_valid) begin
                // dump the backup word to main storage
                backup_valid <= 1'b0;
                dat_o <= backup_storage;
                valid_o <= 1'b1;    
                internal_valid_o <= 1'b1;   
                if (ready_i && valid_i) begin
                    $display ("ERROR: data lost in skid buffer");
                end
            end
            else begin
                // if not overwritten below, you are done.
                valid_o <= 1'b0;
                internal_valid_o <= 1'b0;
            end
        end

        if (internal_ready_i && valid_i) begin
            // must accept data from source
            if (ready_o || !internal_valid_o) begin
                // accept to main registers
                valid_o <= 1'b1;
                internal_valid_o <= 1'b1;
                dat_o <= dat_i;
            end
            else begin
                // accept to backup storage
                backup_valid <= 1'b1;
                backup_storage <= dat_i;
                ready_i <= 1'b0; // stop stop!
                internal_ready_i <= 1'b0;
            end
        end         
    end
end

`ifdef FORMAL
    reg f_past_valid;

    initial f_past_valid = 0;
    always @(posedge clk)
        f_past_valid <= 1;

    always @(*)
    if (!f_past_valid)
        assume(arst);

    ////////////////////////////////////////////////////////////////////////
    // Incoming stream properties / assumptions
    ////////////////////////////////////////////////////////////////////////
    //
    always @(posedge clk)
    if (!f_past_valid) begin
        assume property(!valid_i);
    end else if ($past(valid_i && !ready_i && !arst) && !arst) begin
        assume property(valid_i && $stable(dat_i));
    end

    ////////////////////////////////////////////////////////////////////////
    // Outgoing stream properties / assumptions
    ////////////////////////////////////////////////////////////////////////
    //
    always @(posedge clk)
        if (!f_past_valid) begin
            // Following any reset, valid must be deasserted
            assert property(!valid_o);
        end else if ($past(valid_o && !ready_o && !arst) && !arst) begin
            // Following any stall, valid must remain high and
            // data must be preserved
            assert property(valid_o && $stable(dat_o));
        end

    ////////////////////////////////////////////////////////////////////////
    // Other properties
    ////////////////////////////////////////////////////////////////////////
    //
    // Rule #1:
    //  If registered, then following any reset we should be
    //  ready for a new request
//    always @(posedge clk)
//        if (f_past_valid && $past(arst))
//            prf_rst_rdy: assert property(ready_i);

    // Rule #2:
    //  All incoming data must either go directly to the
    //  output port, or into the skid buffer
    always @(posedge clk)
        if(f_past_valid && !arst && !$past(arst) && $past(valid_i && ready_i && valid_o && !ready_o))
            prf_dat: assert(!ready_i && backup_storage == $past(dat_i));

    // Rule #3:
    //  After the last transaction, valid_o should become idle
    always @(posedge clk)
        if (f_past_valid && !arst && !$past(arst)) begin
            if ($past(valid_i && ready_i))
                assert(valid_o);

            if ($past(!valid_i && ready_i && ready_o))
                assert(!valid_o);
        end

    // Rule #4
    //  Same thing, but this time for ready_i
    always @(posedge clk)
        if (f_past_valid && !arst && $past(!arst && !ready_i && ready_o))
            prf_rdy: assert property(ready_i);

`endif

endmodule

[tasks]
prf     prf
cvr     cvr
bmc     bmc

[options]
prf: mode prove
prf: depth 12

cvr: mode cover
cvr: depth 20

bmc: mode bmc
bmc: depth 20

[engines]
prf: smtbmc
prf: abc pdr

[script]
read -formal ready_skid.v
--pycode-begin--
cmd = "hierarchy -top ready_skid"
output(cmd);
--pycode-end--
prep -top ready_skid

[files]
ready_skid.v

[ZipCPU]

Please see the induction chapter of my formal methods course for the reason why this might be, as well as how to fix the problem. Dan

[ZipCPU]

Almost forgot, I also discuss this same basic problem on the blog as well. Dan

[jimmysitu]

@ZipCPU greate thanks. I get the point.