Skip to content

Commit 7378b36

Browse files
febyejifebyeji
committed
Add TLBI EL1 instructions
1 parent a8c990d commit 7378b36

File tree

3 files changed

+329
-2
lines changed

3 files changed

+329
-2
lines changed

‎interface.sail‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -280,6 +280,7 @@ val iFetch : (bits(addr_size), AccessDescriptor) -> bits(32)
280280
val rMem : (bits(addr_size), AccessDescriptor) -> bits(64)
281281
val wMem_Addr : bits(addr_size) -> unit
282282
val wMem : (bits(addr_size), bits(64), AccessDescriptor) -> unit
283+
val dataMemoryBarrier : MBReqTypes -> unit
283284
val translate_address : (bits(64), AccessDescriptor) -> option(bits(addr_size))
284285

285286
val read_memory : forall 'N, 'N > 0.
@@ -328,3 +329,9 @@ function dataMemoryBarrier(types) = sail_barrier(
328329
domain = MBReqDomain_FullSystem,
329330
types = types,
330331
nXS = false}))
332+
333+
$ifdef SYSTEM_TINY_ARM
334+
val invalidateTLB : (TLBIRecord, Shareability) -> unit
335+
336+
function invalidateTLB(r, s) = sail_tlbi(struct { rec = r, shareability = s })
337+
$endif

‎registers.sail‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -188,5 +188,3 @@ register SCTLR_EL2 : bits(64)
188188
register SCTLR_EL3 : bits(64)
189189

190190
$endif
191-
192-
val dataMemoryBarrier : MBReqTypes -> unit

‎tiny-arm.sail‎

Lines changed: 322 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,21 @@
1+
$ifdef SYSTEM_TINY_ARM
12
union ast = {
23
LoadRegister : (reg_index, reg_index, reg_index),
34
StoreRegister : (reg_index, reg_index, reg_index),
45
ExclusiveOr : (reg_index, reg_index, reg_index),
56
DataMemoryBarrier : MBReqTypes,
67
CompareAndBranch : (reg_index, bits(64)),
8+
TLBIInstr : (TLBIOp, TLBILevel, TLBIMemAttr, Shareability, bool, bool, reg_index)
79
}
10+
$else
11+
union ast = {
12+
LoadRegister : (reg_index, reg_index, reg_index),
13+
StoreRegister : (reg_index, reg_index, reg_index),
14+
ExclusiveOr : (reg_index, reg_index, reg_index),
15+
DataMemoryBarrier : MBReqTypes,
16+
CompareAndBranch : (reg_index, bits(64)),
17+
}
18+
$endif
819

920
val decode : bits(32) -> option(ast)
1021

@@ -184,6 +195,316 @@ function clause execute CompareAndBranch(t, offset) = {
184195
else _PC = _PC + 4;
185196
}
186197

