Skip to content

Commit 0aae602

Browse files
febyejifebyeji
committed
Add DSB, ISB instructions
1 parent 7378b36 commit 0aae602

File tree

5 files changed

+298
-507
lines changed

5 files changed

+298
-507
lines changed

‎instrs-sys.sail‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
$ifdef SYSTEM_TINY_ARM
2+
/* TLBI */
3+
val decodeTLBI : (bits(3), bits(4), bits(4), bits(3), bits(5)) -> option(ast)
4+
function clause decode (0b1101010100001@(op1:bits(3))@(CRn:bits(4))@(CRm:bits(4))@(op2:bits(3))@(Rt:bits(5))) = {
5+
decodeTLBI(op1, CRn, CRm, op2, Rt)
6+
}
7+
8+
function decodeTLBI(op1, CRn, CRm, op2, Rt) = {
9+
let t : reg_index = unsigned(Rt);
10+
/* We are only considering invalidations applied to EL1 in the ISH domain */
11+
let tlbi_op : TLBIOp =
12+
match (op1, CRn, CRm, op2) {
13+
/* TLBI ALL (TLBI ALLE1IS) */
14+
(0b100, 0b1000, 0b0111, 0b100) => TLBIOp_ALL,
15+
/* TLBI by VA (TLBI VAE1IS) */
16+
(0b000, 0b1000, 0b0011, 0b001) => TLBIOp_VA,
17+
/* TLBI by ASID (TLBI ASIDE1IS) */
18+
(0b000, 0b1000, 0b0011, 0b010) => TLBIOp_ASID,
19+
/* TLBI by VA, all ASIDs (TLBI VAAE1IS) */
20+
(0b000, 0b1000, 0b0011, 0b011) => TLBIOp_VAA,
21+
_ => return None()
22+
};
23+
Some(TLBInvalidation(tlbi_op, t))
24+
}
25+
26+
function clause execute TLBInvalidation(op, t) = {
27+
let (va, asid) : (option(bits(64)), option(bits(16))) =
28+
match op {
29+
TLBIOp_ALL => (None(), None()),
30+
TLBIOp_VA => (Some(X(t)), None()),
31+
TLBIOp_ASID => (None(), Some(X(t)[63..48])),
32+
TLBIOp_VAA => (Some(X(t)), None()),
33+
_ => return ()
34+
};
35+
36+
_PC = _PC + 4;
37+
reportTLBI(op, va, asid);
38+
}
39+
$endif

‎instrs-user.sail‎

