data/full_repos/permissive/153960117/hdl/str_gbox.v
data/verilator_xmls/77bd65fe-1df0-46fe-8293-f12775db9d16.xml
module str_gbox
  #(parameter
    DATA_UP_WIDTH   = 2,
    DATA_DN_WIDTH   = 8)
   (input  logic                        clk,
    input  logic                        rst,

    input  logic [DATA_UP_WIDTH-1:0]    up_data,
    input  logic                        up_last,
    input  logic                        up_val,
    output logic                        up_rdy,

    output logic [DATA_DN_WIDTH-1:0]    dn_data,
    output logic                        dn_last,
    output logic                        dn_val,
    input  logic                        dn_rdy
);





`ifdef VERBOSE
    initial begin
        $display("<str_gbox> up words: %d, dn word: %d\n"
                , DATA_UP_WIDTH
                , DATA_DN_WIDTH
                );
`endif



    reg                         skid_val;
    reg                         skid_last;
    reg  [DATA_UP_WIDTH-1:0]    skid_data;

    wire                        up_val_i;
    wire                        up_last_i;
    wire [DATA_UP_WIDTH-1:0]    up_data_i;

    wire                        dn_active;







    always @(posedge clk)
        skid_data <= up_data_i;




    always @(posedge clk)
        if (rst)    skid_val <= 1'b0;
        else        skid_val <= up_val_i & ~dn_active;


    always @(posedge clk)
        if (rst)    skid_last <= 1'b0;
        else        skid_last <= up_last_i & ~dn_active;



    assign up_data_i = up_rdy ? up_data : skid_data;

    assign up_last_i = up_rdy ? up_last : skid_last;

    assign up_val_i  = up_rdy ? up_val  : skid_val;



    assign dn_active = ~dn_val | dn_rdy;


    genvar xx;
    generate
        if (DATA_UP_WIDTH == DATA_DN_WIDTH) begin : PASS_




            always @(posedge clk)
                if      (rst)               up_rdy <= 1'b0;
                else if (dn_rdy | up_val)   up_rdy <= dn_active;


            always @(posedge clk)
                if      (rst)       dn_last <= 1'b0;
                else if (dn_active) dn_last <= up_last_i;


            always @(posedge clk)
                if      (rst)       dn_val <= 1'b0;
                else if (dn_active) dn_val <= up_val_i;


            always @(posedge clk)
                if (dn_active) dn_data <= up_data_i;


