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

`default_nettype none

module vdp_vga_timing #(
    parameter H_ACTIVE_WIDTH = 848,
    parameter V_ACTIVE_HEIGHT = 480,

    parameter H_FRONTPORCH = 16,
    parameter H_SYNC = 112,
    parameter H_BACKPORCH = 112,

    parameter V_FRONTPORCH = 6,
    parameter V_SYNC = 8,
    parameter V_BACKPORCH = 23
) (
    input clk,
	input reset,
    input hold_raster,

    output reg [10:0] raster_x = 0,
    output reg [9:0] raster_y = 0,

    output reg line_ended,
    output reg frame_ended,

    output reg active_line_started,
    output reg active_frame_ended,

    output reg hsync,
    output reg vsync,
    output reg active_display
);
    localparam STATE_FP = 0;
    localparam STATE_SYNC = 1;
    localparam STATE_BP = 2;
    localparam STATE_ACTIVE = 3;

    localparam H_SIZE = H_ACTIVE_WIDTH + H_FRONTPORCH + H_SYNC + H_BACKPORCH;
    localparam V_SIZE = V_ACTIVE_HEIGHT + V_FRONTPORCH + V_SYNC + V_BACKPORCH;

    localparam H_OFFSCREEN_WIDTH = H_SIZE - H_ACTIVE_WIDTH;
    localparam V_OFFSCREEN_HEIGHT = V_SIZE - V_ACTIVE_HEIGHT;

    wire line_ended_nx = x_fsm_nx == STATE_FP && x_fsm == STATE_ACTIVE;
    wire frame_ended_nx = y_fsm_nx == STATE_ACTIVE && y_fsm == STATE_BP && line_ended_nx;
    wire active_frame_ended_nx = line_ended_nx && y_fsm == STATE_ACTIVE && y_fsm_nx == STATE_FP;

    wire hsync_b_nx = x_fsm == STATE_SYNC;
    wire vsync_b_nx = y_fsm == STATE_SYNC;

    wire active_display_nx = y_fsm == STATE_ACTIVE && x_fsm_nx == STATE_ACTIVE;

    wire active_line_started_nx = x_fsm == STATE_FP && x_fsm_nx == STATE_ACTIVE;

    reg [1:0] x_fsm_nx;

    always @* begin
        x_fsm_nx = (raster_x == x_next_count ? x_fsm + 1 : x_fsm);
    end

    reg [1:0] y_fsm_nx;

    always @* begin
        y_fsm_nx = y_fsm;

        if (line_ended_nx) begin
            y_fsm_nx = (raster_y == y_next_count ? y_fsm + 1 : y_fsm);
        end
    end

    reg [1:0] x_fsm = 0;
    reg [1:0] y_fsm = STATE_ACTIVE;

    always @(posedge clk) begin
		if (reset) begin
			x_fsm <= 0;
			y_fsm <= STATE_ACTIVE;
		end else if (!hold_raster) begin
            x_fsm <= x_fsm_nx;
            y_fsm <= y_fsm_nx;
        end
    end

    reg [10:0] x_next_count, y_next_count;

    // target counts to advance state

    always @* begin
        (* full_case, parallel_case *)
        case (x_fsm)
            STATE_FP: x_next_count = H_FRONTPORCH - 1;
            STATE_SYNC: x_next_count = H_FRONTPORCH + H_SYNC - 1;
            STATE_BP: x_next_count = H_SYNC + H_FRONTPORCH + H_BACKPORCH - 1;
            STATE_ACTIVE: x_next_count = H_SIZE - 1;
        endcase
    end

    always @* begin
        (* full_case, parallel_case *)
        case (y_fsm)
            STATE_FP: y_next_count = V_ACTIVE_HEIGHT + V_FRONTPORCH - 1;
            STATE_SYNC: y_next_count = V_ACTIVE_HEIGHT + V_FRONTPORCH + V_SYNC - 1;
            STATE_BP: y_next_count = V_SIZE - 1;
            STATE_ACTIVE: y_next_count = V_ACTIVE_HEIGHT - 1;
        endcase
    end

    reg [10:0] raster_x_nx;
    reg [9:0] raster_y_nx;

    always @* begin
        raster_x_nx = raster_x + 1;
        raster_y_nx = raster_y;

        if (line_ended_nx) begin
            raster_x_nx = 0;
            raster_y_nx = raster_y + 1;

            if (frame_ended_nx) begin
                raster_y_nx = 0;
            end
        end
    end

    always @(posedge clk) begin
		if (reset) begin
			raster_x <= 0;
			raster_y <= 0;
		end else if (!hold_raster) begin
            raster_x <= raster_x_nx;
            raster_y <= raster_y_nx;
		end
    end

    always @(posedge clk) begin
        if (reset) begin
            hsync <= 1;
            vsync <= 1;
            active_display <= 0;
            line_ended <= 0;
            frame_ended <= 0;
            active_line_started <= 0;
            active_frame_ended <= 0;
        end else if (!hold_raster) begin
            hsync <= !hsync_b_nx;
            vsync <= !vsync_b_nx;
            active_display <= active_display_nx;
            line_ended <= line_ended_nx;
            frame_ended <= frame_ended_nx;
            active_line_started <= active_line_started_nx;
            active_frame_ended <= active_frame_ended_nx;
        end
    end

`ifdef FORMAL

    reg past_valid = 0;
    reg [1:0] past_counter = 0;

    initial begin
        restrict(reset);
    end

    always @(posedge clk) begin
        if (past_counter < 3) begin
            past_counter <= past_counter + 1;
        end else begin
            past_valid <= 1;
        end

        if (past_counter != 0) begin
            assume(!reset);
        end
    end

    always @(posedge clk) begin
        if (!$past(reset) && past_counter > 2) begin
            assert(active_display == (raster_x > H_OFFSCREEN_WIDTH && raster_y < (V_SIZE - V_OFFSCREEN_HEIGHT)));

            assert(!hsync == ((raster_x >= H_FRONTPORCH) && (raster_x < H_FRONTPORCH + H_SYNC)));
            assert(!vsync == ((raster_y >= V_ACTIVE_HEIGHT + V_FRONTPORCH) && (raster_y < V_ACTIVE_HEIGHT + V_FRONTPORCH + V_SYNC)));

            assert(line_ended_nx == (raster_x == (H_SIZE - 1)));
            assert(line_ended == (raster_x == 0));

            assert(frame_ended_nx == (raster_y == (V_SIZE - 1)));
            assert(active_frame_ended_nx == (raster_y == V_ACTIVE_HEIGHT - 1 && line_ended_nx));
        end
    end

`endif

endmodule