Lines changed: 199 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
1+
/* LoadStoreRegister: LDR and STR */
2+
val decodeLoadStoreRegister : (bits(2), bits(5), bits(3), bit, bits(5), bits(5)) -> option(ast)
3+
4+
function clause decode (0b11@0b111@0b0@0b00@(opc:bits(2))@0b1@(Rm:bits(5))@(option_v:bits(3))@[S]@0b10@(Rn:bits(5))@(Rt:bits(5))) = {
5+
decodeLoadStoreRegister(opc, Rm, option_v, S, Rn, Rt)
6+
}
7+
8+
function decodeLoadStoreRegister (opc, Rm, option_v, S, Rn, Rt) = {
9+
let t : reg_index = unsigned(Rt);
10+
let n : reg_index = unsigned(Rn);
11+
let m : reg_index = unsigned(Rm);
12+
/* option_v == 0b011 and S == 1 means that the offset in Rm is used as is and not shifted or extended */
13+
if option_v != 0b011 | S == bitone then None ()
14+
else if opc == 0b01
15+
then Some(LoadRegister((t,n,m)))
16+
else if opc == 0b00
17+
then Some(StoreRegister((t,n,m)))
18+
else None ();
19+
}
20+
21+
/* LDR Xt, [Xn, Xm] */
22+
function clause execute LoadRegister(t, n, m) = {
23+
/* Ask for the value of register Xn and record it in the local
24+
* variable base_addr */
25+
let base_addr = X(n);
26+
/* Ask for the value of register Xm and record it in the local
27+
* variable offset */
28+
let offset = X(m);
29+
/* Compute the address */
30+
let addr = base_addr + offset;
31+
let accdesc = create_readAccessDescriptor();
32+
/* Translate the virtual address into the physical address.
33+
* In the user mode, `translate_address` returns input address. */
34+
let addr : bits(addr_size) =
35+
match translate_address(addr, accdesc) {
36+
Some(addr) => addr,
37+
None() => return () // A translation fault is handled in `translate_address`.
38+
};
39+
/* The instruction can't fault now (in a real model), so update the PC */
40+
_PC = _PC + 4;
41+
/* Ask for the eight-byte value in memory starting from location
42+
addr and record it in the local variable data */
43+
let data = rMem(addr, accdesc);
44+
/* Ask for the value of data to be written to register Xt */
45+
X(t) = data;
46+
}
47+
48+
/* STR Xt, [Xn, Xm] */
49+
function clause execute StoreRegister(t, n, m) = {
50+
/* Ask for the value of register Xn and record it in the local
51+
* variable base_addr */
52+
let base_addr = X(n);
53+
/* Ask for the value of register Xm and record it in the local
54+
* variable offset */
55+
let offset = X(m);
56+
/* Compute the address */
57+
let addr = base_addr + offset;
58+
let accdesc = create_writeAccessDescriptor();
59+
/* Translate the virtual address into the physical address.
60+
* In the user mode, `translate_address` returns input address. */
61+
let addr : bits(addr_size) =
62+
match translate_address(addr, accdesc) {
63+
Some(addr) => addr,
64+
None() => return () // A translation fault is handled in `translate_address`.
65+
};
66+
/* Announce that a store into the eight bytes of memory starting
67+
* from location addr will be performed later */
68+
wMem_Addr(addr);
69+
/* The instruction can't fault now (in a real model), so update the PC */
70+
_PC = _PC + 4;
71+
/* Ask for the value of register Xt and record it in the local
72+
* variable data */
73+
let data = X(t);
74+
/* Ask for the value of data to be stored into the eight bytes of
75+
* memory starting from location addr */
76+
wMem(addr, data, accdesc);
77+
}
78+
79+
/* Exclusive OR: EOR */
80+
val decodeExclusiveOr : (bit, bits(2), bit, bits(5), bits(6), bits(5), bits(5)) -> option(ast)
81+
82+
function clause decode ([sf]@0b10@0b01010@(shift:bits(2))@[N]@(Rm:bits(5))@(imm6:bits(6))@(Rn:bits(5))@(Rd:bits(5))) = {
83+
decodeExclusiveOr(sf, shift, N, Rm, imm6, Rn, Rd)
84+
}
85+
86+
function decodeExclusiveOr (sf, shift, N, Rm, imm6, Rn, Rd) = {
87+
let d : reg_index = unsigned(Rd);
88+
let n : reg_index = unsigned(Rn);
89+
let m : reg_index = unsigned(Rm);
90+
91+
if sf == bitzero & imm6[5] == bitone then None ()
92+
else if imm6 != 0b000000 then None ()
93+
else Some(ExclusiveOr((d,n,m)));
94+
}
95+
96+
/* EOR Xd, Xn, Xm */
97+
function clause execute ExclusiveOr(d, n, m) = {
98+
/* Increment the program counter, at the start, since no branching out possible */
99+
_PC = _PC + 4;
100+
/* Ask for the value of register Xn and record it in the local
101+
* variable operand1 */
102+
let operand1 = X(n);
103+
/* Ask for the value of register Xm and record it in the local
104+
* variable operand2 */
105+
let operand2 = X(m);
106+
/* Compute the bitwise exclusive OR, and ask for the value of
107+
* the result to be written to register Xd */
108+
X(d) = operand1 ^ operand2;
109+
}
110+
111+
/* Data Barrier */
112+
val decodeDataBarrier : (bits(4), bool) -> option(ast)
113+
114+
function decodeDataBarrier(CRm, is_sync) = {
115+
let types : MBReqTypes =
116+
match CRm[1..0] {
117+
0b01 => MBReqTypes_Reads,
118+
0b10 => MBReqTypes_Writes,
119+
0b11 => MBReqTypes_All,
120+
_ => return None()
121+
};
122+
123+
if is_sync then
124+
Some(DataSynchronizationBarrier(types))
125+
else
126+
Some(DataMemoryBarrier(types))
127+
}
128+
129+
/* DMB */
130+
function clause decode (0b1101010100@0b0@0b00@0b011@0b0011@(CRm : bits(4))@0b1@0b01@0b11111) = {
131+
decodeDataBarrier(CRm, false)
132+
}
133+
134+
function clause execute DataMemoryBarrier(types) = {
135+
// Update the PC
136+
_PC = _PC + 4;
137+
// Then perform the barrier
138+
dataMemoryBarrier(types);
139+
}
140+
141+
/* DSB */
142+
function clause decode (0b11010101000000110011@(CRm:bits(4))@0b100@0b11111) = {
143+
decodeDataBarrier(CRm, true)
144+
}
145+
146+
function clause execute DataSynchronizationBarrier(types) = {
147+
// Update the PC
148+
_PC = _PC + 4;
149+
// Then perform the barrier
150+
dataSynchronizationBarrer(types)
151+
}
152+
153+
/* ISB */
154+
function clause decode (0b11010101000000110011@(CRm:bits(4))@0b110@0b11111) = {
155+
Some(InstructionSynchronizationBarrier())
156+
}
157+
158+
function clause execute InstructionSynchronizationBarrier() = {
159+
// Update the PC
160+
_PC = _PC + 4;
161+
// Then perform the barrier
162+
instructionSynchronizationBarrier()
163+
}
164+
165+
/* CompareAndBranch: CBZ */
166+
val decodeCompareAndBranch : (bits(19), bits(5)) -> option(ast)
167+
168+
function clause decode (0b1@0b011010@0b0@(imm19:bits(19))@(Rt:bits(5))) = {
169+
decodeCompareAndBranch(imm19, Rt)
170+
}
171+
172+
function decodeCompareAndBranch(imm19, Rt) = {
173+
let t : reg_index = unsigned(Rt);
174+
let offset : bits(64) = sail_sign_extend(imm19@0b00,64);
175+
176+
Some(CompareAndBranch(t,offset));
177+
}
178+
179+
/* CBZ Xt, <offset> */
180+
function clause execute CompareAndBranch(t, offset) = {
181+
/* Ask for the value of register Xt and record it in the local
182+
* variable operand */
183+
let operand = X(t);
184+
/* Check if operand is 0 */
185+
if operand == 0x0000000000000000 then {
186+
/* Ask for the value of the program counter register and record it
187+
* in the local variable base */
188+
let base = PC();
189+
/* Compute the address */
190+
let addr = base + offset;
191+
/* Ask for the value of result to be written to the program counter
192+
* register */
193+
PC() = addr;
194+
}
195+
else _PC = _PC + 4;
196+
}
197+
198+
// This catch-all clause MUST be the last clause for the `decode` function.
199+
function clause decode(_) = { None() }

