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