ARM/v7/arm_decoderScript.sml

662       of (a8,a7, F,a5, F, b7,b6,b5,b4) =>
664              LoadStore (Store_Return_State (~a8) a8 a5 ((4 >< 0) ireg2))
666              LoadStore (Store_Multiple a8 a7 F a5 (ra 0) ireg2))
667        | (a8,a7, F,a5, T, b7,b6,b5,b4) =>
672                LoadStore (Return_From_Exception (~a8) a8 a5 (ra 0))
677                LoadStore (Load_Multiple a8 a7 F a5 (ra 0) ireg2))
702        | ( T,a7, T,a5, F, b7,b6,b5,b4) =>
703            LoadStore (Store_Dual T a7 a5 (ra 0) (rb 12) (rb 8)
708        | ( T,a7, T,a5, T, b7,b6,b5,b4) =>
709            LoadStore (Load_Dual T a7 a5 (ra 0) (rb 12) (rb 8)
799        | (F,F, T,a6,a5, F) =>
801              (Coprocessor_Store F T a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0))
802        | (F,T,a7,a6,a5, F) =>
804              (Coprocessor_Store T a7 a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0))
808        | (F,F, T,a6,a5, T) =>
810              (Coprocessor_Load F T a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0))
811        | (F,T,a7,a6,a5, T) =>
813              (Coprocessor_Load T a7 a6 a5 (ra 0) (rb 12) (ib4 8) (ib8 0))
814        | (T,F,a7,a6,a5,a4) =>
910          | (T,a7, F,a5) =>
912               if a5 /\ (imm5 = 0w) then
915                 DataProcessing (Saturate a7 (ib5 0) (rb 8) imm5 a5 (ra 0)))
983        | (a10, T, T, T,a6,a5,a4, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) =>
985        | (a10,a9,a8,a7,a6,a5,a4, F ,b13, F ,b11,b10,b9,b8,b7,b6,b5,b4) =>
991        | (a10,a9,a8,a7,a6,a5,a4, F ,b13, T ,b11,b10,b9,b8,b7,b6,b5,b4) =>
997        | (a10,a9,a8,a7,a6,a5,a4, T ,b13,b12,b11,b10,b9,b8,b7,b6,b5,b4) =>
1039              | (T,a7,a6,a5) =>
1044             of (F,T,F,a5,  b11,b10,b9,b8,b7,b6) =>
1046                    (Preload_Data T a5 rn (Mode2_immediate (ib12 0)))
1047              | (F,F,F,a5,   T , T , F, F,b7,b6) =>
1049                    (Preload_Data T a5 rn (Mode2_immediate ((7 >< 0) ireg2)))
1050              | (F,F,F,a5,   F , F , F, F, F, F) =>
1052                    (Preload_Data T a5 rn
1054              | (F,F,F,a5,   T ,b10,b9, T,b7,b6) =>
1056              | (F,F,F,a5,   T , T , T, F,b7,b6) =>
1094              | (T,F,F,a5,   T ,b10,b9, T,b7,b6) =>
1096              | (T,F,F,a5,   T , T , T, F,b7,b6) =>
1110              | (T,a7, F,a5) =>
1112                    (Load_Halfword T a7 F T a5 F rn rt
1146              | ( T, T, F,a5,  b11,b10,b9,b8,b7,b6) =>
1148                    (Load_Halfword T T F T a5 F rn rt (Mode3_immediate (ib12 0)))
1149              | ( T, F, F,a5,   T ,b10,b9, T,b7,b6) =>
1151                    (Load_Halfword b10 b9 T T a5 F rn rt
1153              | ( T, F, F,a5,   T , T ,b9, F,b7,b6) =>
1155                    (Load_Halfword T b9 F T a5 b9 rn rt
1157              | ( T, F, F,a5,   F , F , F, F, F, F) =>
1159                    (Load_Halfword T T F T a5 F rn rt
1331            | (T,a6,a5, F,  F,F, F, F) =>
1333                  (Multiply_Long (~a5) a6 F (rb 8) rb12 (rb 0) (ra 0))
1334            | (T, F,a5, T,  T,T, T, T) =>
1335                DataProcessing (Divide a5 (ra 0) (rb 8) (rb 0))
1410    let (q1,a5)   = DIVMOD_2EXP 1 q0 in
1416      (ODD q3,a7 = 1,a6 = 1,a5 = 1,a4 = 1,
1420    let (q1,a5)   = DIVMOD_2EXP 1 q0 in
1423      (ODD q3,a7 = 1,a6 = 1,a5 = 1)) /\
1428    let (q1,a5)   = DIVMOD_2EXP 1 q0 in
1443      (ODD r5,a9 = 1,a8 = 1,a7 = 1,a6 = 1,a5 = 1,a4 = 1,
1448    let (q1,a5)   = DIVMOD_2EXP 1 q0 in
1452      (ODD q4,a8 = 1,a7 = 1,a6 = 1,a5 = 1,a4 = 1)) /\
1460    let (q1,a5)   = DIVMOD_2EXP 1 q0 in
1465      (ODD r2,a6 = 1,a5 = 1,a4 = 1,
1469    let (q0,a5)   = DIVMOD_2EXP 1 (DIV_2EXP 5 m) in
1477      (ODD r2,a7 = 1,a6 = 1,a5 = 1,
1480    let (q0,a5)   = DIVMOD_2EXP 1 (DIV_2EXP 5 m) in
1483    (ODD q2,a7 = 1,a6 = 1,a5 = 1,BIT 11 n))`,