data/full_repos/permissive/153960117/hdl/pool.v
data/verilator_xmls/98dbfe93-a5f9-447b-97ee-28fae0a60f5f.xml
module pool
  #(parameter
    NUM_WIDTH = 16)
   (input  wire                 clk,
    input  wire                 restart,

    input  wire [NUM_WIDTH-1:0] up_data,
    input  wire                 up_valid,

    output reg  [NUM_WIDTH-1:0] dn_data
);





    function new_max;
        input signed [NUM_WIDTH-1:0] new_nb;
        input signed [NUM_WIDTH-1:0] old_nb;

        begin
            new_max = (new_nb > old_nb);
        end
    endfunction


    reg  [NUM_WIDTH-1:0]    up_data_1p;
    reg  [NUM_WIDTH-1:0]    up_data_2p;
    reg  [NUM_WIDTH-1:0]    up_data_3p;

    reg                     up_valid_1p;
    reg                     up_valid_2p;
    reg                     up_valid_3p;

    reg                     restart_1p;
    reg                     restart_2p;





    always @(posedge clk) begin
        if (restart) begin
            restart_1p <= 1'b1;
        end
        else if (restart_1p & up_valid_1p) begin
            restart_1p <= 1'b0;
        end
    end


    always @(posedge clk) begin
        restart_2p  <= restart_1p;

        up_valid_1p <= up_valid;
        up_valid_2p <= up_valid_1p;
        up_valid_3p <= up_valid_2p;
    end


    always @(posedge clk) begin
        up_data_1p   <= 'b0;

        if (up_valid) begin
            up_data_1p   <= up_data;
        end
    end


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


    always @(posedge clk) begin
        if (up_valid_2p) begin
            if (restart_2p || new_max(up_data_2p, up_data_3p)) begin
                up_data_3p <= up_data_2p;
            end
        end
    end


    always @(posedge clk)
        if (up_valid_3p) begin
            dn_data <= up_data_3p;
        end



`ifdef FORMAL

    reg         past_exists;
    reg  [2:0]  past_wait;
    initial begin
        restrict property (past_exists == 1'b0);
        restrict property (past_wait   ==  'b0);
    end


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









    always @(posedge clk)
        if (past_exists && $past(restart_1p, 3) && $past(up_valid_1p, 3)) begin
            assert(dn_data == $past(up_data_1p, 3));
        end




    always @(posedge clk)
        if (past_exists && $fell(restart_1p)) begin
            assert($past(up_valid_1p));
        end








    always @(posedge clk)
        if (past_exists && $past(up_valid_3p)) begin
            assert($signed(dn_data) >= $signed($past(up_data_3p)));
        end




    always @(posedge clk)
        if (past_exists && ($signed(up_data_3p) < $signed($past(up_data_3p)))) begin
            assert($past(restart_2p & up_valid_2p));
        end


`endif
endmodule
module pool
  #(parameter
    NUM_WIDTH = 16)
   (input  wire                 clk,
    input  wire                 restart,

    input  wire [NUM_WIDTH-1:0] up_data,
    input  wire                 up_valid,

    output reg  [NUM_WIDTH-1:0] dn_data
);






    function new_max;
        input signed [NUM_WIDTH-1:0] new_nb;
        input signed [NUM_WIDTH-1:0] old_nb;

        begin
            new_max = (new_nb > old_nb);
        end
    endfunction


    reg  [NUM_WIDTH-1:0]    up_data_1p;
    reg  [NUM_WIDTH-1:0]    up_data_2p;
    reg  [NUM_WIDTH-1:0]    up_data_3p;

    reg                     up_valid_1p;
    reg                     up_valid_2p;
    reg                     up_valid_3p;

    reg                     restart_1p;
    reg                     restart_2p;





    always @(posedge clk) begin
        if (restart) begin
            restart_1p <= 1'b1;
        end
        else if (restart_1p & up_valid_1p) begin
            restart_1p <= 1'b0;
        end
    end


    always @(posedge clk) begin
        restart_2p  <= restart_1p;

        up_valid_1p <= up_valid;
        up_valid_2p <= up_valid_1p;
        up_valid_3p <= up_valid_2p;
    end


    always @(posedge clk) begin
        up_data_1p   <= 'b0;

        if (up_valid) begin
            up_data_1p   <= up_data;
        end
    end


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


    always @(posedge clk) begin
        if (up_valid_2p) begin
            if (restart_2p || new_max(up_data_2p, up_data_3p)) begin
                up_data_3p <= up_data_2p;
            end
        end
    end


    always @(posedge clk)
        if (up_valid_3p) begin
            dn_data <= up_data_3p;
        end



`ifdef FORMAL

    reg         past_exists;
    reg  [2:0]  past_wait;
    initial begin
        restrict property (past_exists == 1'b0);
        restrict property (past_wait   ==  'b0);
    end


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









    always @(posedge clk)
        if (past_exists && $past(restart_1p, 3) && $past(up_valid_1p, 3)) begin
            assert(dn_data == $past(up_data_1p, 3));
        end




    always @(posedge clk)
        if (past_exists && $fell(restart_1p)) begin
            assert($past(up_valid_1p));
        end








    always @(posedge clk)
        if (past_exists && $past(up_valid_3p)) begin
            assert($signed(dn_data) >= $signed($past(up_data_3p)));
        end




    always @(posedge clk)
        if (past_exists && ($signed(up_data_3p) < $signed($past(up_data_3p)))) begin
            assert($past(restart_2p & up_valid_2p));
        end


`endif
endmodule