MMU description » History » Version 112
Andrei Tatarnikov, 01/29/2015 12:37 PM
1 | 24 | Alexander Kamkin | h1. MMU Description |
---|---|---|---|
2 | 1 | Taya Sergeeva | |
3 | 66 | Alexander Kamkin | _~By Alexander Kamkin and Taya Sergeeva~_ |
4 | 62 | Alexander Kamkin | |
5 | 63 | Alexander Kamkin | {{toc}} |
6 | |||
7 | 35 | Alexander Kamkin | A _memory management unit_ (_MMU_) is known to be one of the most complex and error-prone components of a modern microprocessor. MicroTESK has a special subsystem, called _MMU subsystem_, intended for (1) specifying memory devices and (2) deriving testing knowledge from such specifications. The subsystem provides unified facilities for describing memory buffers (like _L1_ and _L2 caches_, _translation look-aside buffers_ (_TLBs_), etc.) as well as a means for connecting several buffers into a memory hierarchy. |
8 | 1 | Taya Sergeeva | |
9 | 72 | Alexander Kamkin | h2. Grammar |
10 | 66 | Alexander Kamkin | |
11 | <pre> |
||
12 | 102 | Andrei Tatarnikov | startRule |
13 | : declaration* EOF! |
||
14 | 66 | Alexander Kamkin | ; |
15 | 1 | Taya Sergeeva | |
16 | 102 | Andrei Tatarnikov | declaration |
17 | 66 | Alexander Kamkin | : address |
18 | 102 | Andrei Tatarnikov | | segment |
19 | 66 | Alexander Kamkin | | buffer |
20 | 102 | Andrei Tatarnikov | | mmu |
21 | 66 | Alexander Kamkin | ; |
22 | </pre> |
||
23 | |||
24 | 103 | Andrei Tatarnikov | The expression syntax is derived from nML/Sim-nML (see [[Sim-nML Language Reference]]). |
25 | 89 | Alexander Kamkin | |
26 | 91 | Alexander Kamkin | h2. Address Description (address) |
27 | 56 | Taya Sergeeva | |
28 | 1 | Taya Sergeeva | A buffer is accessed by an _address_, which is typically a _bit vector_ of a fixed length (width). Different buffers are allowed to have a common address space (e.g., L1 and L2 are usually both addressed by physical addresses). However, in general case, each buffer has its own domain. |
29 | |||
30 | 110 | Andrei Tatarnikov | An address space is described using a keyword @address@. The description includes the address type _identifier_ and the address _width_. The latter is specified in brackets. Its value should be non-negative (zero-length addresses are permitted). |
31 | 1 | Taya Sergeeva | |
32 | 75 | Alexander Kamkin | h3. Grammar |
33 | 69 | Alexander Kamkin | |
34 | <pre> |
||
35 | address |
||
36 | 104 | Andrei Tatarnikov | : ''address'' addressTypeID ''('' expr '')'' |
37 | 69 | Alexander Kamkin | ; |
38 | </pre> |
||
39 | |||
40 | 111 | Andrei Tatarnikov | h3. Examples |
41 | 106 | Andrei Tatarnikov | |
42 | <pre>// A 64-bit virtual address (VA). |
||
43 | address VA(64)</pre> |
||
44 | |||
45 | <pre>// A 36-bit physical address (PA). |
||
46 | address PA(36)</pre> |
||
47 | |||
48 | 112 | Andrei Tatarnikov | h2. Address Space Segment Description (segment) |
49 | 1 | Taya Sergeeva | |
50 | 112 | Andrei Tatarnikov | An address space segment is specified using the @segment@ keyword. A segment is associated with a specific address type. It is possible to specify any number (≥ 0) of segments (with different names) for one address type. Each segment is characterized by its _identifier_ and _address range_. Different segments should have different names, but address ranges are allowed to overlap, and moreover, to be the same. |
51 | 1 | Taya Sergeeva | |
52 | 112 | Andrei Tatarnikov | h3. Grammar |
53 | 69 | Alexander Kamkin | |
54 | <pre> |
||
55 | 112 | Andrei Tatarnikov | segment |
56 | : ''segment'' segmentID ''('' argumentID '':'' addressTypeID '')'' |
||
57 | ''range'' ''='' ''('' expr '','' expr '')'' |
||
58 | 99 | Alexander Kamkin | ; |
59 | 97 | Alexander Kamkin | </pre> |
60 | |||
61 | 112 | Andrei Tatarnikov | h3. Examples |
62 | 97 | Alexander Kamkin | |
63 | 1 | Taya Sergeeva | <pre> |
64 | 112 | Andrei Tatarnikov | segment USEG (va: VA) |
65 | range = (0x0000000000000000, 0x000000007fffffff) |
||
66 | 97 | Alexander Kamkin | </pre> |
67 | |||
68 | 68 | Alexander Kamkin | h3. Address Format (format) |
69 | 95 | Alexander Kamkin | |
70 | 98 | Alexander Kamkin | The @format@ parameter specifies the address _format_ (a number of named fields). Any number (≥ 0) of formats (with different names) can be specified for one address. |
71 | 94 | Alexander Kamkin | |
72 | A field has three attributes: a _name_, a _width_ and, optionally, an _initial value_. |
||
73 | 69 | Alexander Kamkin | |
74 | h4. Grammar |
||
75 | |||
76 | 1 | Taya Sergeeva | <pre> |
77 | format |
||
78 | 101 | Alexander Kamkin | : ''format'' formatID ''='' ''('' |
79 | 69 | Alexander Kamkin | field ('','' field)* |
80 | '')'' |
||
81 | ; |
||
82 | |||
83 | field |
||
84 | : ID '':'' expr (''='' expr)? |
||
85 | ; |
||
86 | </pre> |
||
87 | |||
88 | 72 | Alexander Kamkin | h2. Examples |
89 | 1 | Taya Sergeeva | |
90 | <pre> |
||
91 | 66 | Alexander Kamkin | // The singleton. |
92 | 90 | Alexander Kamkin | address Void |
93 | 1 | Taya Sergeeva | // The address width is zero (this is admissible for single-item buffers). |
94 | 90 | Alexander Kamkin | width = 0 |
95 | 66 | Alexander Kamkin | </pre> |
96 | 1 | Taya Sergeeva | |
97 | 88 | Alexander Kamkin | <pre> |
98 | 90 | Alexander Kamkin | // An unstructured 64-bit virtual addresses (VA). |
99 | 84 | Alexander Kamkin | address VA |
100 | 90 | Alexander Kamkin | // The address width. |
101 | 1 | Taya Sergeeva | width = 64 |
102 | </pre> |
||
103 | 66 | Alexander Kamkin | |
104 | <pre> |
||
105 | 90 | Alexander Kamkin | // A stuctured 40-bit physical addresses (PA). |
106 | 1 | Taya Sergeeva | address PA |
107 | 90 | Alexander Kamkin | // The address width. |
108 | 1 | Taya Sergeeva | width = 40 |
109 | 84 | Alexander Kamkin | // The address format: (<39..36>, TAG=<35..12>, INDEX=<11..5>, LOCAL=<4..0>). |
110 | 97 | Alexander Kamkin | format PA_L1 = ( |
111 | 84 | Alexander Kamkin | TAG : 24, // The tag (the <35..12> address bits). |
112 | 1 | Taya Sergeeva | INDEX : 7, // The set index (the <11..5> address bits). |
113 | LOCAL : 5, // The byte position (the <0..4> address bits). |
||
114 | 90 | Alexander Kamkin | ) |
115 | 84 | Alexander Kamkin | </pre> |
116 | 2 | Taya Sergeeva | |
117 | 91 | Alexander Kamkin | h2. Buffer Description (buffer) |
118 | 76 | Alexander Kamkin | |
119 | 1 | Taya Sergeeva | A buffer is described using a keyword @buffer@. The description specifies a set of parameters, including @ways@, @sets@, @format@, @index@, @match@ and @policy@. All of the parameters except @index@ (if @sets = 1@) and @policy@ are obligatory. |
120 | 75 | Alexander Kamkin | |
121 | h3. Grammar |
||
122 | 1 | Taya Sergeeva | |
123 | 75 | Alexander Kamkin | <pre> |
124 | 83 | Alexander Kamkin | buffer |
125 | 90 | Alexander Kamkin | : ''buffer'' bufferTypeID ''('' addressTypeID addressArgID '')'' |
126 | (bufferParameter)* |
||
127 | 75 | Alexander Kamkin | ; |
128 | |||
129 | bufferParameter |
||
130 | : ways |
||
131 | | sets |
||
132 | | format |
||
133 | | index |
||
134 | | match |
||
135 | | policy |
||
136 | ; |
||
137 | 1 | Taya Sergeeva | </pre> |
138 | |||
139 | 78 | Alexander Kamkin | h3. Buffer Associativity (ways) |
140 | |||
141 | 84 | Alexander Kamkin | The @ways@ parameter specifies the buffer _associativity_ (the number of lines in a set). The parameter is obligatory; its value should be positive. |
142 | 78 | Alexander Kamkin | |
143 | 1 | Taya Sergeeva | h4. Grammar |
144 | 80 | Alexander Kamkin | |
145 | <pre> |
||
146 | ways |
||
147 | : ''ways'' ''='' expr |
||
148 | 1 | Taya Sergeeva | ; |
149 | </pre> |
||
150 | |||
151 | 80 | Alexander Kamkin | h3. Buffer Length (sets) |
152 | 83 | Alexander Kamkin | |
153 | 84 | Alexander Kamkin | The @sets@ parameter specifies the buffer _length_ (the number of sets a cache). The parameter is obligatory; its value should be positive. |
154 | 78 | Alexander Kamkin | |
155 | 1 | Taya Sergeeva | h4. Grammar |
156 | 80 | Alexander Kamkin | |
157 | <pre> |
||
158 | 1 | Taya Sergeeva | sets |
159 | 80 | Alexander Kamkin | : ''sets'' ''='' expr |
160 | ; |
||
161 | 1 | Taya Sergeeva | </pre> |
162 | |||
163 | h3. Buffer Line Format (format) |
||
164 | 96 | Alexander Kamkin | |
165 | 98 | Alexander Kamkin | The @format@ parameter specifies the buffer _line format_ (a number of named fields). Any number (≥ 0) of formats (with different names) can be specified for one buffer. |
166 | 83 | Alexander Kamkin | |
167 | 82 | Alexander Kamkin | A field has three attributes: a name, a width and, optionally, an initial value. |
168 | |||
169 | h4. Grammar |
||
170 | 1 | Taya Sergeeva | |
171 | 82 | Alexander Kamkin | <pre> |
172 | 83 | Alexander Kamkin | format |
173 | 101 | Alexander Kamkin | : ''format'' formatID ''='' ''('' field ('','' field)* '')'' |
174 | 82 | Alexander Kamkin | ; |
175 | 1 | Taya Sergeeva | |
176 | field |
||
177 | : fieldID '':'' expr (''='' expr)? |
||
178 | ; |
||
179 | </pre> |
||
180 | |||
181 | h3. Buffer Index Function (index) |
||
182 | 83 | Alexander Kamkin | |
183 | 84 | Alexander Kamkin | The @index@ parameter specifies the _address-to-index function_, which maps an address into the set index. The function may be omitted if the number of sets is @1@. |
184 | 1 | Taya Sergeeva | |
185 | h4. Grammar |
||
186 | |||
187 | 83 | Alexander Kamkin | <pre> |
188 | 1 | Taya Sergeeva | index |
189 | 90 | Alexander Kamkin | : ''index'' ''='' expr |
190 | 83 | Alexander Kamkin | ; |
191 | </pre> |
||
192 | 1 | Taya Sergeeva | |
193 | h3. Buffer Match Predicate (match) |
||
194 | 83 | Alexander Kamkin | |
195 | 84 | Alexander Kamkin | The @match@ parameter specifies the _address-line match predicate_, which checks if an address matches a line. The parameter is obligatory. |
196 | 83 | Alexander Kamkin | |
197 | h4. Grammar |
||
198 | 1 | Taya Sergeeva | |
199 | 83 | Alexander Kamkin | <pre> |
200 | index |
||
201 | 90 | Alexander Kamkin | : ''match'' ''='' expr |
202 | 1 | Taya Sergeeva | ; |
203 | </pre> |
||
204 | 83 | Alexander Kamkin | |
205 | 1 | Taya Sergeeva | h3. Buffer Data Replacement Policy (policy) |
206 | |||
207 | 57 | Taya Sergeeva | The @policy@ parameters specifies the _data replacement_ (_eviction_) _policy_. The parameter is optional. The list of supported policies includes: @RANDOM@, @FIFO@, @PLRU@ and @LRU@. |
208 | 84 | Alexander Kamkin | |
209 | 1 | Taya Sergeeva | h4. Grammar |
210 | |||
211 | <pre> |
||
212 | policy |
||
213 | : ''policy'' ''='' policyID |
||
214 | 54 | Taya Sergeeva | ; |
215 | </pre> |
||
216 | |||
217 | 1 | Taya Sergeeva | h3. Examples |
218 | |||
219 | 84 | Alexander Kamkin | <pre> |
220 | 90 | Alexander Kamkin | // A 4-way set associative cache (L1) addressed by physical addresses (PA). |
221 | buffer L1(PA addr) |
||
222 | 84 | Alexander Kamkin | // The cache associativity. |
223 | 1 | Taya Sergeeva | ways = 4 |
224 | 84 | Alexander Kamkin | // The number of sets. |
225 | 90 | Alexander Kamkin | sets = 128 |
226 | 1 | Taya Sergeeva | // The line format. |
227 | 101 | Alexander Kamkin | format LINE = ( |
228 | 85 | Alexander Kamkin | V : 1 = 0, // The validity flag (by default, the line is invalid). |
229 | TAG : 24, // The tag (the <35..12> address bits). |
||
230 | 1 | Taya Sergeeva | DATA : 256 // The data (4 double words). |
231 | 90 | Alexander Kamkin | ) |
232 | // The address-to-index function (example: using address fields). |
||
233 | index = addr.INDEX |
||
234 | // The address-line predicate (example: using address bits). |
||
235 | 101 | Alexander Kamkin | match = addr<35..12> == LINE.TAG |
236 | 1 | Taya Sergeeva | // The data replacement policy (example: using predefined policy LRU - Least Recently Used). |
237 | policy = LRU |
||
238 | 91 | Alexander Kamkin | </pre> |
239 | |||
240 | h2. Memory Description (memory) |
||
241 | |||
242 | 92 | Alexander Kamkin | A memory is described using a keyword @memory@. The description includes two obligatory parameters @read@ and @write@. |
243 | |||
244 | 91 | Alexander Kamkin | h3. Grammar |
245 | |||
246 | <pre> |
||
247 | 1 | Taya Sergeeva | memory |
248 | 92 | Alexander Kamkin | : ''memory'' memoryTypeID ''('' addressTypeID addressArgID '')'' |
249 | 91 | Alexander Kamkin | (memoryParameter)* |
250 | ; |
||
251 | |||
252 | memoryParameter |
||
253 | : read |
||
254 | | write |
||
255 | ; |
||
256 | 1 | Taya Sergeeva | </pre> |
257 | 91 | Alexander Kamkin | |
258 | 92 | Alexander Kamkin | h3. Memory Read Action (read) |
259 | 1 | Taya Sergeeva | |
260 | 92 | Alexander Kamkin | The @read@ parameter specifies the _read action_, which is a sequence of statements describing how the read operation is to be performed (by means of data transfers between buffers). The parameter is obligatory. |
261 | |||
262 | 91 | Alexander Kamkin | h4. Grammar |
263 | |||
264 | <pre> |
||
265 | read |
||
266 | : ''read'' ''='' ''{'' sequence ''}'' |
||
267 | 1 | Taya Sergeeva | ; |
268 | </pre> |
||
269 | |||
270 | 92 | Alexander Kamkin | h3. Memory Write Action (write) |
271 | |||
272 | The @write@ parameter specifies the _read action_, which is a sequence of statements describing how the write operation is to be performed (by means of data transfers between buffers). The parameter is obligatory. |
||
273 | 91 | Alexander Kamkin | |
274 | h4. Grammar |
||
275 | |||
276 | <pre> |
||
277 | write |
||
278 | : ''write'' ''='' ''{'' sequence ''}'' |
||
279 | ; |
||
280 | </pre> |
||
281 | |||
282 | h3. Examples |
||
283 | |||
284 | <pre> |
||
285 | 93 | Alexander Kamkin | // A memory unit addressed by virtual addresses (VA). |
286 | memory Memory(VA addr) |
||
287 | // The read action. |
||
288 | 1 | Taya Sergeeva | read = { |
289 | 93 | Alexander Kamkin | // Some statements. |
290 | ... |
||
291 | 1 | Taya Sergeeva | } |
292 | 93 | Alexander Kamkin | // The write action. |
293 | 1 | Taya Sergeeva | write = { |
294 | 93 | Alexander Kamkin | // Some statements. |
295 | ... |
||
296 | 91 | Alexander Kamkin | } |
297 | 1 | Taya Sergeeva | </pre> |