//
// Enum for coordinate axis
//
enum XY = X, Y

// Big syntax
enum RGB is
    R
    G
    B
end enum

//
// Resolution structure
//
struct Resolution with (Coord : type(default int(15, 0))) is

    var active_area : Coord[for enum XY]
    var front_porch : Coord[for enum XY]
    var back_porch  : Coord[for enum XY]
    var sync        : Coord[for enum XY]
    var total       : Coord[for enum XY]

    var req_clock_mhz  : ClockFrequency

    function sync_start(xy : XY) : Coord = @active_area[xy] + @front_porch[xy]
    function sync_end(xy : XY) : Coord   = @sync_start(xy) + @sync[xy] - 1
    function in_sync(xy : XY, pos : Coord) = @sync_start(xy, pos) <= pos <= @sync_end(xy, pos)
    function calc_total(xy : XY) : Coord = @active_area[xy] + @front_porch[xy] + @back_porch[xy] + @sync_pulse[xy]
    function in_screen(x,y) : bool = x < @active_area.X && y < @active_area.Y

    assertion CoordValid  is
        // internally assert_no_overflow rewrites expression
        // into the series of intermediate steps that store result in bigger int (i.e. a+b+c => i1 = a + b; i2 = i1+c)
        // then it checks that no overflow occur
        assert_no_overflow("Coord is large enough for X", @calc_total(X))
        assert_no_overflow("Coord is large enough for Y", @calc_total(Y))
    end assertion

    assertion totalsValid is
        assert("total dots per horizontal line", @calcTotal(X) == @total.X)
        assert("total lines per frame", @calcTotal(Y) == total.Y)
    end assertion

    assertion syncsOrdered is
        assert("X", @sync_end(X) > @sync_start(X))
        assert("Y", @sync_end(Y) > @sync_start(Y))
    end assertion

    assertion clockNonZero = @req_clock_mhz > 0

    assertion clockMatch(c : clock) is
        assert("clock match", c.frequency == @clock)
    end assertion
end struct


const VGA_800_600_60 : Resolution is
    active_area = {800, 600}
    front_porch = {40,  1}
    back_porch  = {88, 23}
    sync        = {128, 4}
    total       = {1056, 628}

    ensure assertion (ALL) // prove all assertions that don't take arguments(these will be proved later)
end


module vgaImpl
with
    res : Resolution
    bitsPerChannel : integer[for enum RGB]
signals
    clk <: clock // explicitly declare clock
    red :> int(bitsPerChannel.R)
    green : output(int(bitsPerChannel.G)) // different syntax for output
    blue  :> int(bitsPerChannel.B)
    hsync, vsync :> bool
    x, y :> Optional(bool, isOutputPos))
is
    // ensure last assertion
    // if there are assertions that take argument, that module which uses them,
    // must do at least one call to instantiate the proof.
    ensure res.clockMatch(clk)

    // registers for current coordinate
    var px : res.Coord(default 0) // set value on both (implicit) reset signal and in initial block
    var py : res.Coord(default 0)

    // specifications
    assertion h_sync_valid_active = assert(0 <= x < res.active_area.X  ==> hsync == false)
    assertion h_sync_valid_front = assert(res.active_area.X <= x < res.active_area + res.front_porch.X  ==> hsync == false)
    assertion h_sync_valid_sync = assert(res.in_sync(x, px) ==> hsync == true)
    assertion h_sync_valid_back = assert(res.active_area.X + res.front_porch.X + res.sync.X <= x < res.total.X ==> hsync == false)

    assertion v_sync_valid_active = assert(0 <= y < res.active_area.Y  ==> vsync == false)
    assertion v_sync_valid_front = assert(res.active_area.Y <= y < res.active_area + res.front_porch.Y  ==> vsync == false)
    assertion v_sync_valid_sync = assert(res.in_sync(y, py) ==> vsync == true)
    assertion v_sync_valid_back = assert(res.active_area.Y + res.front_porch.Y + res.sync.Y <= y < res.total.Y ==> vsync == false)

    assertion color_invisible_out_of_screen is
        assert(!res.in_screen(px, py) ==> red == 0)
        assert(!res.in_screen(px, py) ==> green == 0)
        assert(!res.in_screen(px, py) ==> blue == 0)
    end assertion

    assertion coords_valid is
        assert(px < res.total.X)
        assert(py < res.total.Y)
    end assertion

    // Driver for coordinate
    task Pixel is
        if px + 1 == res.total.X {
            px = 0
            if (py + 1 != res.total.Y)
                py = py + 1
            else
                py = 0
        } else {
            px = px + 1
        }
    end task

    // Syncs driver
    task Sync is
        hsync = res.in_sync(X, px)
        vsync = res.in_sync(Y, py)
    end task


    // Color driver
    task Color is
        if ! res.in_screen(px, py) {
            red = 0
            green = 0
            blue = 0
        } else {
            const x_even = px(3)
            const y_even = py(3)
            const output = x_even == y_even

            red = output ? red.max_unsigned_value() : 0
            green = output ? green.max_unsigned_value() : 0
            blue = output ? blue.max_unsigned_value() : 0
        }
    end task
end