| /* |
| * 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) |
| } |
| } |