`ifdef FORMAL
            reg  past_exists;
            initial begin
                past_exists = 1'b0;
            end



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








            always @(posedge clk)
                if (past_exists && $past(dn_val && dn_rdy && up_rdy)) begin
                    assert(dn_data == $past(up_data));
                end



            always @(posedge clk)
                if (past_exists && $past(dn_val && dn_rdy && ~up_rdy)) begin
                    assert(dn_data == $past(skid_data));
                end







            always @(posedge clk)
                if (past_exists && $past( ~rst && up_val && up_rdy && ~dn_val)) begin
                    assert(($past(up_data) == dn_data) && dn_val);
                end



            always @(posedge clk)
                if (past_exists && $past( ~rst && up_val && up_rdy && dn_val && ~dn_rdy)) begin
                    assert(($past(up_data) == skid_data) && dn_val);
                end

`endif
        end
        else if (DATA_UP_WIDTH > DATA_DN_WIDTH) begin : SERIAL_


            localparam DATA_NB = DATA_UP_WIDTH/DATA_DN_WIDTH;


            wire [2*DATA_NB-1:0]        token_nx;
            reg  [DATA_NB-1:0]          token;
            reg  [DATA_UP_WIDTH-1:0]    serial_data;
            reg  [DATA_NB-1:0]          serial_last;
            reg  [DATA_NB-1:0]          serial_valid;

            wire                        up_active;
            reg                         up_rdy_i;



            assign up_active    = up_val_i & token[0];

            assign up_rdy       = up_rdy_i & token[0];




            always @(posedge clk)
                if      (rst)                           up_rdy_i <= 1'b0;
                else if ((dn_rdy & token[0]) | up_val)  up_rdy_i <= dn_active;



            assign token_nx = {token, token};


            always @(posedge clk)
                if (rst) token <= 'b1;
                else if (dn_active) begin

                    if ( ~token[0] | up_active) begin
                        token <= token_nx[DATA_NB-1 +: DATA_NB];
                    end
                end


            always @(posedge clk)
                if (dn_active) begin

                    serial_data <= serial_data >> DATA_DN_WIDTH;
                    if (up_active) begin
                        serial_data <= up_data_i;
                    end
                end


            always @(posedge clk)
                if (rst) serial_last <= 'b0;
                else if (dn_active) begin

                    serial_last <= serial_last >> 1;
                    if (up_active & up_last_i) begin
                        serial_last             <= 'b0;
                        serial_last[DATA_NB-1]  <= 1'b1;
                    end
                end


            always @(posedge clk)
                if (rst) serial_valid <= 'b0;
                else if (dn_active) begin

                    serial_valid <= serial_valid >> 1;
                    if (up_active) begin
                        serial_valid <= {DATA_NB{1'b1}};
                    end
                end



            assign dn_data  = serial_data[0 +: DATA_DN_WIDTH];

            assign dn_last  = serial_last[0];

            assign dn_val   = serial_valid[0];


`ifdef FORMAL
            reg  past_exists;
            reg  past_wait;
            initial begin
                past_exists = 1'b0;
                past_wait   = 1'b0;
            end



            always @(posedge clk)
                {past_exists, past_wait} <= {past_wait, 1'b1};


            reg  [DATA_UP_WIDTH-1:0]    up_data_a;
            reg  [DATA_UP_WIDTH-1:0]    up_data_b;
            reg  [DATA_UP_WIDTH-1:0]    up_current;
            reg  [DATA_DN_WIDTH-1:0]    up_str [0:DATA_NB-1];
            reg                         up_wr;
            reg                         up_rd;
            integer                     cnt;
            reg                         cnt_done;




            always @(posedge clk)
                if      (rst)               up_wr <= 1'b0;
                else if (up_val & up_rdy)   up_wr <= ~up_wr;


            always @(posedge clk)
                if      (rst)       up_rd <= 1'b0;
                else if (cnt_done)  up_rd <= ~up_rd;


            always @(posedge clk)
                if (up_val & up_rdy & ~up_wr)   up_data_a <= up_data;


            always @(posedge clk)
                if (up_val & up_rdy &  up_wr)   up_data_b <= up_data;


            always @(posedge clk)
                if (up_rd)  up_current <= up_data_b;
                else        up_current <= up_data_a;


            for (xx = 0; xx < DATA_NB; xx = xx + 1) begin

                assign up_str[xx] = up_current[xx*DATA_DN_WIDTH +: DATA_DN_WIDTH];

            end





            always @(posedge clk) begin
                if (rst) begin
                    cnt         <=  'b0;
                    cnt_done    <= 1'b0;
                end
                else begin
                    cnt_done    <= 1'b0;

                    if (dn_val & dn_rdy) begin
                        cnt <= cnt + 'd1;

                        if (cnt >= (DATA_NB-1)) begin
                            cnt         <= 'b0;
                            cnt_done    <= 1'b1;
                        end
                    end
                end
            end


            always @(posedge clk)
                if (past_exists && $past((dn_val & dn_rdy), 2)) begin
                    assert($past(dn_data, 2) == up_str[$past(cnt, 2)]);
                end


`endif
        end
        else if (DATA_UP_WIDTH < DATA_DN_WIDTH) begin : DSERIAL_

            localparam DATA_NB = DATA_DN_WIDTH/DATA_UP_WIDTH;

            integer                     ii;
            wire [2*DATA_NB-1:0]        token_nx;
            reg  [DATA_NB-1:0]          token;





            always @(posedge clk)
                if      (rst)               up_rdy <= 1'b0;
                else if (dn_rdy | up_val)   up_rdy <= dn_active;



            assign token_nx = {token, token};


            always @(posedge clk)
                if (rst) dn_last <= 1'b0;
                else if (dn_active) begin
                    dn_last <= up_val_i & up_last_i;
                end


            always @(posedge clk)
                if (rst) dn_val <= 1'b0;
                else if (dn_active) begin
                    dn_val <= (token[DATA_NB-1] & up_val_i) | (up_val_i & up_last_i);
                end


            always @(posedge clk)
                if (rst | (dn_active & up_val_i & up_last_i)) token <= 'b1;
                else if (dn_active & up_val_i) begin
                    token <= token_nx[DATA_NB-1 +: DATA_NB];
                end


            always @(posedge clk)
                for (ii=0; ii<DATA_NB; ii=ii+1) begin
                    if (dn_active & token[0]) begin
                        dn_data[ii*DATA_UP_WIDTH +: DATA_UP_WIDTH] <= {DATA_UP_WIDTH{1'b0}};
                    end

                    if (dn_active & token[ii]) begin
                        dn_data[ii*DATA_UP_WIDTH +: DATA_UP_WIDTH] <= up_data_i;
                    end
                end


`ifdef FORMAL
            reg  past_exists;
            initial begin
                past_exists = 1'b0;
            end



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


            reg  [DATA_DN_WIDTH-1:0]    up_data_1p;
            reg  [DATA_DN_WIDTH-1:0]    up_data_2p;
            integer                     cnt;
            reg                         cnt_done;





            always @(posedge clk) begin
                if (rst) begin
                    cnt         <=  'b0;
                    cnt_done    <= 1'b0;
                end
                else begin
                    cnt_done    <= 1'b0;

                    if (up_val & up_rdy) begin
                        cnt <= cnt + 'd1;

                        if ((cnt >= (DATA_NB-1)) || up_last) begin
                            cnt         <= 'b0;
                            cnt_done    <= 1'b1;
                        end
                    end
                end
            end


            always @(posedge clk)
                if (up_val & up_rdy) begin
                    if (cnt == 0) begin
                        up_data_1p <= {DATA_DN_WIDTH{1'b0}};
                    end

                    up_data_1p[cnt*DATA_UP_WIDTH +: DATA_UP_WIDTH] <= up_data;
                end


            always @(posedge clk)
                if (cnt_done) begin
                    up_data_2p  <= up_data_1p;
                end


            always @(posedge clk)
                if (past_exists && $past(dn_val & dn_rdy)) begin
                    assert($past(dn_data) == up_data_2p);
                end

`endif

        end
    endgenerate


`ifdef FORMAL

`ifdef STR_GBOX
`define ASSUME assume
`else
`define ASSUME assert
`endif


    reg  past_exists;
    initial begin
        past_exists = 1'b0;


        rst = 1'b1;
    end



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









    always @(posedge clk)
        if (past_exists && ~rst && $past( ~up_rdy)) begin
            assert($stable(skid_data));
            assert($stable(skid_val));
            assert($stable(skid_last));
        end




    always @(posedge clk)
        if ( ~rst && $fell(up_rdy)) begin
            assert(skid_data == $past(up_data));
        end








    always @(posedge clk)
        if (past_exists && $past(up_val && ~up_rdy)) begin
            `ASSUME($stable(up_data));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(up_val)) begin
            `ASSUME($past(up_rdy));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(up_last)) begin
            `ASSUME($past(up_rdy) && $past(up_val));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(up_rdy)) begin
            assert($past(up_val));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $past(dn_val && ~dn_rdy)) begin
            assert($stable(dn_data));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(dn_val)) begin
            assert($past(dn_rdy));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(dn_last)) begin
            assert($past(dn_rdy) && $past(dn_val));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(dn_rdy)) begin
            `ASSUME($past(dn_val));
        end


`endif
endmodule
module str_gbox
  #(parameter
    DATA_UP_WIDTH   = 2,
    DATA_DN_WIDTH   = 8)
   (input  logic                        clk,
    input  logic                        rst,

    input  logic [DATA_UP_WIDTH-1:0]    up_data,
    input  logic                        up_last,
    input  logic                        up_val,
    output logic                        up_rdy,

    output logic [DATA_DN_WIDTH-1:0]    dn_data,
    output logic                        dn_last,
    output logic                        dn_val,
    input  logic                        dn_rdy
);






`ifdef VERBOSE
    initial begin
        $display("<str_gbox> up words: %d, dn word: %d\n"
                , DATA_UP_WIDTH
                , DATA_DN_WIDTH
                );
`endif



    reg                         skid_val;
    reg                         skid_last;
    reg  [DATA_UP_WIDTH-1:0]    skid_data;

    wire                        up_val_i;
    wire                        up_last_i;
    wire [DATA_UP_WIDTH-1:0]    up_data_i;

    wire                        dn_active;







    always @(posedge clk)
        skid_data <= up_data_i;




    always @(posedge clk)
        if (rst)    skid_val <= 1'b0;
        else        skid_val <= up_val_i & ~dn_active;


    always @(posedge clk)
        if (rst)    skid_last <= 1'b0;
        else        skid_last <= up_last_i & ~dn_active;



    assign up_data_i = up_rdy ? up_data : skid_data;

    assign up_last_i = up_rdy ? up_last : skid_last;

    assign up_val_i  = up_rdy ? up_val  : skid_val;



    assign dn_active = ~dn_val | dn_rdy;


    genvar xx;
    generate
        if (DATA_UP_WIDTH == DATA_DN_WIDTH) begin : PASS_




            always @(posedge clk)
                if      (rst)               up_rdy <= 1'b0;
                else if (dn_rdy | up_val)   up_rdy <= dn_active;


            always @(posedge clk)
                if      (rst)       dn_last <= 1'b0;
                else if (dn_active) dn_last <= up_last_i;


            always @(posedge clk)
                if      (rst)       dn_val <= 1'b0;
                else if (dn_active) dn_val <= up_val_i;


            always @(posedge clk)
                if (dn_active) dn_data <= up_data_i;


`ifdef FORMAL
            reg  past_exists;
            initial begin
                past_exists = 1'b0;
            end



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








            always @(posedge clk)
                if (past_exists && $past(dn_val && dn_rdy && up_rdy)) begin
                    assert(dn_data == $past(up_data));
                end



            always @(posedge clk)
                if (past_exists && $past(dn_val && dn_rdy && ~up_rdy)) begin
                    assert(dn_data == $past(skid_data));
                end







            always @(posedge clk)
                if (past_exists && $past( ~rst && up_val && up_rdy && ~dn_val)) begin
                    assert(($past(up_data) == dn_data) && dn_val);
                end



            always @(posedge clk)
                if (past_exists && $past( ~rst && up_val && up_rdy && dn_val && ~dn_rdy)) begin
                    assert(($past(up_data) == skid_data) && dn_val);
                end

`endif
        end
        else if (DATA_UP_WIDTH > DATA_DN_WIDTH) begin : SERIAL_


            localparam DATA_NB = DATA_UP_WIDTH/DATA_DN_WIDTH;


            wire [2*DATA_NB-1:0]        token_nx;
            reg  [DATA_NB-1:0]          token;
            reg  [DATA_UP_WIDTH-1:0]    serial_data;
            reg  [DATA_NB-1:0]          serial_last;
            reg  [DATA_NB-1:0]          serial_valid;

            wire                        up_active;
            reg                         up_rdy_i;



            assign up_active    = up_val_i & token[0];

            assign up_rdy       = up_rdy_i & token[0];




            always @(posedge clk)
                if      (rst)                           up_rdy_i <= 1'b0;
                else if ((dn_rdy & token[0]) | up_val)  up_rdy_i <= dn_active;



            assign token_nx = {token, token};


            always @(posedge clk)
                if (rst) token <= 'b1;
                else if (dn_active) begin

                    if ( ~token[0] | up_active) begin
                        token <= token_nx[DATA_NB-1 +: DATA_NB];
                    end
                end


            always @(posedge clk)
                if (dn_active) begin

                    serial_data <= serial_data >> DATA_DN_WIDTH;
                    if (up_active) begin
                        serial_data <= up_data_i;
                    end
                end


            always @(posedge clk)
                if (rst) serial_last <= 'b0;
                else if (dn_active) begin

                    serial_last <= serial_last >> 1;
                    if (up_active & up_last_i) begin
                        serial_last             <= 'b0;
                        serial_last[DATA_NB-1]  <= 1'b1;
                    end
                end


            always @(posedge clk)
                if (rst) serial_valid <= 'b0;
                else if (dn_active) begin

                    serial_valid <= serial_valid >> 1;
                    if (up_active) begin
                        serial_valid <= {DATA_NB{1'b1}};
                    end
                end



            assign dn_data  = serial_data[0 +: DATA_DN_WIDTH];

            assign dn_last  = serial_last[0];

            assign dn_val   = serial_valid[0];


`ifdef FORMAL
            reg  past_exists;
            reg  past_wait;
            initial begin
                past_exists = 1'b0;
                past_wait   = 1'b0;
            end



            always @(posedge clk)
                {past_exists, past_wait} <= {past_wait, 1'b1};


            reg  [DATA_UP_WIDTH-1:0]    up_data_a;
            reg  [DATA_UP_WIDTH-1:0]    up_data_b;
            reg  [DATA_UP_WIDTH-1:0]    up_current;
            reg  [DATA_DN_WIDTH-1:0]    up_str [0:DATA_NB-1];
            reg                         up_wr;
            reg                         up_rd;
            integer                     cnt;
            reg                         cnt_done;




            always @(posedge clk)
                if      (rst)               up_wr <= 1'b0;
                else if (up_val & up_rdy)   up_wr <= ~up_wr;


            always @(posedge clk)
                if      (rst)       up_rd <= 1'b0;
                else if (cnt_done)  up_rd <= ~up_rd;


            always @(posedge clk)
                if (up_val & up_rdy & ~up_wr)   up_data_a <= up_data;


            always @(posedge clk)
                if (up_val & up_rdy &  up_wr)   up_data_b <= up_data;


            always @(posedge clk)
                if (up_rd)  up_current <= up_data_b;
                else        up_current <= up_data_a;


            for (xx = 0; xx < DATA_NB; xx = xx + 1) begin

                assign up_str[xx] = up_current[xx*DATA_DN_WIDTH +: DATA_DN_WIDTH];

            end





            always @(posedge clk) begin
                if (rst) begin
                    cnt         <=  'b0;
                    cnt_done    <= 1'b0;
                end
                else begin
                    cnt_done    <= 1'b0;

                    if (dn_val & dn_rdy) begin
                        cnt <= cnt + 'd1;

                        if (cnt >= (DATA_NB-1)) begin
                            cnt         <= 'b0;
                            cnt_done    <= 1'b1;
                        end
                    end
                end
            end


            always @(posedge clk)
                if (past_exists && $past((dn_val & dn_rdy), 2)) begin
                    assert($past(dn_data, 2) == up_str[$past(cnt, 2)]);
                end


`endif
        end
        else if (DATA_UP_WIDTH < DATA_DN_WIDTH) begin : DSERIAL_

            localparam DATA_NB = DATA_DN_WIDTH/DATA_UP_WIDTH;

            integer                     ii;
            wire [2*DATA_NB-1:0]        token_nx;
            reg  [DATA_NB-1:0]          token;





            always @(posedge clk)
                if      (rst)               up_rdy <= 1'b0;
                else if (dn_rdy | up_val)   up_rdy <= dn_active;



            assign token_nx = {token, token};


            always @(posedge clk)
                if (rst) dn_last <= 1'b0;
                else if (dn_active) begin
                    dn_last <= up_val_i & up_last_i;
                end


            always @(posedge clk)
                if (rst) dn_val <= 1'b0;
                else if (dn_active) begin
                    dn_val <= (token[DATA_NB-1] & up_val_i) | (up_val_i & up_last_i);
                end


            always @(posedge clk)
                if (rst | (dn_active & up_val_i & up_last_i)) token <= 'b1;
                else if (dn_active & up_val_i) begin
                    token <= token_nx[DATA_NB-1 +: DATA_NB];
                end


            always @(posedge clk)
                for (ii=0; ii<DATA_NB; ii=ii+1) begin
                    if (dn_active & token[0]) begin
                        dn_data[ii*DATA_UP_WIDTH +: DATA_UP_WIDTH] <= {DATA_UP_WIDTH{1'b0}};
                    end

                    if (dn_active & token[ii]) begin
                        dn_data[ii*DATA_UP_WIDTH +: DATA_UP_WIDTH] <= up_data_i;
                    end
                end


`ifdef FORMAL
            reg  past_exists;
            initial begin
                past_exists = 1'b0;
            end



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


            reg  [DATA_DN_WIDTH-1:0]    up_data_1p;
            reg  [DATA_DN_WIDTH-1:0]    up_data_2p;
            integer                     cnt;
            reg                         cnt_done;





            always @(posedge clk) begin
                if (rst) begin
                    cnt         <=  'b0;
                    cnt_done    <= 1'b0;
                end
                else begin
                    cnt_done    <= 1'b0;

                    if (up_val & up_rdy) begin
                        cnt <= cnt + 'd1;

                        if ((cnt >= (DATA_NB-1)) || up_last) begin
                            cnt         <= 'b0;
                            cnt_done    <= 1'b1;
                        end
                    end
                end
            end


            always @(posedge clk)
                if (up_val & up_rdy) begin
                    if (cnt == 0) begin
                        up_data_1p <= {DATA_DN_WIDTH{1'b0}};
                    end

                    up_data_1p[cnt*DATA_UP_WIDTH +: DATA_UP_WIDTH] <= up_data;
                end


            always @(posedge clk)
                if (cnt_done) begin
                    up_data_2p  <= up_data_1p;
                end


            always @(posedge clk)
                if (past_exists && $past(dn_val & dn_rdy)) begin
                    assert($past(dn_data) == up_data_2p);
                end

`endif

        end
    endgenerate


`ifdef FORMAL

`ifdef STR_GBOX
`define ASSUME assume
`else
`define ASSUME assert
`endif


    reg  past_exists;
    initial begin
        past_exists = 1'b0;


        rst = 1'b1;
    end



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









    always @(posedge clk)
        if (past_exists && ~rst && $past( ~up_rdy)) begin
            assert($stable(skid_data));
            assert($stable(skid_val));
            assert($stable(skid_last));
        end




    always @(posedge clk)
        if ( ~rst && $fell(up_rdy)) begin
            assert(skid_data == $past(up_data));
        end








    always @(posedge clk)
        if (past_exists && $past(up_val && ~up_rdy)) begin
            `ASSUME($stable(up_data));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(up_val)) begin
            `ASSUME($past(up_rdy));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(up_last)) begin
            `ASSUME($past(up_rdy) && $past(up_val));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(up_rdy)) begin
            assert($past(up_val));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $past(dn_val && ~dn_rdy)) begin
            assert($stable(dn_data));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(dn_val)) begin
            assert($past(dn_rdy));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(dn_last)) begin
            assert($past(dn_rdy) && $past(dn_val));
        end



    always @(posedge clk)
        if (past_exists && $past( ~rst) && $fell(dn_rdy)) begin
            `ASSUME($past(dn_val));
        end


`endif
endmodule