verilog/rtl/vdp_lite_user_proj/vdp_sprite_raster_collision.v

// vdp_sprite_raster_collision.v
//
// Copyright (C) 2020 Dan Rodrigues <danrr.gh.oss@gmail.com>
//
// SPDX-License-Identifier: Apache-2.0

`default_nettype none

module vdp_sprite_raster_collision #(
`ifdef FORMAL
    // This FORMAL condition can applied in a wrapper testbench instead of doing it here
    // the assertions below can then be lifted out of this source since they just assert on outputs anyway
    parameter SPRITES_TOTAL = 16
`else
    parameter SPRITES_TOTAL = 255
`endif
) (
    input clk,
    input restart,

    input [8:0] render_y,

    // sprite attribute data
    input [8:0] sprite_y,
    input [4:0] sprite_height,
    input width_select_in,
    input flip_y,

    // sprite to read attributes for
    output reg [7:0] sprite_test_id,

    // hit list outputs
    output reg [7:0] hit_list_index,

    output reg [7:0] sprite_id,
    output reg [3:0] sprite_y_intersect,
    output reg width_select_out,

    output reg hit_list_write_en,

    output reg finished
);
    localparam READ_LATENCY = 3;

    // changes per line
    reg [8:0] render_y_r;

    // changes per sprite
    reg [8:0] sprite_y_r;
    reg [4:0] sprite_height_r;

    wire ready;

    delay_ffr #(.DELAY(3)) ready_dm (
        .clk(clk),
        .reset(restart),
        .in(1'b1),
        .out(ready)
    );

    wire output_valid;

    delay_ffr #(.DELAY(1)) output_valid_dm (
        .clk(clk),
        .reset(restart),
        .in(ready),
        .out(output_valid)
    );

    wire flip_y_d, width_select_d;

    delay_ffr #(.DELAY(2), .WIDTH(2)) attributes_dm (
        .clk(clk),
        .reset(restart),
        .in({flip_y, width_select_in}),
        .out({flip_y_d, width_select_d})
    );

    wire [4:0] sprite_height_d;

    delay_ffr #(.DELAY(2), .WIDTH(5)) sprite_height_dm (
        .clk(clk),
        .reset(restart),
        .in(sprite_height),
        .out(sprite_height_d)
    );

    reg finished_t;

    reg [8:0] sprite_y_intersect_t;
    reg has_collision, has_collision_t;

    wire [8:0] sprite_y_intersect_nx = render_y_r - sprite_y_r;
    wire has_collision_nx = sprite_y_intersect_nx < sprite_height_r;
    wire hit_list_needs_increment = ready && (has_collision_t || will_finish);

    wire finished_nx = finished_t || all_sprites_processed;
    wire will_finish = !finished_t && finished_nx;

    wire all_sprites_processed = (sprite_id == (SPRITES_TOTAL - READ_LATENCY + 1)) && output_valid;
    wire hit_list_full = 0; // hit_list_index == 9'h100;

    wire collision_needs_writing = (ready && has_collision_t && !finished_t);
    wire hit_list_terminator_needs_writing = (!hit_list_full && finished_t);
    wire hit_list_write_en_nx = collision_needs_writing || hit_list_terminator_needs_writing;

    always @(posedge clk) begin
        if (restart) begin
            finished <= 0;
            finished_t <= 0;
            hit_list_write_en <= 0;

            // probably not needed, account for any latency and remove
            // this is already registered in parent vdp module
            render_y_r <= render_y;
            
            // -1 for preincrement index
            hit_list_index <= -1;

            sprite_test_id <= 0;
            sprite_id <= -(READ_LATENCY) - 1;
        end else if (!finished) begin
            hit_list_index <= hit_list_needs_increment ? hit_list_index + 1 : hit_list_index;
            sprite_test_id <= sprite_test_id + 1;
            sprite_id <= sprite_id + 1;

            hit_list_write_en <= hit_list_write_en_nx;

            finished_t <= finished_nx;
            finished <= finished_t;
        end else begin
            hit_list_write_en <= 0;
        end
    end

    always @(posedge clk) begin
        if (restart) begin
            has_collision_t <= 0;
            has_collision <= 0;
            width_select_out <= 0;
            sprite_y_intersect <= 0;
            sprite_y_r <= 0;
            sprite_y_intersect_t <= 0;
            sprite_height_r <= 0;
        end else begin
            // register inputs from y_block
            sprite_y_r <= sprite_y;
            sprite_height_r <= sprite_height;

            // register comparator result from previously read y_block
            sprite_y_intersect_t <= sprite_y_intersect_nx;
            has_collision_t <= has_collision_nx;

            // move the above registered result to the output for this module
            sprite_y_intersect <= flip_y_d ? sprite_height_d - sprite_y_intersect_t - 1 : sprite_y_intersect_t;
            has_collision <= has_collision_t;
            width_select_out <= width_select_d;
        end
    end