‎interface.sail‎

Lines changed: 46 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,25 @@ function base_AddressDescriptor (accdesc: AccessDescriptor) -> AddressDescriptor
216216
mecid = sail_zeros(16),
217217
vaddress = sail_zeros(64)
218218
}
219+
220+
function base_TLBIRecord (op : TLBIOp) -> TLBIRecord = struct {
221+
op = op,
222+
from_aarch64 = true,
223+
security = SS_NonSecure,
224+
regime = Regime_EL10,
225+
vmid = 0x0000,
226+
asid = 0x0000,
227+
level = TLBILevel_Any,
228+
attr = TLBI_AllAttr,
229+
ipaspace = PAS_NonSecure,
230+
address = sail_zeros(64),
231+
end_address_name = sail_zeros(64),
232+
d64 = true,
233+
d128 = false,
234+
ttl = 0b0000,
235+
tg = 0b00,
236+
}
237+
219238
$endif
220239

221240
$ifdef SYSTEM_TINY_ARM
@@ -275,12 +294,15 @@ instantiation sail_mem_address_announce with
275294
'CHERI = false,
276295
'cap_size_log = 0
277296

278-
/* See tiny-arm for descriptions, interface for definitions */
297+
/* See tiny-arm for descriptions, interface for definitions */
279298
val iFetch : (bits(addr_size), AccessDescriptor) -> bits(32)
280299
val rMem : (bits(addr_size), AccessDescriptor) -> bits(64)
281300
val wMem_Addr : bits(addr_size) -> unit
282301
val wMem : (bits(addr_size), bits(64), AccessDescriptor) -> unit
283302
val dataMemoryBarrier : MBReqTypes -> unit
303+
val dataSynchronizationBarrer : MBReqTypes -> unit
304+
val instructionSynchronizationBarrier : unit -> unit
305+
284306
val translate_address : (bits(64), AccessDescriptor) -> option(bits(addr_size))
285307

286308
val read_memory : forall 'N, 'N > 0.
@@ -326,12 +348,32 @@ instantiation sail_barrier with
326348

327349
function dataMemoryBarrier(types) = sail_barrier(
328350
Barrier_DMB(struct{
329-
domain = MBReqDomain_FullSystem,
351+
domain = MBReqDomain_InnerShareable,
352+
types = types,
353+
nXS = false}))
354+
355+
function dataSynchronizationBarrer(types) = sail_barrier(
356+
Barrier_DSB(struct{
357+
domain = MBReqDomain_InnerShareable,
330358
types = types,
331359
nXS = false}))
332360

361+
function instructionSynchronizationBarrier() = sail_barrier(Barrier_ISB())
362+
333363
$ifdef SYSTEM_TINY_ARM
334-
val invalidateTLB : (TLBIRecord, Shareability) -> unit
364+
val reportTLBI : (TLBIOp, option(bits(64)), option(bits(16))) -> unit
335365

336-
function invalidateTLB(r, s) = sail_tlbi(struct { rec = r, shareability = s })
366+
function reportTLBI(op, addr, asid) = {
367+
var r = base_TLBIRecord(op);
368+
r.address = match addr {
369+
Some(addr) => addr,
370+
None() => 0x0000000000000000
371+
};
372+
r.asid = match asid {
373+
Some(asid) => asid,
374+
None() => 0x0000
375+
};
376+
377+
sail_tlbi(struct { rec = r, shareability = Shareability_ISH })
378+
}
337379
$endif

‎sail_files‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,6 @@ interface_types.sail
33
registers.sail
44
interface.sail
55
translation.sail
6-
tiny-arm.sail
6+
tiny-arm.sail
7+
instrs-sys.sail
8+
instrs-user.sail

0 commit comments

Comments
 (0)