arm/model/arm.sml

46 type HCR =
54   { HCR: HCR, HSCTLR: HSCTLR, HSR: HSR, MVBAR: BitsN.nbit, NSACR: NSACR,
1121   : HCR, x') =
1125    TWI = TWI, VA = VA, VF = VF, VI = VI, VM = VM, hcr'rst = hcr'rst}: HCR
1129   : HCR, x') =
1133    TWI = TWI, VA = VA, VF = VF, VI = VI, VM = VM, hcr'rst = hcr'rst}: HCR
1137   : HCR, x') =
1142    hcr'rst = hcr'rst}: HCR
1146   : HCR, x') =
1151    hcr'rst = hcr'rst}: HCR
1155   : HCR, x') =
1159    TWI = TWI, VA = VA, VF = VF, VI = VI, VM = VM, hcr'rst = hcr'rst}: HCR
1163   : HCR, x') =
1167    TWI = TWI, VA = VA, VF = VF, VI = VI, VM = VM, hcr'rst = hcr'rst}: HCR
1171   : HCR, x') =
1175    TWI = TWI, VA = VA, VF = VF, VI = VI, VM = VM, hcr'rst = hcr'rst}: HCR
1179   : HCR, x') =
1184    hcr'rst = hcr'rst}: HCR
1188   : HCR, x') =
1193    hcr'rst = hcr'rst}: HCR
1197   : HCR, x') =
1202    hcr'rst = hcr'rst}: HCR
1206   : HCR, x') =
1211    hcr'rst = hcr'rst}: HCR
1215   : HCR, x') =
1220    hcr'rst = hcr'rst}: HCR
1224   : HCR, x') =
1229    hcr'rst = hcr'rst}: HCR
1233   : HCR, x') =
1238    hcr'rst = hcr'rst}: HCR
1242   : HCR, x') =
1247    hcr'rst = hcr'rst}: HCR
1251   : HCR, x') =
1256    hcr'rst = hcr'rst}: HCR
1260   : HCR, x') =
1265    hcr'rst = hcr'rst}: HCR
1269   : HCR, x') =
1274    hcr'rst = hcr'rst}: HCR
1278   : HCR, x') =
1283    hcr'rst = hcr'rst}: HCR
1287   : HCR, x') =
1292    hcr'rst = hcr'rst}: HCR
1296   : HCR, x') =
1301    hcr'rst = hcr'rst}: HCR
1305   : HCR, x') =
1310    hcr'rst = hcr'rst}: HCR
1314   : HCR, x') =
1319    hcr'rst = hcr'rst}: HCR
1323   : HCR, x') =
1328    hcr'rst = hcr'rst}: HCR
1332    hcr'rst}: HCR, x') =
1337   : HCR
1339 fun CP15_HCR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1341   {HCR = x', HSCTLR = HSCTLR, HSR = HSR, MVBAR = MVBAR, NSACR = NSACR,
1344 fun CP15_HSCTLR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1346   {HCR = HCR, HSCTLR = x', HSR = HSR, MVBAR = MVBAR, NSACR = NSACR,
1349 fun CP15_HSR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1351   {HCR = HCR, HSCTLR = HSCTLR, HSR = x', MVBAR = MVBAR, NSACR = NSACR,
1354 fun CP15_MVBAR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1356   {HCR = HCR, HSCTLR = HSCTLR, HSR = HSR, MVBAR = x', NSACR = NSACR,
1359 fun CP15_NSACR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1361   {HCR = HCR, HSCTLR = HSCTLR, HSR = HSR, MVBAR = MVBAR, NSACR = x',
1364 fun CP15_SCR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1366   {HCR = HCR, HSCTLR = HSCTLR, HSR = HSR, MVBAR = MVBAR, NSACR = NSACR,
1369 fun CP15_SCTLR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1371   {HCR = HCR, HSCTLR = HSCTLR, HSR = HSR, MVBAR = MVBAR, NSACR = NSACR,
1374 fun CP15_VBAR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1376   {HCR = HCR, HSCTLR = HSCTLR, HSR = HSR, MVBAR = MVBAR, NSACR = NSACR,
1561   ({HCR =
1905 fun rec'HCR x =
1916 fun reg'HCR x =
1933 fun write'rec'HCR (_,x) = reg'HCR x;
1935 fun write'reg'HCR (_,x) = rec'HCR x;
3196         ((#TGE((#HCR((!CP15) : CP15)) : HCR)) andalso
3247           ((#TGE((#HCR((!CP15) : CP15)) : HCR)) andalso
3456          ((#IMO((#HCR((!CP15) : CP15)) : HCR)) andalso (not(IsSecure ())))))) orelse
3546          ((#FMO((#HCR((!CP15) : CP15)) : HCR)) andalso (not(IsSecure ())))))) orelse
3698           (#TGE((#HCR((!CP15) : CP15)) : HCR)))))
6187               (#TSC((#HCR((!CP15) : CP15)) : HCR))))