1#
2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3#
4# SPDX-License-Identifier: GPL-2.0-only
5#
6
7---
8$schema: http://json-schema.org/draft-07/schema#
9description: Schema for seL4 hardware.yml
10type: object
11additionalProperties: false
12properties:
13  devices:
14    type: array
15    uniqueItems: true
16    description: top-level list of devices
17    items:
18      $ref: '#/definitions/device'
19required: [devices]
20definitions:
21  device:
22    type: object
23    additionalProperties: false
24    properties:
25      compatible:
26        description: List of compatible strings to which this rule applies
27        type: array
28        minItems: 1
29        uniqueItems: true
30      regions:
31        description: Memory regions this device has that the kernel might use
32        type: array
33        items:
34          $ref: '#/definitions/region'
35        uniqueItems: true
36      interrupts:
37        description: Interrupts this device has that the kernel might use.
38        type: object
39        additionalProperties: false
40        patternProperties:
41          '^[A-Za-z_][A-Za-z0-9_]*$':
42            $ref: '#/definitions/interrupt'
43    required: [compatible]
44  region:
45    type: object
46    additionalProperties: false
47    properties:
48      index:
49        description: Region index this property should apply to
50        type: integer
51        minimum: 0
52      kernel:
53        description: kernel macro used to access this region. If not present, region will not be mapped.
54        $ref: '#/definitions/macro'
55      kernel_size:
56        description: >
57          Maximum size of the region in the kernel.
58          This will map PAGE_ALIGN_UP(max(kernel_size, region_size)) bytes starting at the
59          device's base address into the kernel.
60        type: integer
61        default: 1 << PAGE_BITS
62      macro:
63        description: only map the region to the kernel if this macro is defined
64        $ref: '#/definitions/macro'
65      user:
66        description: >
67          Whether or not to make a device untyped for userspace for this region.
68          If true, will always expose this region to userspace.
69          If false, region will only be exposed if kernel is not using it.
70        default: false
71        type: boolean
72    required: [index, kernel]
73  interrupt:
74    oneOf:
75      - type: object
76        additionalProperties: false
77        properties:
78          # TODO: remove enable_macro altogether. We don't use it.
79          enable_macro:
80            description: only set interrupt if this macro is defined - this rule will be ignored if the given macro is false.
81            $ref: '#/definitions/macro'
82          index:
83            description: index of interrupt in device's interrupts array
84            $ref: '#/definitions/interrupt_index'
85          sel_macro:
86            description: >
87              if macro is defined, use 'index' as IRQ, otherwise use undef_index.
88              For example if a device had interrupts = [1, 2, 3]
89              and a rule like
90                MY_INTERRUPT:
91                  index: 0
92                  sel_macro: MY_MACRO
93                  undef_index: 2
94              then the C header output would look like
95              #ifdef MY_MACRO
96              #define MY_INTERRUPT 1 /* interrupt 0 of device */
97              #else
98              #define MY_INTERRUPT 3 /* interrupt 2 of device */
99              #endif /* MY_MACRO */
100            $ref: '#/definitions/macro'
101          undef_index:
102            description: index of interrupt in device's array to use when sel_macro is undefined
103            $ref: '#/definitions/interrupt_index'
104          priority:
105            description: if multiple conflicting IRQs are present, the IRQ with the  highest priority will be selected.
106            default: 0
107            type: integer
108        required: [index]
109        dependencies:
110          sel_macro: [undef_index]
111          undef_index: [sel_macro]
112      - $ref: '#/definitions/interrupt_index'
113  interrupt_index:
114    oneOf:
115      - type: integer
116        description: index of interrupt in device's interrupts array
117        minimum: 0
118      - $ref: '#/definitions/boot-cpu'
119  macro:
120    type: string
121    pattern: '^!?[A-Za-z_][A-Za-z0-9_]*$'
122    minLength: 1
123  boot-cpu:
124    type: string  # TODO: why does 'const' not work here?
125    description: >
126      Use interrupt associated with the seL4,boot-cpu set in the chosen node.
127      For instance, a chosen node like
128
129      chosen {
130        seL4,boot-cpu = <&cpu2>;
131      }
132
133      and a device like
134
135      device {
136        interrupts = <0x1 0x2 0x3 0x4>;
137        interrupt-affinity = <&cpu0 &cpu1 &cpu2 &cpu3>;
138      }
139
140      would use interrupt 0x3 if the boot-cpu option was used as the index.
141    pattern: '^boot-cpu$'
142
143