198+
$ifdef SYSTEM_TINY_ARM
199+
200+
/* TLB Invalidation: TLBI */
201+
val decodeTLBI : (bits(3), bits(4), bits(4), bits(3), bits(5)) -> option(ast)
202+
203+
function clause decode (0b1101010100@0b0@0b01@(op1:bits(3))@(CRn:bits(4))
204+
@(CRm:bits(4))@(op2:bits(3))
205+
@(Rt:bits(5))) = {
206+
decodeTLBI(op1, CRn, CRm, op2, Rt)
207+
}
208+
209+
function decodeTLBI(op1, CRn, CRm, op2, Rt) = {
210+
let t : reg_index = unsigned(Rt);
211+
212+
match (op1, CRn, CRm, op2) {
213+
/* TLBI VMALLE1IS: Invalidate by VMID, All, EL1, Inner-Shareable */
214+
(0b000, 0b1000, 0b0011, 0b000) => {
215+
Some(TLBIInstr(
216+
TLBIOp_VMALL,
217+
TLBILevel_Any,
218+
TLBI_AllAttr,
219+
Shareability_ISH,
220+
false,
221+
false,
222+
t
223+
))
224+
},
225+
226+
/* TLBI VMALLE1OS: Invalidate by VMID, All, EL1, Outer-Shareable */
227+
(0b000, 0b1000, 0b0001, 0b000) => {
228+
Some(TLBIInstr(
229+
TLBIOp_VMALL,
230+
TLBILevel_Any,
231+
TLBI_AllAttr,
232+
Shareability_OSH,
233+
false,
234+
false,
235+
t
236+
))
237+
},
238+
239+
/* TLBI VAE1: Invalidate by VA, EL1 */
240+
(0b000, 0b1000, 0b0111, 0b001) => {
241+
Some(TLBIInstr(
242+
TLBIOp_VA,
243+
TLBILevel_Any,
244+
TLBI_AllAttr,
245+
Shareability_NSH,
246+
false,
247+
true, /* Xt supplies VA */
248+
t
249+
))
250+
},
251+
252+
/* TLBI VAE1IS: Invalidate by VA, EL1, Inner-Shareable */
253+
(0b000, 0b1000, 0b0011, 0b001) => {
254+
Some(TLBIInstr(
255+
TLBIOp_VA,
256+
TLBILevel_Any,
257+
TLBI_AllAttr,
258+
Shareability_ISH,
259+
false,
260+
true,
261+
t
262+
))
263+
},
264+
265+
/* TLBI VAE1OS: Invalidate by VA, EL1, Outer-Shareable */
266+
(0b000, 0b1000, 0b0001, 0b001) => {
267+
Some(TLBIInstr(
268+
TLBIOp_VA,
269+
TLBILevel_Any,
270+
TLBI_AllAttr,
271+
Shareability_OSH,
272+
false,
273+
true,
274+
t
275+
))
276+
},
277+
278+
/* TLBI ASIDE1: Invalidate by ASID, EL1 (Xt supplies ASID) */
279+
(0b000, 0b1000, 0b0111, 0b010) => {
280+
Some(TLBIInstr(
281+
TLBIOp_VA, /* generic “by parameter” op */
282+
TLBILevel_Any,
283+
TLBI_AllAttr,
284+
Shareability_NSH,
285+
false,
286+
true, /* Xt supplies ASID */
287+
t
288+
))
289+
},
290+
291+
/* TLBI ASIDE1IS: Inner-Shareable */
292+
(0b000, 0b1000, 0b0011, 0b010) => {
293+
Some(TLBIInstr(
294+
TLBIOp_VA,
295+
TLBILevel_Any,
296+
TLBI_AllAttr,
297+
Shareability_ISH,
298+
false,
299+
true,
300+
t
301+
))
302+
},
303+
304+
/* TLBI ASIDE1OS: Outer-Shareable */
305+
(0b000, 0b1000, 0b0001, 0b010) => {
306+
Some(TLBIInstr(
307+
TLBIOp_VA,
308+
TLBILevel_Any,
309+
TLBI_AllAttr,
310+
Shareability_OSH,
311+
false,
312+
true,
313+
t
314+
))
315+
},
316+
317+
/* TLBI VAAE1: Invalidate by VA, All ASID, EL1 */
318+
(0b000, 0b1000, 0b0111, 0b011) => {
319+
Some(TLBIInstr(
320+
TLBIOp_VA,
321+
TLBILevel_Any,
322+
TLBI_AllAttr,
323+
Shareability_NSH,
324+
false,
325+
true,
326+
t
327+
))
328+
},
329+
330+
/* TLBI VAAE1IS: Inner-Shareable */
331+
(0b000, 0b1000, 0b0011, 0b011) => {
332+
Some(TLBIInstr(
333+
TLBIOp_VA,
334+
TLBILevel_Any,
335+
TLBI_AllAttr,
336+
Shareability_ISH,
337+
false,
338+
true,
339+
t
340+
))
341+
},
342+
343+
/* TLBI VAAE1OS: Outer-Shareable */
344+
(0b000, 0b1000, 0b0001, 0b011) => {
345+
Some(TLBIInstr(
346+
TLBIOp_VA,
347+
TLBILevel_Any,
348+
TLBI_AllAttr,
349+
Shareability_OSH,
350+
false,
351+
true,
352+
t
353+
))
354+
},
355+
356+
/* TLBI ALLE1: Invalidate All, EL1 */
357+
(0b100, 0b1000, 0b0111, 0b100) => {
358+
Some(TLBIInstr(
359+
TLBIOp_VMALL,
360+
TLBILevel_Any,
361+
TLBI_AllAttr,
362+
Shareability_NSH,
363+
false,
364+
false,
365+
t
366+
))
367+
},
368+
369+
/* TLBI ALLE1IS: Inner-Shareable */
370+
(0b100, 0b1000, 0b0011, 0b100) => {
371+
Some(TLBIInstr(
372+
TLBIOp_VMALL,
373+
TLBILevel_Any,
374+
TLBI_AllAttr,
375+
Shareability_ISH,
376+
false,
377+
false,
378+
t
379+
))
380+
},
381+
382+
/* TLBI ALLE1OS: Outer-Shareable */
383+
(0b100, 0b1000, 0b0001, 0b100) => {
384+
Some(TLBIInstr(
385+
TLBIOp_VMALL,
386+
TLBILevel_Any,
387+
TLBI_AllAttr,
388+
Shareability_OSH,
389+
false,
390+
false,
391+
t
392+
))
393+
},
394+
395+
/* TLBI VALE1: Invalidate by VA, Last-level, EL1 */
396+
(0b000, 0b1000, 0b0111, 0b101) => {
397+
Some(TLBIInstr(
398+
TLBIOp_VA,
399+
TLBILevel_Last,
400+
TLBI_AllAttr,
401+
Shareability_NSH,
402+
false,
403+
true,
404+
t
405+
))
406+
},
407+
408+
/* TLBI VALE1IS: Inner-Shareable */
409+
(0b000, 0b1000, 0b0011, 0b101) => {
410+
Some(TLBIInstr(
411+
TLBIOp_VA,
412+
TLBILevel_Last,
413+
TLBI_AllAttr,
414+
Shareability_ISH,
415+
false,
416+
true,
417+
t
418+
))
419+
},
420+
421+
/* TLBI VALE1OS: Outer-Shareable */
422+
(0b000, 0b1000, 0b0001, 0b101) => {
423+
Some(TLBIInstr(
424+
TLBIOp_VA,
425+
TLBILevel_Last,
426+
TLBI_AllAttr,
427+
Shareability_OSH,
428+
false,
429+
true,
430+
t
431+
))
432+
},
433+
434+
/* TLBI VAALE1: Invalidate by VA, All ASID, Last-level, EL1 */
435+
(0b000, 0b1000, 0b0111, 0b111) => {
436+
Some(TLBIInstr(
437+
TLBIOp_VA,
438+
TLBILevel_Last,
439+
TLBI_AllAttr,
440+
Shareability_NSH,
441+
false,
442+
true,
443+
t
444+
))
445+
},
446+
447+
/* TLBI VAALE1IS: Inner-Shareable */
448+
(0b000, 0b1000, 0b0011, 0b111) => {
449+
Some(TLBIInstr(
450+
TLBIOp_VA,
451+
TLBILevel_Last,
452+
TLBI_AllAttr,
453+
Shareability_ISH,
454+
false,
455+
true,
456+
t
457+
))
458+
},
459+
460+
/* TLBI VAALE1OS: Outer-Shareable */
461+
(0b000, 0b1000, 0b0001, 0b111) => {
462+
Some(TLBIInstr(
463+
TLBIOp_VA,
464+
TLBILevel_Last,
465+
TLBI_AllAttr,
466+
Shareability_OSH,
467+
false,
468+
true,
469+
t
470+
))
471+
},
472+
473+
/* TODO: TLBI by ranges? */
474+
_ => None()
475+
}
476+
}
477+
478+
/* TLBI */
479+
function clause execute TLBIInstr(op, level, attr, shareability,
480+
is_range, uses_addr, t) = {
481+
_PC = _PC + 4;
482+
483+
let addr = if uses_addr then X(t) else 0x0000000000000000;
484+
485+
let r : TLBIRecord = struct {
486+
op = op,
487+
from_aarch64 = true,
488+
security = SS_NonSecure,
489+
regime = Regime_EL10,
490+
vmid = 0x0000,
491+
asid = ASID_read(),
492+
level = level,
493+
attr = attr,
494+
ipaspace = PAS_NonSecure,
495+
address = addr,
496+
end_address_name = addr,
497+
d64 = true,
498+
d128 = false,
499+
ttl = 0b0000,
500+
tg = 0b00,
501+
};
502+
503+
invalidateTLB(r, shareability);
504+
}
505+
506+
$endif
507+
187508
// This needs to be the last clause
188509
function clause decode(_) = { None() }
189510

@@ -206,3 +527,4 @@ function fetch_and_execute () = {
206527
None () => assert (false, "Unsupported Encoding")
207528
}
208529
}
530+

0 commit comments

Comments
 (0)