1/*
2 * Lexical conventions:
3 *
4 * identifiers -> ([a-z] | [A-Z]){[a-z] | [A-Z] | [0-9] | '_'}
5 * numbers -> decimal | hexadecimal
6 * arithmetic_op -> '+' | '-' | '*' | '[]' | '++'
7 * boolean_op -> '!' | '&&' | '||'
8 */
9
10module CortexA9_Core((0 to 0xFFFFE000) core_periphbase) { // Module parameters are natural numbers and have a range
11    /*
12     * Node domains: {memory, intr, power, clock} 
13     * Node types have arbitrary dimension, meaning is hardware dependent
14     * E.g. here: 1st dimension: address, 2nd dimension data word
15     */
16    output memory (0 bits 8; 0 bits 32) SCU
17    output memory (0 bits 8; 0 bits 32) Global_Timer 
18    output memory (0 bits 8; 0 bits 32) GIC_PROC        // 0 bits 8 == 0 to 2^8-1
19    output memory (0 bits 12; 0 bits 32/*;*/) GIC_DISTR     // Trailing ';' should be allowed but optional (Parser does not yet allow it)
20    output memory (0 bits 32; 0 bits 32) L2
21
22    /* 
23     * Node declaration and definition is separate
24     * Convention: keep together whenever possible
25     */
26    input intr (0 to 1023) CPU_INTR
27    CPU_INTR accepts [
28        (0, 2, 8 to 1023) // Specify sparse ranges
29    ]
30
31    memory (0 bits 8; 0 bits 32) Private_Timers
32    Private_Timers accepts [
33        (0 bits 8; *)
34    ]
35
36    memory (0 bits 13; 0 bits 32) PRIVATE_PERIPH
37    PRIVATE_PERIPH maps [
38        /* All dimensions of origin and target need to be specified */
39        (0x0000 to 0x00FC; 0 bits 32) to SCU at (0x0 to 0xFC; 0 bits 32);
40
41        /*
42         * Wildcards map whole range of dimension
43         * The following are equivalent
44         */
45        (0x0100 bits 8; *) to GIC_PROC at (*; *);
46        (0x0100 bits 8; 0 bits 32) to GIC_PROC at (0 bits 8; 0 bits 32);
47
48        /* Mapped ranges must have same size or target must be constant */
49        (0x0200 bits 8; *) to Global_Timer at (*; *); // OK, one-to-one mapping
50        (0x0200 bits 8; *) to Global_Timer at (*; 0); // OK, 2nd dimension collapsed to 0 
51        (0x0200 bits 9; *) to Global_Timer at (*; *); // Error
52
53        (0x0600 bits 8; *) to Private_Timers at (*; *);
54        (0x1000 bits 12; *) to GIC_DISTR at (*; *)/*;*/ // Trailing ';' should be allowed but optional (Parser does not yet allow it)
55    ]
56
57    memory (0 bits 32, 0 bits 32) CPU_PHYS
58    CPU_PHYS maps [
59        (core_periphbase bits 13; *) to PRIVATE_PERIPH at (*; *)
60    ]
61    CPU_PHYS overlays L2 // overlay node's type must be the same as node's type
62}
63
64module CortexA9_MPCore((1 to 4) num_cores, (0 to 0xFFFFE000) periphbase) {
65    input intr (32 to 1019) GIC
66    input intr (0 to 1023) CPU_INTR[0 to num_cores-1]
67    output memory (0 bits 32, 0 bits 32) L2
68
69    /*
70     * Module instances must be declared
71     */
72    instance Core[0 to num_cores-1] of CortexA9_Core
73    Core[0 to num_cores-1] instantiates CortexA9_Core(perhiphbase)
74
75    memory (0 bits 8; 0 bits 32) SCU
76    SCU accepts [(0x0 to 0xFC; *)]
77
78    memory (0 bits 8; 0 bits 32) Global_Timer 
79    Global_Timer accepts [(0 bits 8; *)]
80
81    memory (0 bits 8; 0 bits 32) GIC_PROC
82    GIC_PROC accepts [(0 bits 8; *)]
83
84    memory (0 bits 12; 0 bits 32) GIC_DISTR
85    GIC_DISTR accepts [(0 bits 12; *)]
86
87    forall c in (0 to num_cores-1) {
88        /*
89         * Instantiate module and bind output ports
90         * Format: <output_port> to <node>
91         * All output ports must be bound, types of port and node must match exactly
92         */
93        Core[c] binds [
94            SCU to Cluster_SCU;
95            Global_Timer to Global_Timer;
96            GIC_PROC to GIC_PROC;
97            GIC_DISTR to GIC_DISTR;
98            L2 to L2
99        ]
100
101        /*
102         * Reference input ports with dot notation
103         */
104        GIC maps [
105            (*) to Core[c].CPU_INTR at (0 to 1019-32)
106        ]
107
108        /*
109         * Input port pass-through, for the moment introduces proxy node
110         */
111        CPU_INTR[c] overlays Core[c].CPU_INTR
112    }
113}
114
115/*
116 * Named types
117 * Only possible at file scope
118 * If we have a use case, we might introduce module scope types
119 */
120type L2_Bus (0 bits 32; 0 bits 32)
121
122module OMAP44xx {
123    /* 
124     * Named constants
125     * Only possible at module scope, use parameters to pass to other modules
126     * Only natural number constants are possible.
127     * If we have a use case we might introduce tuple constants
128     */
129    const PERIPHBASE 0x48240000
130    const NUM_CORES 2
131
132    /* 
133     * Multidimensional arrays through tuple indices
134     */
135    instance MPU[1 to 2; 1 to 2] of CortexA9_MPCore
136    MPU[*; *] instantiates CortexA9_MPCore(NUM_CORES, PERIPHBASE)  // Use constants
137
138    MPU[*; *] binds [
139        L2 to L2
140    ]
141
142    intr (0 to 1023) INTR_CTRL
143    forall s in (1 to 2) {
144        INTR_CTRL maps [
145            /* Multicast interrupt vector 1 to all 1st cores of MPU[1; 1] and MPU[2; 1] */
146            (1) to MPU[s; 1].CPU_INTR[1] at (0);
147            /* Same for vector 2 to 2nd cores */
148            (2) to MPU[s; 1].CPU_INTR[2] at (0);
149            /* Same for vector 3 to 1st cores of MPI[1; 2] and MPU[2; 2] */
150            (3) to MPU[s; 2].CPU_INTR[1] at (0);
151            /* And for vector 4 to 2nd cores */
152            (4) to MPU[s; 2].CPU_INTR[2] at (0)/*;*/
153        ]
154    }
155
156    /*
157     * Node definitions can be split over several statements
158     */
159    INTR_CTRL maps [
160        (5) to MPU[1; 1].CPU_INTR[1] at (1)
161    ]
162
163    memory (0 bits 30, 0 bits 32) SDRAM
164    SDRAM accepts [
165        /*
166         * Specify 1st order logic formula for properties that has to be true for the block to match
167         */
168        (0x00000000 bits 28; *) read && !write;  // read-only
169        (0x10000000 bits 28; *) read && write;   // read-write
170        (0x20000000 bits 28; *) read;            // read, don't care about write
171        (0x30000000 bits 28; *)                 // don't care about properties
172    ]
173
174    memory (L2_Bus) L2 // Reference named type
175    L2 maps [
176        /*
177         * Specify 1st order logic formulas for incoming and outgoing properties
178         */
179        (0x80000000 bits 28; *) !write to SDRAM at (0 bits 28; *) read && !write;  // map all non writeable to 1st quarter of RAM as read-only
180        (0x80000000 bits 28; *) write to SDRAM at (0 bits 28; *) read && write;   // map all writeable to 2nd quarter of RAM as read-write
181        (0x90000000 bits 28; *) to SDRAM at (0x10000000 bits 28; *) read && write;
182        (0xA0000000 bits 28; *) to SDRAM at (0x20000000 bits 28; *) read, SDRAM at (0x30000000, 0); // Multicast
183        (0xB0000000 bits 28; *) to SDRAM at (0x30000000 bits 28; *)/*;*/
184    ]
185
186    /* 
187     * Converting from one namespace to another
188     * 
189     * Destination type is optional, if specified, all target ranges have to match
190     */
191    memory (0 bits 32, 0 bits 32) to intr (32 to 1019) CHIPSET
192    CHIPSET converts [
193        // (0; 0 to 1019-32) !read to MPU[1; 1].GIC at (*) edge_trig;
194        (0; 1) to MPU[1;1].CPU_INTR[1] at (0); // Error, type does not match
195        (0; 2) to MPU[1;1].CPU_INTR[1] at (1)/*;*/ // Error, type does not match
196    ]
197
198    intr (0 to 1023) to memory MSI_CTRL
199    MSI_CTRL converts [
200        /* ... */
201    ]
202
203    /*
204     * Changing the dimensionality through a mapping
205     */
206    memory (0 bits 7; 0 to 1) RAM_2D
207    RAM_2D accepts [(*; *)]
208
209    memory (0 bits 3; 0 bits 3; 0 bits 2) BUS_3D
210    forall a in (0 bits 3) {
211        forall b in (0 bits 3) {
212            forall c in (0 bits 2) {
213                BUS_3D maps [
214                    /* Split address parts with slice operator: */
215                    (0; 0; c) to RAM_2D at (c[1]; c[0]);
216
217                    /* Concatenate address parts with concat/slice operator :*/
218                    (a; b; 0) to RAM_2D at (a ++ b[0 to 2]; 0);
219                    (a; b; 1) to RAM_2D at (a ++ b[0 to 2]; 1);
220
221                    /*
222                     * ++[] is left associative
223                     * The following are equal:
224                     */
225                    (a; b; c) to RAM_2D at ( a ++ b[0 to 2]  ++ c[1]; c[0]);
226                    (a; b; c) to RAM_2D at ((a ++ b[0 to 2]) ++ c[1]; c[0])/*;*/
227                ]
228            }
229        }
230    }
231}
232