MMU description » History » Version 99
Alexander Kamkin, 12/04/2014 03:15 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 | startRule |
||
13 | : bufferOrAddress* |
||
14 | ; |
||
15 | |||
16 | bufferOrAddress |
||
17 | : address |
||
18 | | buffer |
||
19 | ; |
||
20 | </pre> |
||
21 | |||
22 | 89 | Alexander Kamkin | The expression syntax is derived from nML/Sim-nML (see _MicroTESK Language Reference_). |
23 | |||
24 | 91 | Alexander Kamkin | h2. Address Description (address) |
25 | 56 | Taya Sergeeva | |
26 | 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. |
27 | |||
28 | 76 | Alexander Kamkin | An address space is described using a keyword @address@. The description can specify two parameters: @width@ (obligatory) and @format@ (optional). |
29 | 1 | Taya Sergeeva | |
30 | 75 | Alexander Kamkin | h3. Grammar |
31 | 69 | Alexander Kamkin | |
32 | <pre> |
||
33 | address |
||
34 | 90 | Alexander Kamkin | : ''address'' ID |
35 | (addressParameter)* |
||
36 | 69 | Alexander Kamkin | ; |
37 | |||
38 | addressParameter |
||
39 | : width |
||
40 | 97 | Alexander Kamkin | | segment |
41 | 69 | Alexander Kamkin | | format |
42 | ; |
||
43 | </pre> |
||
44 | |||
45 | 79 | Alexander Kamkin | h3. Address Width (width) |
46 | 1 | Taya Sergeeva | |
47 | 84 | Alexander Kamkin | The @width@ parameter specifies the address _width_. The parameter is obligatory; its value should be non-negative (zero-length addresses are permitted). |
48 | 1 | Taya Sergeeva | |
49 | 69 | Alexander Kamkin | h4. Grammar |
50 | |||
51 | <pre> |
||
52 | width |
||
53 | : ''width'' ''='' expr |
||
54 | ; |
||
55 | </pre> |
||
56 | |||
57 | 97 | Alexander Kamkin | h3. Address Space Segment (segment) |
58 | |||
59 | 99 | Alexander Kamkin | The @segment@ parameter specifies the address space _segment_. Any number (≥ 0) of segments (with different names) can be specified for one address. Each segment is characterized by its _name_ and _address range_. Different segments should have different names, but address ranges are allowed to overlap, and moreover, to be the same. |
60 | 97 | Alexander Kamkin | |
61 | h4. Grammar |
||
62 | |||
63 | <pre> |
||
64 | segment |
||
65 | : ''segment'' segmentID ''='' ''('' expr '','' expr '')'' |
||
66 | ; |
||
67 | </pre> |
||
68 | |||
69 | 68 | Alexander Kamkin | h3. Address Format (format) |
70 | 95 | Alexander Kamkin | |
71 | 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. |
72 | 94 | Alexander Kamkin | |
73 | A field has three attributes: a _name_, a _width_ and, optionally, an _initial value_. |
||
74 | 69 | Alexander Kamkin | |
75 | h4. Grammar |
||
76 | |||
77 | <pre> |
||
78 | 1 | Taya Sergeeva | format |
79 | 97 | Alexander Kamkin | : ''format'' formatID? ''='' ''('' |
80 | 69 | Alexander Kamkin | field ('','' field)* |
81 | '')'' |
||
82 | ; |
||
83 | |||
84 | field |
||
85 | : ID '':'' expr (''='' expr)? |
||
86 | ; |
||
87 | </pre> |
||
88 | |||
89 | 72 | Alexander Kamkin | h2. Examples |
90 | 1 | Taya Sergeeva | |
91 | <pre> |
||
92 | 66 | Alexander Kamkin | // The singleton. |
93 | 90 | Alexander Kamkin | address Void |
94 | 1 | Taya Sergeeva | // The address width is zero (this is admissible for single-item buffers). |
95 | 90 | Alexander Kamkin | width = 0 |
96 | 66 | Alexander Kamkin | </pre> |
97 | 1 | Taya Sergeeva | |
98 | 88 | Alexander Kamkin | <pre> |
99 | 90 | Alexander Kamkin | // An unstructured 64-bit virtual addresses (VA). |
100 | 84 | Alexander Kamkin | address VA |
101 | 90 | Alexander Kamkin | // The address width. |
102 | 1 | Taya Sergeeva | width = 64 |
103 | </pre> |
||
104 | 66 | Alexander Kamkin | |
105 | <pre> |
||
106 | 90 | Alexander Kamkin | // A stuctured 40-bit physical addresses (PA). |
107 | 1 | Taya Sergeeva | address PA |
108 | 90 | Alexander Kamkin | // The address width. |
109 | 1 | Taya Sergeeva | width = 40 |
110 | 84 | Alexander Kamkin | // The address format: (<39..36>, TAG=<35..12>, INDEX=<11..5>, LOCAL=<4..0>). |
111 | 97 | Alexander Kamkin | format PA_L1 = ( |
112 | 84 | Alexander Kamkin | TAG : 24, // The tag (the <35..12> address bits). |
113 | 1 | Taya Sergeeva | INDEX : 7, // The set index (the <11..5> address bits). |
114 | LOCAL : 5, // The byte position (the <0..4> address bits). |
||
115 | 90 | Alexander Kamkin | ) |
116 | 84 | Alexander Kamkin | </pre> |
117 | 2 | Taya Sergeeva | |
118 | 91 | Alexander Kamkin | h2. Buffer Description (buffer) |
119 | 76 | Alexander Kamkin | |
120 | 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. |
121 | 75 | Alexander Kamkin | |
122 | h3. Grammar |
||
123 | 1 | Taya Sergeeva | |
124 | 75 | Alexander Kamkin | <pre> |
125 | 83 | Alexander Kamkin | buffer |
126 | 90 | Alexander Kamkin | : ''buffer'' bufferTypeID ''('' addressTypeID addressArgID '')'' |
127 | (bufferParameter)* |
||
128 | 75 | Alexander Kamkin | ; |
129 | |||
130 | bufferParameter |
||
131 | : ways |
||
132 | | sets |
||
133 | | format |
||
134 | | index |
||
135 | | match |
||
136 | | policy |
||
137 | ; |
||
138 | 1 | Taya Sergeeva | </pre> |
139 | |||
140 | 78 | Alexander Kamkin | h3. Buffer Associativity (ways) |
141 | |||
142 | 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. |
143 | 78 | Alexander Kamkin | |
144 | 1 | Taya Sergeeva | h4. Grammar |
145 | 80 | Alexander Kamkin | |
146 | <pre> |
||
147 | ways |
||
148 | : ''ways'' ''='' expr |
||
149 | 1 | Taya Sergeeva | ; |
150 | </pre> |
||
151 | |||
152 | 80 | Alexander Kamkin | h3. Buffer Length (sets) |
153 | 83 | Alexander Kamkin | |
154 | 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. |
155 | 78 | Alexander Kamkin | |
156 | 1 | Taya Sergeeva | h4. Grammar |
157 | 80 | Alexander Kamkin | |
158 | <pre> |
||
159 | 1 | Taya Sergeeva | sets |
160 | 80 | Alexander Kamkin | : ''sets'' ''='' expr |
161 | ; |
||
162 | 1 | Taya Sergeeva | </pre> |
163 | |||
164 | h3. Buffer Line Format (format) |
||
165 | 96 | Alexander Kamkin | |
166 | 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. |
167 | 83 | Alexander Kamkin | |
168 | 82 | Alexander Kamkin | A field has three attributes: a name, a width and, optionally, an initial value. |
169 | |||
170 | h4. Grammar |
||
171 | 1 | Taya Sergeeva | |
172 | 82 | Alexander Kamkin | <pre> |
173 | 83 | Alexander Kamkin | format |
174 | 97 | Alexander Kamkin | : ''format'' formatID? ''='' ''('' field ('','' field)* '')'' |
175 | 82 | Alexander Kamkin | ; |
176 | 1 | Taya Sergeeva | |
177 | field |
||
178 | : fieldID '':'' expr (''='' expr)? |
||
179 | ; |
||
180 | </pre> |
||
181 | |||
182 | h3. Buffer Index Function (index) |
||
183 | 83 | Alexander Kamkin | |
184 | 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@. |
185 | 1 | Taya Sergeeva | |
186 | h4. Grammar |
||
187 | |||
188 | 83 | Alexander Kamkin | <pre> |
189 | 1 | Taya Sergeeva | index |
190 | 90 | Alexander Kamkin | : ''index'' ''='' expr |
191 | 83 | Alexander Kamkin | ; |
192 | </pre> |
||
193 | 1 | Taya Sergeeva | |
194 | h3. Buffer Match Predicate (match) |
||
195 | 83 | Alexander Kamkin | |
196 | 84 | Alexander Kamkin | The @match@ parameter specifies the _address-line match predicate_, which checks if an address matches a line. The parameter is obligatory. |
197 | 83 | Alexander Kamkin | |
198 | h4. Grammar |
||
199 | 1 | Taya Sergeeva | |
200 | 83 | Alexander Kamkin | <pre> |
201 | index |
||
202 | 90 | Alexander Kamkin | : ''match'' ''='' expr |
203 | 1 | Taya Sergeeva | ; |
204 | </pre> |
||
205 | 83 | Alexander Kamkin | |
206 | 1 | Taya Sergeeva | h3. Buffer Data Replacement Policy (policy) |
207 | |||
208 | 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@. |
209 | 84 | Alexander Kamkin | |
210 | 1 | Taya Sergeeva | h4. Grammar |
211 | |||
212 | <pre> |
||
213 | policy |
||
214 | : ''policy'' ''='' policyID |
||
215 | 54 | Taya Sergeeva | ; |
216 | </pre> |
||
217 | |||
218 | 1 | Taya Sergeeva | h3. Examples |
219 | |||
220 | 84 | Alexander Kamkin | <pre> |
221 | 90 | Alexander Kamkin | // A 4-way set associative cache (L1) addressed by physical addresses (PA). |
222 | buffer L1(PA addr) |
||
223 | 84 | Alexander Kamkin | // The cache associativity. |
224 | 90 | Alexander Kamkin | ways = 4 |
225 | 84 | Alexander Kamkin | // The number of sets. |
226 | 90 | Alexander Kamkin | sets = 128 |
227 | 1 | Taya Sergeeva | // The line format. |
228 | 85 | Alexander Kamkin | format = ( |
229 | V : 1 = 0, // The validity flag (by default, the line is invalid). |
||
230 | TAG : 24, // The tag (the <35..12> address bits). |
||
231 | 84 | Alexander Kamkin | DATA : 256 // The data (4 double words). |
232 | 90 | Alexander Kamkin | ) |
233 | // The address-to-index function (example: using address fields). |
||
234 | index = addr.INDEX |
||
235 | // The address-line predicate (example: using address bits). |
||
236 | match = addr<35..12> == TAG |
||
237 | 1 | Taya Sergeeva | // The data replacement policy (example: using predefined policy LRU - Least Recently Used). |
238 | policy = LRU |
||
239 | 91 | Alexander Kamkin | </pre> |
240 | |||
241 | h2. Memory Description (memory) |
||
242 | |||
243 | 92 | Alexander Kamkin | A memory is described using a keyword @memory@. The description includes two obligatory parameters @read@ and @write@. |
244 | |||
245 | 91 | Alexander Kamkin | h3. Grammar |
246 | |||
247 | <pre> |
||
248 | 1 | Taya Sergeeva | memory |
249 | 92 | Alexander Kamkin | : ''memory'' memoryTypeID ''('' addressTypeID addressArgID '')'' |
250 | 91 | Alexander Kamkin | (memoryParameter)* |
251 | ; |
||
252 | |||
253 | memoryParameter |
||
254 | : read |
||
255 | | write |
||
256 | ; |
||
257 | 1 | Taya Sergeeva | </pre> |
258 | 91 | Alexander Kamkin | |
259 | 92 | Alexander Kamkin | h3. Memory Read Action (read) |
260 | 1 | Taya Sergeeva | |
261 | 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. |
262 | |||
263 | 91 | Alexander Kamkin | h4. Grammar |
264 | |||
265 | <pre> |
||
266 | read |
||
267 | : ''read'' ''='' ''{'' sequence ''}'' |
||
268 | 1 | Taya Sergeeva | ; |
269 | </pre> |
||
270 | |||
271 | 92 | Alexander Kamkin | h3. Memory Write Action (write) |
272 | |||
273 | 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. |
||
274 | 91 | Alexander Kamkin | |
275 | h4. Grammar |
||
276 | |||
277 | <pre> |
||
278 | write |
||
279 | : ''write'' ''='' ''{'' sequence ''}'' |
||
280 | ; |
||
281 | </pre> |
||
282 | |||
283 | h3. Examples |
||
284 | |||
285 | <pre> |
||
286 | 93 | Alexander Kamkin | // A memory unit addressed by virtual addresses (VA). |
287 | memory Memory(VA addr) |
||
288 | // The read action. |
||
289 | 1 | Taya Sergeeva | read = { |
290 | 93 | Alexander Kamkin | // Some statements. |
291 | ... |
||
292 | 1 | Taya Sergeeva | } |
293 | 93 | Alexander Kamkin | // The write action. |
294 | 1 | Taya Sergeeva | write = { |
295 | 93 | Alexander Kamkin | // Some statements. |
296 | ... |
||
297 | 91 | Alexander Kamkin | } |
298 | 1 | Taya Sergeeva | </pre> |