`ifdef FORMAL

    reg past_valid = 0;
    integer valid_count = 0;

    initial begin
        restrict(restart);
    end

    always @(posedge clk) begin
        if (past_valid) begin
            assume(!restart);
        end
    end

    always @(posedge clk) begin
        if (past_valid) begin
            if ($past(restart)) begin
                assert(!output_valid);
            end
        end

        past_valid <= 1;

        if (!restart) begin
            valid_count <= valid_count + 1;
        end else begin
            valid_count <= 0;
        end
    end

    // expectations when evaluation just started

    always @(posedge clk) begin
        if (past_valid) begin
            if ($fell(restart)) begin
                assert(sprite_test_id == 8'h00);
                assert(!finished);
                assert(!output_valid);
                assert(!hit_list_write_en);
            end
        end
    end

    // expectations when evaluation just finished
    
    always @(posedge clk) begin
        if (past_valid) begin
            if ($rose(finished)) begin
                assert(output_valid);
                assert(hit_list_write_en);
            end
        end
    end

    always @(posedge clk) begin
        if (past_valid) begin
            if ($rose(output_valid) && has_collision) begin
                if (has_collision) begin
                    // it's PRE increment pointer so it's only 00 on the first collision
                    assert(hit_list_index == 8'h00);
                    assert(hit_list_write_en);
                end else begin
                    // and it should be ff (or -1) if there was no collision initially
                    assert(hit_list_index == 8'hff);
                    assert(!hit_list_write_en);
                end 
            end
        end
    end

    // temporary variables for use with the below assertions

    integer sprite_pos, raster_pos;
    integer sprite_top;
    integer flipped_y_intersect;

    localparam PIPE_DELAY = 3;

    // the pipeline adds latency of PIPE_DELAY cycles so these are added for convenience

    reg [8:0] input_sprite_y;
    reg [8:0] input_render_y;
    reg [7:0] input_sprite_height;
    reg input_flip_y;
    reg input_width_select_in;

    always @(posedge clk) begin
        input_sprite_y = $past(sprite_y, PIPE_DELAY - 1);
        input_render_y = $past(render_y, PIPE_DELAY - 1);
        input_sprite_height = $past(sprite_height, PIPE_DELAY - 1);
        input_flip_y = $past(flip_y, PIPE_DELAY - 1);
        input_width_select_in = $past(width_select_in, PIPE_DELAY - 1);
    end

    always @(posedge clk) begin
        if (valid_count > (PIPE_DELAY + 1)) begin
            sprite_top = input_sprite_y;
            sprite_pos = input_sprite_y + input_sprite_height;
            raster_pos = input_render_y;
            flipped_y_intersect = (sprite_y_intersect ^ {4{input_flip_y}}) % input_sprite_height;

            // a) cases where there IS collision
            if (!finished && output_valid && has_collision) begin
                // intersect should in be in range (0..<sprite_height)
                assert(flipped_y_intersect < input_sprite_height);

                // raster >= sprite.top
                // assert($past(render_y, PIPE_DELAY) >= $past(sprite_y, PIPE_DELAY));

                // sprite.bottom > raster
                assert(sprite_pos > raster_pos);

                assert(width_select_out == input_width_select_in);

                assert(hit_list_write_en);
            end

            // b) cases where there is NO collision:
            if (!finished && output_valid && !has_collision) begin
                assert(raster_pos < sprite_top
                    || raster_pos >= sprite_pos);

                assert(!hit_list_write_en);
            end
        end

        // render_y is not supposed to change in the middle of a sprite list evaluation
        if (!restart) begin
            assume($stable(render_y));
        end
    end

`endif

endmodule