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