arm/model/arm.sml

27 type SCTLR =
55     SCR: SCR, SCTLR: SCTLR, VBAR: BitsN.nbit }
862    V, VE, Z, sctlr'rst}: SCTLR, x') =
865    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
868    V, VE, Z, sctlr'rst}: SCTLR, x') =
871    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
874    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
877    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
880    V, VE, Z, sctlr'rst}: SCTLR, x') =
883    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
886    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
889    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
892    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
895    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
898    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
901    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
904    V, VE, Z, sctlr'rst}: SCTLR, x') =
907    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
910    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
913    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
916    V, VE, Z, sctlr'rst}: SCTLR, x') =
919    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
922    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
925    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
928    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
931    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
934    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
937    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
940    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
943    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
946    V, VE, Z, sctlr'rst}: SCTLR, x') =
949    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
952    V, VE, Z, sctlr'rst}: SCTLR, x') =
955    VE = VE, Z = Z, sctlr'rst = sctlr'rst}: SCTLR
958    U, V, VE, Z, sctlr'rst}: SCTLR, x') =
961    VE = x', Z = Z, sctlr'rst = sctlr'rst}: SCTLR
964    V, VE, Z, sctlr'rst}: SCTLR, x') =
967    VE = VE, Z = x', sctlr'rst = sctlr'rst}: SCTLR
970    SW, TE, U, V, VE, Z, sctlr'rst}: SCTLR, x') =
973    VE = VE, Z = Z, sctlr'rst = x'}: SCTLR
1339 fun CP15_HCR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1342    SCR = SCR, SCTLR = SCTLR, VBAR = VBAR}: CP15
1344 fun CP15_HSCTLR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1347    SCR = SCR, SCTLR = SCTLR, VBAR = VBAR}: CP15
1349 fun CP15_HSR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1352    SCR = SCR, SCTLR = SCTLR, VBAR = VBAR}: CP15
1354 fun CP15_MVBAR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1357    SCR = SCR, SCTLR = SCTLR, VBAR = VBAR}: CP15
1359 fun CP15_NSACR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1362    SCR = SCR, SCTLR = SCTLR, VBAR = VBAR}: CP15
1364 fun CP15_SCR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1367    SCR = x', SCTLR = SCTLR, VBAR = VBAR}: CP15
1369 fun CP15_SCTLR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1372    SCR = SCR, SCTLR = x', VBAR = VBAR}: CP15
1374 fun CP15_VBAR_rupd ({HCR, HSCTLR, HSR, MVBAR, NSACR, SCR, SCTLR, VBAR}
1377    SCR = SCR, SCTLR = SCTLR, VBAR = x'}: CP15
1581     SCTLR =
1791 fun rec'SCTLR x =
1804 fun reg'SCTLR x =
1821 fun write'rec'SCTLR (_,x) = reg'SCTLR x;
1823 fun write'reg'SCTLR (_,x) = rec'SCTLR x;
1951     ((v = 6) andalso (#U((#SCTLR((!CP15) : CP15)) : SCTLR)))
1992   #DZ((#SCTLR((!CP15) : CP15)) : SCTLR);
2114     val nmfi = #NMFI((#SCTLR((!CP15) : CP15)) : SCTLR)
2696       else if (#A((#SCTLR((!CP15) : CP15)) : SCTLR)) orelse
2697          (#U((#SCTLR((!CP15) : CP15)) : SCTLR))
2718       else if (#A((#SCTLR((!CP15) : CP15)) : SCTLR)) orelse
2719          (#U((#SCTLR((!CP15) : CP15)) : SCTLR))
2760         if (not(#A((#SCTLR((!CP15) : CP15)) : SCTLR))) andalso
2761            (not(#U((#SCTLR((!CP15) : CP15)) : SCTLR)))
2768         else if #A((#SCTLR((!CP15) : CP15)) : SCTLR)
2797       if (not(#A((#SCTLR((!CP15) : CP15)) : SCTLR))) andalso
2798          (not(#U((#SCTLR((!CP15) : CP15)) : SCTLR)))
2808     else if #A((#SCTLR((!CP15) : CP15)) : SCTLR)
3126   if #V((#SCTLR((!CP15) : CP15)) : SCTLR)
3137   ; CPSR := (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3138   ; CPSR := (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3151   ; CPSR := (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3152   ; CPSR := (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3174   ; CPSR := (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3175   ; CPSR := (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3222            (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3224            (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3272              (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3274              (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3375            (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3377            (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3437            (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3439            (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3503            (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3505            (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3506          ; if #VE((#SCTLR((!CP15) : CP15)) : SCTLR)
3526     ; CPSR := (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3527     ; CPSR := (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3528     ; if #VE((#SCTLR((!CP15) : CP15)) : SCTLR)
3599            (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3601            (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3602          ; if #VE((#SCTLR((!CP15) : CP15)) : SCTLR)
3623     ; CPSR := (PSR_T_rupd((!CPSR),#TE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3624     ; CPSR := (PSR_E_rupd((!CPSR),#EE((#SCTLR((!CP15) : CP15)) : SCTLR)))
3625     ; if #VE((#SCTLR((!CP15) : CP15)) : SCTLR)