data/full_repos/permissive/153960117/hdl/rescale.v
 line:53: before: "("
data/verilator_xmls/b8204d3d-b592-41c2-95b3-c3223fca84fb.xml
module rescale
  #(parameter
    NUM_WIDTH   = 33,
    NUM_AWIDTH  = $clog2(NUM_WIDTH),

    IMG_WIDTH   = 16)
   (input  wire                 clk,

    input  wire [7:0]           shift,

    input  wire [NUM_WIDTH-1:0] up_data,
    output reg  [IMG_WIDTH-1:0] dn_data
);





    localparam signed [IMG_WIDTH-1:0] IMG_MAX = ({1'b0, {IMG_WIDTH-1{1'b1}}});
    localparam signed [IMG_WIDTH-1:0] IMG_MIN = ({1'b1, {IMG_WIDTH-1{1'b0}}});

    localparam NUM_WIDTH_MAX = NUM_WIDTH;


    function grater_than_max (
            input [NUM_WIDTH-1:0]   number,
            input [NUM_AWIDTH-1:0]  overflow
        );
        reg   [NUM_AWIDTH-1:0]  ii;

        begin
            grater_than_max = 1'b0;
            for (ii = 0; ii < NUM_WIDTH[NUM_AWIDTH-1:0]; ii=ii+1) begin
                if (number[ii] & (ii >= overflow)) begin
                    grater_than_max = ~number[NUM_WIDTH-1];
                end
            end
        end
    endfunction


    function less_than_min (
            input [NUM_WIDTH-1:0]   number,
            input [NUM_AWIDTH-1:0]  overflow
        );

        reg   [NUM_AWIDTH-1:0]  ii;

        begin
            less_than_min = 1'b0;
            for (ii = 0; ii < NUM_WIDTH[NUM_AWIDTH-1:0]; ii=ii+1) begin
                if ( ~number[ii] & (ii >= overflow)) begin
                    less_than_min = number[NUM_WIDTH-1];
                end
            end
        end
    endfunction




    reg  [NUM_WIDTH-1:0]    up_data_1p;
    reg  [NUM_AWIDTH-1:0]   overflow_1p;

    reg  [NUM_WIDTH-1:0]    rescale_data_1p;
    reg  [IMG_WIDTH-1:0]    rescale_data_2p;
    reg  [IMG_WIDTH-1:0]    rescale_data_3p;

    reg                     bound_max_2p;
    reg                     bound_min_2p;





    always @(posedge clk) begin
        up_data_1p <= up_data;



        overflow_1p <= (IMG_WIDTH[NUM_AWIDTH-1:0] - 'b1) + shift[NUM_AWIDTH-1:0];
    end



    always @(posedge clk)
        bound_max_2p <= grater_than_max(up_data_1p, overflow_1p);



    always @(posedge clk)
        bound_min_2p <= less_than_min(up_data_1p, overflow_1p);


    always @(posedge clk) begin

        rescale_data_1p <= up_data >> shift;
        rescale_data_2p <= rescale_data_1p[0 +: IMG_WIDTH];
    end


    always @(posedge clk)
        if      (bound_min_2p)  rescale_data_3p <= IMG_MIN;
        else if (bound_max_2p)  rescale_data_3p <= IMG_MAX;
        else                    rescale_data_3p <= rescale_data_2p;


    always @(posedge clk)
        dn_data <= rescale_data_3p;



`ifdef FORMAL

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

    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 @(*) begin
        `ASSUME(shift <= (NUM_WIDTH-IMG_WIDTH));
    end



    function signed [NUM_WIDTH-1:0] shift_with_sign (
            input [NUM_WIDTH-1:0]   number,
            input [NUM_AWIDTH-1:0]  shift_right
        );
        reg   [7:0]  ii;

        begin

            for (ii = 0; ii < NUM_WIDTH; ii=ii+1) begin
                if (ii < shift_right) begin
                    number = {number[NUM_WIDTH-1], number[NUM_WIDTH-1:1]};
                end
            end

            shift_with_sign = number;
        end
    endfunction



    always @(posedge clk)
        if (past_exists) begin

            if (shift_with_sign($past(up_data, 4), $past(shift, 4)) < $signed(IMG_MIN)) begin
                assert(dn_data == IMG_MIN);
            end

            if (shift_with_sign($past(up_data, 4), $past(shift, 4)) > $signed(IMG_MAX)) begin
                assert(dn_data == IMG_MAX);
            end
        end



    always @(posedge clk)
        if (past_exists
            && (shift_with_sign($past(up_data, 4), $past(shift, 4)) > $signed(IMG_MIN))
            && (shift_with_sign($past(up_data, 4), $past(shift, 4)) < $signed(IMG_MAX))
            ) begin

            assert(dn_data == $past(up_data[shift +: IMG_WIDTH], 4));
        end



    always @(posedge clk)
        if (past_exists) begin
            assert(dn_data[IMG_WIDTH-1] == $past(up_data[NUM_WIDTH-1], 4));
        end





    always @(posedge clk)
        if (past_exists) begin
            assert($signed(IMG_MIN) <= $signed(dn_data) <= $signed(IMG_MAX));
        end


`endif
endmodule
module rescale
  #(parameter
    NUM_WIDTH   = 33,
    NUM_AWIDTH  = $clog2(NUM_WIDTH),

    IMG_WIDTH   = 16)
   (input  wire                 clk,

    input  wire [7:0]           shift,

    input  wire [NUM_WIDTH-1:0] up_data,
    output reg  [IMG_WIDTH-1:0] dn_data
);






    localparam signed [IMG_WIDTH-1:0] IMG_MAX = ({1'b0, {IMG_WIDTH-1{1'b1}}});
    localparam signed [IMG_WIDTH-1:0] IMG_MIN = ({1'b1, {IMG_WIDTH-1{1'b0}}});

    localparam NUM_WIDTH_MAX = NUM_WIDTH;


    function grater_than_max (
            input [NUM_WIDTH-1:0]   number,
            input [NUM_AWIDTH-1:0]  overflow
        );
        reg   [NUM_AWIDTH-1:0]  ii;

        begin
            grater_than_max = 1'b0;
            for (ii = 0; ii < NUM_WIDTH[NUM_AWIDTH-1:0]; ii=ii+1) begin
                if (number[ii] & (ii >= overflow)) begin
                    grater_than_max = ~number[NUM_WIDTH-1];
                end
            end
        end
    endfunction


    function less_than_min (
            input [NUM_WIDTH-1:0]   number,
            input [NUM_AWIDTH-1:0]  overflow
        );

        reg   [NUM_AWIDTH-1:0]  ii;

        begin
            less_than_min = 1'b0;
            for (ii = 0; ii < NUM_WIDTH[NUM_AWIDTH-1:0]; ii=ii+1) begin
                if ( ~number[ii] & (ii >= overflow)) begin
                    less_than_min = number[NUM_WIDTH-1];
                end
            end
        end
    endfunction




    reg  [NUM_WIDTH-1:0]    up_data_1p;
    reg  [NUM_AWIDTH-1:0]   overflow_1p;

    reg  [NUM_WIDTH-1:0]    rescale_data_1p;
    reg  [IMG_WIDTH-1:0]    rescale_data_2p;
    reg  [IMG_WIDTH-1:0]    rescale_data_3p;

    reg                     bound_max_2p;
    reg                     bound_min_2p;





    always @(posedge clk) begin
        up_data_1p <= up_data;



        overflow_1p <= (IMG_WIDTH[NUM_AWIDTH-1:0] - 'b1) + shift[NUM_AWIDTH-1:0];
    end



    always @(posedge clk)
        bound_max_2p <= grater_than_max(up_data_1p, overflow_1p);



    always @(posedge clk)
        bound_min_2p <= less_than_min(up_data_1p, overflow_1p);


    always @(posedge clk) begin

        rescale_data_1p <= up_data >> shift;
        rescale_data_2p <= rescale_data_1p[0 +: IMG_WIDTH];
    end


    always @(posedge clk)
        if      (bound_min_2p)  rescale_data_3p <= IMG_MIN;
        else if (bound_max_2p)  rescale_data_3p <= IMG_MAX;
        else                    rescale_data_3p <= rescale_data_2p;


    always @(posedge clk)
        dn_data <= rescale_data_3p;



`ifdef FORMAL

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

    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 @(*) begin
        `ASSUME(shift <= (NUM_WIDTH-IMG_WIDTH));
    end



    function signed [NUM_WIDTH-1:0] shift_with_sign (
            input [NUM_WIDTH-1:0]   number,
            input [NUM_AWIDTH-1:0]  shift_right
        );
        reg   [7:0]  ii;

        begin

            for (ii = 0; ii < NUM_WIDTH; ii=ii+1) begin
                if (ii < shift_right) begin
                    number = {number[NUM_WIDTH-1], number[NUM_WIDTH-1:1]};
                end
            end

            shift_with_sign = number;
        end
    endfunction



    always @(posedge clk)
        if (past_exists) begin

            if (shift_with_sign($past(up_data, 4), $past(shift, 4)) < $signed(IMG_MIN)) begin
                assert(dn_data == IMG_MIN);
            end

            if (shift_with_sign($past(up_data, 4), $past(shift, 4)) > $signed(IMG_MAX)) begin
                assert(dn_data == IMG_MAX);
            end
        end



    always @(posedge clk)
        if (past_exists
            && (shift_with_sign($past(up_data, 4), $past(shift, 4)) > $signed(IMG_MIN))
            && (shift_with_sign($past(up_data, 4), $past(shift, 4)) < $signed(IMG_MAX))
            ) begin

            assert(dn_data == $past(up_data[shift +: IMG_WIDTH], 4));
        end



    always @(posedge clk)
        if (past_exists) begin
            assert(dn_data[IMG_WIDTH-1] == $past(up_data[NUM_WIDTH-1], 4));
        end





    always @(posedge clk)
        if (past_exists) begin
            assert($signed(IMG_MIN) <= $signed(dn_data) <= $signed(IMG_MAX));
        end


`endif
endmodule