ARM/v4/arm_evalScript.sml

3 (* DESCRIPTION   : Various theorems about the ISA and instruction encoding   *)
536   `(!cond offset. DECODE_ARM (enc (instruction$B cond offset)) = br) /\
537    (!cond offset. DECODE_ARM (enc (instruction$BL cond offset)) = br)`,
541   `!cond. DECODE_ARM (enc (instruction$SWI cond)) = swi_ex`,
557   `!f. f IN {instruction$AND; instruction$EOR;
558              instruction$SUB; instruction$RSB;
559              instruction$ADD; instruction$ADC;
560              instruction$SBC; instruction$RSC;
561              instruction$ORR; instruction$BIC} ==>
568   `!f. f IN {instruction$TST; instruction$TEQ;
569              instruction$CMP; instruction$CMN} ==>
574   `!f. f IN {instruction$MOV; instruction$MVN} ==>
582       DECODE_ARM (enc (instruction$MUL cond s rd rm rs)) = mla_mul) /\
584       DECODE_ARM (enc (instruction$MLA cond s rd rm rs rn)) = mla_mul) /\
586       DECODE_ARM (enc (instruction$UMULL cond s rdlo rdhi rm rs)) = mla_mul) /\
588       DECODE_ARM (enc (instruction$UMLAL cond s rdlo rdhi rm rs)) = mla_mul) /\
590       DECODE_ARM (enc (instruction$SMULL cond s rdlo rdhi rm rs)) = mla_mul) /\
592       DECODE_ARM (enc (instruction$SMLAL cond s rdlo rdhi rm rs)) = mla_mul)`,
597       DECODE_ARM (enc (instruction$LDR cond b opt rd rn offset)) = ldr_str) /\
599       DECODE_ARM (enc (instruction$STR cond b opt rd rn offset)) = ldr_str)`,
606       DECODE_ARM (enc (instruction$LDRH cond s h opt rd rn offset)) =
609       DECODE_ARM (enc (instruction$STRH cond opt rd rn offset)) = ldrh_strh)`,
617       DECODE_ARM (enc (instruction$LDM cond s opt rn list)) = ldm_stm) /\
619       DECODE_ARM (enc (instruction$STM cond s opt rn list)) = ldm_stm)`,
623   `!cond b rd rm rn. DECODE_ARM (enc (instruction$SWP cond b rd rm rn)) = swp`,
627   `!cond r rd. DECODE_ARM (enc (instruction$MRS cond r rd)) = mrs`,
631   `!cond psrd op.  DECODE_ARM (enc (instruction$MSR cond psrd op)) = msr`,
637       DECODE_ARM (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) =
639    (!cond. DECODE_ARM (enc (instruction$UND cond)) = cdp_und) /\
641       DECODE_ARM (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) =
644       DECODE_ARM (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = mcr) /\
646       DECODE_ARM (enc (instruction$STC cond n opt cpn crd rn offset)) =
649       DECODE_ARM (enc (instruction$LDC cond n opt cpn crd rn offset)) =
655       DECODE_CP (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) =
657    (!cond. DECODE_CP (enc (instruction$UND cond)) = cdp_und) /\
659       DECODE_CP (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = mrc) /\
661       DECODE_CP (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = mcr) /\
663       DECODE_CP (enc (instruction$STC cond n opt cpn crd rn offset)) =
666       DECODE_CP (enc (instruction$LDC cond n opt cpn crd rn offset)) =
672       enc (instruction$CDP cond cpn cop1 crd crn crm cop2) ' 27) /\
673    (!cond. enc (instruction$UND cond) ' 27 = F) /\
675       enc (instruction$MRC cond cpn cop1 rd crn crm cop2) ' 27) /\
677       enc (instruction$MCR cond cpn cop1 rd crn crm cop2) ' 27) /\
679       enc (instruction$STC cond n opt cpn crd rn offset) ' 27) /\
681       enc (instruction$LDC cond n opt cpn crd rn offset) ' 27)`,
694       DECODE_BRANCH (enc (instruction$B cond offset)) = (F, offset)) /\
696       DECODE_BRANCH (enc (instruction$BL cond offset)) = (T, offset))`,
894   `!f. f IN {instruction$AND; instruction$EOR;
895              instruction$SUB; instruction$RSB;
896              instruction$ADD; instruction$ADC;
897              instruction$SBC; instruction$RSC;
898              instruction$ORR; instruction$BIC} ==>
907   `!f. f IN {instruction$TST; instruction$TEQ;
908              instruction$CMP; instruction$CMN} ==>
917   `!f. f IN {instruction$MOV; instruction$MVN} ==>
927       DECODE_MLA_MUL (enc (instruction$MUL cond s rd rm rs)) =
930       DECODE_MLA_MUL (enc (instruction$MLA cond s rd rm rs rn)) =
933       DECODE_MLA_MUL (enc (instruction$UMULL cond s rdlo rdhi rm rs)) =
936       DECODE_MLA_MUL (enc (instruction$UMLAL cond s rdlo rdhi rm rs)) =
939       DECODE_MLA_MUL (enc (instruction$SMULL cond s rdlo rdhi rm rs)) =
942       DECODE_MLA_MUL (enc (instruction$SMLAL cond s rdlo rdhi rm rs)) =
949       DECODE_LDR_STR (enc (instruction$LDR cond b opt rd rn offset)) =
953       DECODE_LDR_STR (enc (instruction$STR cond b opt rd rn offset)) =
963       DECODE_LDRH_STRH (enc (instruction$LDRH cond s h opt rd rn offset)) =
968       DECODE_LDRH_STRH (enc (instruction$STRH cond opt rd rn offset)) =
979       DECODE_LDM_STM (enc (instruction$LDM cond s opt rn l)) =
982       DECODE_LDM_STM (enc (instruction$STM cond s opt rn l)) =
989       DECODE_SWP (enc (instruction$SWP cond b rd rm rn)) = (b,rn,rd,rm)`,
994   `!cond r rd. DECODE_MRS (enc (instruction$MRS cond r rd)) = (r, rd)`,
1001       DECODE_MSR (enc (instruction$MSR cond psrd Op2)) =
1016       (15 >< 12) (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = rd) /\
1018       (15 >< 12) (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = rd`,
1024       DECODE_LDC_STC (enc (instruction$LDC cond n opt cpn crd rn offset)) =
1027       DECODE_LDC_STC (enc (instruction$STC cond n opt cpn crd rn offset)) =
1034       enc (instruction$LDC cond n opt cpn crd rn offset) ' 20) /\
1036       ~(enc (instruction$STC cond n opt cpn crd rn offset) ' 20)`,
1042       DECODE_CDP (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) =
1045       DECODE_CPN (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) = cpn`,
1051       DECODE_MRC_MCR (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) =
1054       DECODE_CPN (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = cpn) /\
1056       DECODE_MRC_MCR (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) =
1059       DECODE_CPN (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = cpn)`,
1176       CONDITION_PASSED flgs (enc (instruction$B cond offset)) =
1179       CONDITION_PASSED flgs (enc (instruction$BL cond offset)) =
1184   `!cond flgs. CONDITION_PASSED flgs (enc (instruction$SWI cond)) =
1195   `!f. f IN {instruction$AND; instruction$EOR;
1196              instruction$SUB; instruction$RSB;
1197              instruction$ADD; instruction$ADC;
1198              instruction$SBC; instruction$RSC;
1199              instruction$ORR; instruction$BIC} ==>
1206   `!f. f IN {instruction$TST; instruction$TEQ;
1207              instruction$CMP; instruction$CMN} ==>
1214   `!f. f IN {instruction$MOV; instruction$MVN} ==>
1222       CONDITION_PASSED flgs (enc (instruction$MUL cond s rd rm rs)) =
1225       CONDITION_PASSED flgs (enc (instruction$MLA cond s rd rm rs rn)) =
1228       CONDITION_PASSED flgs (enc (instruction$UMULL cond s rdlo rdhi rm rs)) =
1231       CONDITION_PASSED flgs (enc (instruction$UMLAL cond s rdlo rdhi rm rs)) =
1234       CONDITION_PASSED flgs (enc (instruction$SMULL cond s rdlo rdhi rm rs)) =
1237       CONDITION_PASSED flgs (enc (instruction$SMLAL cond s rdlo rdhi rm rs)) =
1243       CONDITION_PASSED flgs (enc (instruction$LDR cond b opt rd rn offset)) =
1246       CONDITION_PASSED flgs (enc (instruction$STR cond b opt rd rn offset)) =
1252       CONDITION_PASSED flgs (enc (instruction$LDRH cond s h opt rd rn offset)) =
1255       CONDITION_PASSED flgs (enc (instruction$STRH cond opt rd rn offset)) =
1261       CONDITION_PASSED flgs (enc (instruction$LDM cond s opt rn list)) =
1264       CONDITION_PASSED flgs (enc (instruction$STM cond s opt rn list)) =
1270       CONDITION_PASSED flgs (enc (instruction$SWP cond b rd rm rn)) =
1276       CONDITION_PASSED flgs (enc (instruction$MRS cond r rd)) =
1282       CONDITION_PASSED flgs (enc (instruction$MSR cond psrd op)) =
1289         (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) =
1291    (!cond. CONDITION_PASSED flgs (enc (instruction$UND cond)) =
1295         (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) =
1299         (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) =
1303         (enc (instruction$STC cond n opt cpn crd rn offset)) =
1307         (enc (instruction$LDC cond n opt cpn crd rn offset)) =
1324  [`instruction$AND`, `instruction$EOR`, `instruction$SUB`, `instruction$RSB`,
1325   `instruction$ADD`, `instruction$ADC`, `instruction$SBC`, `instruction$RSC`,
1326   `instruction$ORR`, `instruction$BIC`];
1329  [`instruction$TST`, `instruction$TEQ`, `instruction$CMP`, `instruction$CMN`];
1331 val opc3 = [`instruction$MOV`, `instruction$MVN`];