arm/model/arm.sml

36 type HSR = { EC: BitsN.nbit, IL: bool, ISS: BitsN.nbit }
54   { HCR: HCR, HSCTLR: HSCTLR, HSR: HSR, MVBAR: BitsN.nbit, NSACR: NSACR,
1025 fun HSR_EC_rupd ({EC, IL, ISS}: HSR, x') = {EC = x', IL = IL, ISS = ISS}
1026   : HSR
1028 fun HSR_IL_rupd ({EC, IL, ISS}: HSR, x') = {EC = EC, IL = x', ISS = ISS}
1029   : HSR
1031 fun HSR_ISS_rupd ({EC, IL, ISS}: HSR, x') = {EC = EC, IL = IL, ISS = x'}
1032   : HSR
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,
1572     HSR = {EC = BitsN.B(0x0,6), IL = false, ISS = BitsN.B(0x0,25)},
1853 fun rec'HSR x =
1857 fun reg'HSR x =
1862 fun write'rec'HSR (_,x) = reg'HSR x;
1864 fun write'reg'HSR (_,x) = rec'HSR x;
3686         val x0 = #HSR((!CP15) : CP15)
3688         CP15 := (CP15_HSR_rupd((!CP15),write'reg'HSR(x0,(!HSRValue))))