/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

#include <camkes-single-threaded.h>
#include <camkes-BPMPServer.h>
#include <camkes-fdt-bind-driver.h>

component BPMP {
    hardware;
    dataport Buf(4096) tx_channel;
    dataport Buf(4096) rx_channel;
}

component BPMPServer {
    single_threaded_component()
    BPMPServer_server_interfaces(the_bpmp)

    /* hardware interfaces */
    emits Dummy dummy_source;
    consumes Dummy hsp;
    fdt_bind_drivers_interfaces(["/bpmp"]);
    dataport Buf(4096) bpmp_tx;
    dataport Buf(4096) bpmp_rx;

    composition {
        component BPMP bpmp;
        connection seL4DTBHardware hsp_conn(from dummy_source, to hsp);
        /* The BPMP shared memory regions aren't located in a particularly nice
         * location for the seL4DTBHardware connector */
        connection seL4HardwareMMIO bpmp_tx_mmio(from bpmp_tx, to bpmp.tx_channel);
        connection seL4HardwareMMIO bpmp_rx_mmio(from bpmp_rx, to bpmp.rx_channel);
        fdt_bind_driver_connections();
        BPMPServer_server_connections(the_bpmp)
    }

    configuration {
        hsp.dtb = dtb({ "path" : "/tegra-hsp@3c00000" });
        bpmp.tx_channel_paddr = 0x3004e000;
        bpmp.tx_channel_size = 0x1000;
        bpmp.rx_channel_paddr = 0x3004f000;
        bpmp.rx_channel_size = 0x1000;
        BPMPServer_server_configurations(the_bpmp)
    }
}