Lines Matching defs:x0
1558 val CP14 = ref ({TEEHBR = BitsN.B(0x0,32)}): CP14 ref
1562 {AMO = false, BSU = BitsN.B(0x0,2), DC = false, FB = false,
1564 TGE = false, TID = BitsN.B(0x0,4), TIDCP = false, TPC = false,
1567 VM = false, hcr'rst = BitsN.B(0x0,4)},
1571 hsctlr'rst = BitsN.B(0x0,23)},
1572 HSR = {EC = BitsN.B(0x0,6), IL = false, ISS = BitsN.B(0x0,25)},
1573 MVBAR = BitsN.B(0x0,32),
1576 cp = BitsN.B(0x0,14), nsacr'rst = BitsN.B(0x0,14)},
1580 scr'rst = BitsN.B(0x0,22)},
1585 V = false, VE = false, Z = false, sctlr'rst = BitsN.B(0x0,14)},
1586 VBAR = BitsN.B(0x0,32)}): CP15 ref
1589 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1590 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1592 psr'rst = BitsN.B(0x0,4)}): PSR ref
1594 val CurrentCondition = ref (BitsN.B(0x0,4)): BitsN.nbit ref
1596 val ELR_hyp = ref (BitsN.B(0x0,32)): BitsN.nbit ref
1607 QC = false, RMode = BitsN.B(0x0,2), UFC = false, UFE = false,
1608 V = false, Z = false, fpscr'rst = BitsN.B(0x0,10)},
1609 REG = Map.mkMap(SOME 32,BitsN.B(0x0,64))}): FP ref
1611 val MEM = ref (Map.mkMap(SOME 4294967296,BitsN.B(0x0,8)))
1614 val REG = ref (Map.mkMap(SOME 34,BitsN.B(0x0,32)))
1618 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1619 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1621 psr'rst = BitsN.B(0x0,4)}): PSR ref
1624 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1625 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1627 psr'rst = BitsN.B(0x0,4)}): PSR ref
1630 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1631 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1633 psr'rst = BitsN.B(0x0,4)}): PSR ref
1636 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1637 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1639 psr'rst = BitsN.B(0x0,4)}): PSR ref
1642 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1643 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1645 psr'rst = BitsN.B(0x0,4)}): PSR ref
1648 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1649 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1651 psr'rst = BitsN.B(0x0,4)}): PSR ref
1654 ({A = false, C = false, E = false, F = false, GE = BitsN.B(0x0,4),
1655 I = false, IT = BitsN.B(0x0,8), J = false, M = BitsN.B(0x0,5),
1657 psr'rst = BitsN.B(0x0,4)}): PSR ref
2005 BitsN.B(0x0,_) => InstrSet_ARM
2016 else write'ISETSTATE(BitsN.B(0x0,2))
2022 if HaveThumb2 () then #IT((!CPSR) : PSR) else BitsN.B(0x0,8);
2028 then if (BitsN.bits(2,0) (ITSTATE ())) = (BitsN.B(0x0,3))
2029 then write'ITSTATE(BitsN.B(0x0,8))
2039 fun InITBlock () = not((BitsN.bits(3,0) (ITSTATE ())) = (BitsN.B(0x0,4)));
2044 if (ITSTATE ()) = (BitsN.B(0x0,8))
2046 else if not((BitsN.bits(3,0) (#IT((!CPSR) : PSR))) = (BitsN.B(0x0,4)))
2065 BitsN.B(0x0,_) => #Z((!CPSR) : PSR)
2360 BitsN.B(0x0,_) => RName_0usr
2421 ((not((BitsN.bits(1,0) value) = (BitsN.B(0x0,2)))) andalso
2466 (not((BitsN.bits(1,0) address) = (BitsN.B(0x0,2))))
2469 ; BranchTo(BitsN.@@(BitsN.bits(31,2) address,BitsN.B(0x0,2)))
2471 else BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1)));
2477 (BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1)))
2481 ; BranchTo(BitsN.@@(BitsN.bits(31,1) address,BitsN.B(0x0,1)))
2513 1 => Bitstring.bits(7,0) (mem1(BitsN.+(address,BitsN.B(0x0,32))))
2518 (mem1(BitsN.+(address,BitsN.B(0x0,32)))))
2525 mem1(BitsN.+(address,BitsN.B(0x0,32)))])
2536 mem1(BitsN.+(address,BitsN.B(0x0,32)))])
2543 val x = BitsN.+(address,BitsN.B(0x0,32))
2552 val x = BitsN.+(address,BitsN.B(0x0,32))
2570 val x = BitsN.+(address,BitsN.B(0x0,32))
2604 val x = BitsN.+(address,BitsN.B(0x0,32))
2692 val VA = ref (BitsN.B(0x0,32))
2714 val VA = ref (BitsN.B(0x0,32))
2856 then if (Align 32 (PC (),4)) = (BitsN.B(0x0,32))
2860 then if (SP ()) = (BitsN.B(0x0,32))
2863 else if (R n) = (BitsN.B(0x0,32))
2866 ; write'ITSTATE(BitsN.B(0x0,8))
2878 if w = (BitsN.BV(0x0,N)) then IntInf.~ 1 else BitsN.toInt(BitsN.log2 w);
2883 (IntInf.-(Nat.toInt(BitsN.size(BitsN.BV(0x0,N))),1),
2893 (0,Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),
2902 val s = Nat.-(Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),p)
2913 ( if Nat.<(BitsN.size(BitsN.BV(0x0,M)),N)
2928 ( if Nat.<(BitsN.size(BitsN.BV(0x0,M)),N)
2937 then (BitsN.BV(0x0,M),true)
2956 Bitstring.bit(extended_x,BitsN.size(BitsN.BV(0x0,N))))
2965 (Nat.<=(shift,BitsN.size(BitsN.BV(0x0,N)))) andalso
2974 BitsN.bit(x,Nat.-(Nat.min(BitsN.size(BitsN.BV(0x0,N)),shift),1)))
2992 (Bitstring.bits(Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),1)
3002 BitsN.B(0x0,_) => (SRType_LSL,BitsN.toNat imm5)
3004 (SRType_LSR,if imm5 = (BitsN.B(0x0,5)) then 32 else BitsN.toNat imm5)
3006 (SRType_ASR,if imm5 = (BitsN.B(0x0,5)) then 32 else BitsN.toNat imm5)
3008 if imm5 = (BitsN.B(0x0,5))
3015 BitsN.B(0x0,_) => SRType_LSL
3046 if (BitsN.bits(11,10) imm12) = (BitsN.B(0x0,2))
3050 BitsN.B(0x0,_) =>
3053 if (BitsN.bits(7,0) imm12) = (BitsN.B(0x0,8))
3056 [BitsN.B(0x0,8),BitsN.bits(7,0) imm12,
3057 BitsN.B(0x0,8),BitsN.bits(7,0) imm12]
3059 if (BitsN.bits(7,0) imm12) = (BitsN.B(0x0,8))
3062 [BitsN.bits(7,0) imm12,BitsN.B(0x0,8),
3063 BitsN.bits(7,0) imm12,BitsN.B(0x0,8)]
3065 if (BitsN.bits(7,0) imm12) = (BitsN.B(0x0,8))
3103 BitsN.B(0x0,_) => (BitsN.&&(a,b),(c,false))
3130 else BitsN.B(0x0,32);
3142 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3156 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3164 val x0 = #SCR((!CP15) : CP15)
3166 CP15 := (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3172 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3176 ; BranchTo(BitsN.+(ExcVectorBase (),BitsN.B(0x0,32)))
3210 val x0 = #SCR((!CP15) : CP15)
3212 CP15 := (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3219 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3259 val x0 = #SCR((!CP15) : CP15)
3262 (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3269 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3292 val x0 = #SCR((!CP15) : CP15)
3294 CP15 := (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3340 val x0 = #SCR((!CP15) : CP15)
3343 (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3357 val x0 = #SCR((!CP15) : CP15)
3359 CP15 := (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3372 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3402 val x0 = #SCR((!CP15) : CP15)
3405 (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3419 val x0 = #SCR((!CP15) : CP15)
3421 CP15 := (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3434 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3462 val x0 = #SCR((!CP15) : CP15)
3465 (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3474 {EC = BitsN.B(0x0,6), IL = false, ISS = BitsN.B(0x0,25)}))
3485 val x0 = #SCR((!CP15) : CP15)
3487 CP15 := (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3500 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3524 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3552 val x0 = #SCR((!CP15) : CP15)
3555 (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3564 {EC = BitsN.B(0x0,6), IL = false, ISS = BitsN.B(0x0,25)}))
3575 val x0 = #SCR((!CP15) : CP15)
3577 CP15 := (CP15_SCR_rupd((!CP15),SCR_NS_rupd(x0,false)))
3596 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3621 ; CPSR := (PSR_IT_rupd((!CPSR),BitsN.B(0x0,8)))
3645 val HSRValue = ref (BitsN.B(0x0,32))
3654 ; if ((BitsN.bits(5,4) ec) = (BitsN.B(0x0,2))) andalso
3655 (not((BitsN.bits(3,0) ec) = (BitsN.B(0x0,4))))
3686 val x0 = #HSR((!CP15) : CP15)
3688 CP15 := (CP15_HSR_rupd((!CP15),write'reg'HSR(x0,(!HSRValue))))
3700 val HSRString = ref (BitsN.B(0x0,25))
3707 else BitsN.B(0x0,16)))
3717 val HSRString = BitsN.@@(immediate,BitsN.B(0x0,9))
3723 if (BitsN.bits(4,3) SYSm) = (BitsN.B(0x0,2))
3829 if not(nonzero = ((R n) = (BitsN.B(0x0,32))))
3853 ; write'ITSTATE(BitsN.B(0x0,8))
3919 then BitsN.B(0x0,32)
3932 ; CPSR := (PSR_Z_rupd((!CPSR),result = (BitsN.B(0x0,32))))
3949 then BitsN.B(0x0,32)
3987 (true,(BitsN.B(0x0,4),(n,(imm32,carry)))))
4015 (true,(BitsN.B(0x0,4),(n,(m,(shift_t,shift_n))))));
4024 (setflags,(d,(BitsN.B(0x0,4),(m,(shift_t,shift_n))))));
4044 (BitsN.B(0xD,4),(setflags,(d,(BitsN.B(0x0,4),(n,(shift_t,m))))));
4056 val result = ref (BitsN.B(0x0,32))
4062 BitsN.B(0x0,_) =>
4115 ; CPSR := (PSR_Z_rupd((!CPSR),result = (BitsN.B(0x0,32))))
4137 ; CPSR := (PSR_Z_rupd((!CPSR),result = (BitsN.B(0x0,32))))
4161 if accumulate then BitsN.@@(rdhi,rdlo) else BitsN.B(0x0,64))
4167 ; CPSR := (PSR_Z_rupd((!CPSR),result = (BitsN.B(0x0,64))))
4296 val acc = if a = (BitsN.B(0xF,4)) then BitsN.B(0x0,32) else R a
4338 val acc = if a = (BitsN.B(0xF,4)) then BitsN.B(0x0,32) else R a
4365 BitsN.B(0x0,_) =>
4411 else BitsN.B(0x0,2))))
4423 else BitsN.B(0x0,2))))
4558 BitsN.B(0x0,_) =>
4600 else BitsN.B(0x0,2))))
4616 else BitsN.B(0x0,2))))
4751 val acc = if a = (BitsN.B(0xF,4)) then BitsN.B(0x0,32) else R a
4781 if (R m) = (BitsN.B(0x0,32))
4784 else ( write'R(BitsN.B(0x0,32),d); IncPC () )
4845 val acc = if n = (BitsN.B(0xF,4)) then BitsN.B(0x0,32) else R n
4856 val acc = if n = (BitsN.B(0xF,4)) then BitsN.B(0x0,32) else R n
4872 val acc = if n = (BitsN.B(0xF,4)) then BitsN.B(0x0,32) else R n
4961 (if n = (BitsN.B(0xF,4)) then BitsN.B(0x0,32) else R n)
5003 else BitsN.B(0x0,32),t)
5031 else BitsN.B(0x0,32),t)
5059 else BitsN.B(0x0,32),t)
5155 else BitsN.B(0x0,32),t)
5172 else BitsN.B(0x0,32),t)
5195 else BitsN.B(0x0,32),t)
5235 then write'R(BitsN.B(0x0,32),n)
5283 then write'R(BitsN.B(0x0,32),n)
5448 write'MemU 32 (BitsN.B(0x0,32),x)
5482 write'MemU_unpriv 32 (BitsN.B(0x0,32),x)
5560 write'MemU 16 (BitsN.B(0x0,16),x)
5589 write'MemU_unpriv 16 (BitsN.B(0x0,16),x)
5623 write'MemA 32 (BitsN.B(0x0,32),x)
5727 ; write'R(BitsN.B(0x0,32),d)
5746 ; write'R(BitsN.B(0x0,32),d)
5765 ; write'R(BitsN.B(0x0,32),d)
5788 ; write'R(BitsN.B(0x0,32),d)
5927 ; if (BitsN.bits(4,3) SYSm) = (BitsN.B(0x0,2))
5963 val targetmode = ref (BitsN.B(0x0,5))
6058 ; if (BitsN.bits(4,3) SYSm) = (BitsN.B(0x0,2))
6100 val targetmode = ref (BitsN.B(0x0,5))
6189 val HSRString = BitsN.B(0x0,25)
6315 BitsN.B(0x0,_) => IEEEReal.TO_NEAREST
6427 BitsN.resize_replicate 19 (BitsN.B(0x0,1),19)])
6432 BitsN.resize_replicate 48 (BitsN.B(0x0,1),48)];
6448 fun FPZero32 sign = BitsN.@@(sign,BitsN.B(0x0,31));
6450 fun FPZero64 sign = BitsN.@@(sign,BitsN.B(0x0,63));
6541 | NONE => FPZero64(BitsN.B(0x0,1))
6542 val x0 = #FPSCR((!FP) : FP)
6543 val w = reg'FPSCR x0
6549 (x0,
6556 | NONE => FPZero32(BitsN.B(0x0,1))
6557 val x0 = #FPSCR((!FP) : FP)
6558 val w = reg'FPSCR x0
6564 (x0,BitsN.bitFieldInsert(31,28) (w,FPCompare32(S d,op2)))))
6571 val x0 = #FPSCR((!FP) : FP)
6573 FP := (FP_FPSCR_rupd((!FP),write'reg'FPSCR(x0,R t)))
6752 val imm32 = BitsN.zeroExtend 32 (BitsN.@@(imm8,BitsN.B(0x0,2)))
6799 val imm32 = BitsN.zeroExtend 32 (BitsN.@@(imm8,BitsN.B(0x0,2)))
7067 (not((BitsN.bits(12,11) ireg) = (BitsN.B(0x0,2))))
7089 if (!undefined) then Undefined(BitsN.B(0x0,32)) else NoOperation;
7093 ; if ConditionPassed () then Undefined(BitsN.B(0x0,32)) else NoOperation
7168 | _ => Undefined(BitsN.B(0x0,32))
7194 | _ => Undefined(BitsN.B(0x0,32));
7230 (BitsN.fromBitstring([sz'0],1)) = (BitsN.B(0x0,1))
7284 (BitsN.fromBitstring([sz'0],1)) = (BitsN.B(0x0,1))
7333 val single_reg = (BitsN.fromBitstring([sz'0],1)) = (BitsN.B(0x0,1))
7340 8),BitsN.B(0x0,2)))
7396 BitsN.B(0x0,_) =>
7398 (dp_operation,(op2 = (BitsN.B(0x0,1)),(d,(n,m))))
7479 val add = (BitsN.fromBitstring([op'0],1)) = (BitsN.B(0x0,1))
7518 val add = (BitsN.fromBitstring([op'0],1)) = (BitsN.B(0x0,1))
7555 (BitsN.fromBitstring([sz'0],1)) = (BitsN.B(0x0,1))
7710 else (false,("",Undefined(BitsN.B(0x0,32))))
7742 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
7745 (BitsN.B(0x0,4)))
7758 else (false,("",Undefined(BitsN.B(0x0,32))))
7822 val unsigned = (BitsN.fromBitstring([op'0],1)) = (BitsN.B(0x0,1))
7859 val unsigned = (BitsN.fromBitstring([u'0],1)) = (BitsN.B(0x0,1))
7901 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
7902 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
7904 (BitsN.fromBitstring([sz'0],1)) = (BitsN.B(0x0,1))
7947 (BitsN.B(0x0,2))) andalso
7950 (BitsN.B(0x0,4)))
8078 (BitsN.B(0x0,3))) andalso
8081 (BitsN.B(0x0,4)))
8095 | _ => (false,("",Undefined(BitsN.B(0x0,32))));
8135 (BitsN.B(0x0,3))) andalso
8139 (BitsN.B(0x0,6))) andalso
8141 (BitsN.B(0x0,1))) andalso
8144 sb'3'0000'0],4)) = (BitsN.B(0x0,4)))))
8195 sb'0'0000000'0],7)) = (BitsN.B(0x0,7))
8198 then ( if ((not(mode = (BitsN.B(0x0,5)))) andalso
8199 (M = (BitsN.B(0x0,1)))) orelse
8201 ((BitsN.concat[A,I,F]) = (BitsN.B(0x0,3)))) orelse
8202 (((imod = (BitsN.B(0x0,2))) andalso
8203 (M = (BitsN.B(0x0,1)))) orelse
8379 4)) = (BitsN.B(0x0,4))) andalso
8461 4)) = (BitsN.B(0x0,4))))
8510 4)) = (BitsN.B(0x0,4))))
8611 ((R = (BitsN.B(0x0,1))) andalso (HaveDSPSupport ())))
8619 val is_pldw = R = (BitsN.B(0x0,1))
8674 ((R = (BitsN.B(0x0,1))) andalso (HaveDSPSupport ())))
8676 val is_pldw = R = (BitsN.B(0x0,1))
8735 4)) = (BitsN.B(0x0,4))) andalso
8741 (BitsN.B(0x0,3)))))
8800 (BitsN.B(0x0,4))) andalso
8808 (BitsN.B(0x0,8))))
8869 BitsN.B(0x0,1)])
8879 then Undefined(BitsN.B(0x0,32))
8881 ; Branch(BranchExchange(BitsN.B(0x0,4)))
8955 (BitsN.B(0x0,2))) andalso
8958 (BitsN.B(0x0,4)))
9014 (BitsN.B(0x0,2))) andalso
9015 (((BitsN.fromBitstring([sb'2'0'0],1)) = (BitsN.B(0x0,1))) andalso
9018 (BitsN.B(0x0,4)))))
9065 (BitsN.B(0x0,2)))
9121 (BitsN.B(0x0,2))) andalso
9122 ((BitsN.fromBitstring([sb'2'0'0],1)) = (BitsN.B(0x0,1))))
9126 ((mask = (BitsN.B(0x0,4))) orelse
9307 (BitsN.B(0x0,4))
9368 then Undefined(BitsN.B(0x0,32))
9445 (BitsN.B(0x0,12))
9589 (BitsN.B(0x0,4))
9695 (BitsN.B(0x0,4))
9755 Undefined(BitsN.B(0x0,32))
10104 (BitsN.B(0x0,4))
10164 ; Store(StoreExclusive(Rd,(Rt,(Rn,BitsN.B(0x0,32)))))
10210 ; Load(LoadExclusive(Rt,(Rn,BitsN.B(0x0,32))))
10530 (BitsN.B(0x0,4))
10586 (BitsN.B(0x0,4))
10591 (P = (BitsN.B(0x0,1))) orelse
10650 (BitsN.B(0x0,4))
10653 ((not(H = (BitsN.B(0x0,1)))) orelse
10668 val unsigned = S = (BitsN.B(0x0,1))
10715 (BitsN.B(0x0,4))
10718 (not(H = (BitsN.B(0x0,1)))) orelse
10722 (P = (BitsN.B(0x0,1))) orelse
10739 val unsigned = S = (BitsN.B(0x0,1))
10788 (BitsN.B(0x0,4))
10794 (P = (BitsN.B(0x0,1))) orelse
10800 (((P = (BitsN.B(0x0,1))) andalso
10865 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
10931 (P = (BitsN.B(0x0,1))) orelse
10935 (((P = (BitsN.B(0x0,1))) andalso
11005 ((not(H = (BitsN.B(0x0,1)))) orelse
11017 val unsigned = S = (BitsN.B(0x0,1))
11070 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
11073 (not(H = (BitsN.B(0x0,1)))) orelse
11083 val unsigned = S = (BitsN.B(0x0,1))
11136 (not(H = (BitsN.B(0x0,1)))) orelse
11140 (P = (BitsN.B(0x0,1))) orelse
11154 val unsigned = S = (BitsN.B(0x0,1))
11267 (P = (BitsN.B(0x0,1))) orelse
11378 (BitsN.B(0x0,4)))
11423 then ( if (mask = (BitsN.B(0x0,4))) orelse
11600 (P = (BitsN.B(0x0,1))) orelse
11726 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
11788 (P = (BitsN.B(0x0,1))) orelse
11919 (P = (BitsN.B(0x0,1))) orelse
12050 (P = (BitsN.B(0x0,1))) orelse
12175 (BitsN.@@(tb,BitsN.B(0x0,1)),
12276 BitsN.B(0x0,1)),
12369 (BitsN.B(0x0,2))
12384 ([rotate'1,rotate'0],2),BitsN.B(0x0,3)))
12424 (BitsN.B(0x0,2))
12439 ([rotate'1,rotate'0],2),BitsN.B(0x0,3)))
12479 (BitsN.B(0x0,2))
12494 ([rotate'1,rotate'0],2),BitsN.B(0x0,3)))
13079 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
13194 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
13377 BitsN.B(0x0,2)))
13419 BitsN.B(0x0,2)))
13689 BitsN.B(0x0,_) =>
13856 (setflags,(d,(n,BitsN.B(0x0,12))))))
14013 (BitsN.B(0x0,3))
14041 (BitsN.B(0x0,3))
14072 imm8'1,imm8'0],8),BitsN.B(0x0,2)))
14109 BitsN.B(0x0,_) =>
14204 BitsN.B(0x0,2)))
14291 BitsN.B(0x0,1)))
14336 imm8'1,imm8'0],8),BitsN.B(0x0,2)))
14439 BitsN.B(0x0,1)])
14523 [BitsN.B(0x0,1),BitsN.fromBitstring([M'0],1),
14524 BitsN.B(0x0,6),
14562 (BitsN.B(0x0,3)))
14590 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
14593 then ( if ((BitsN.concat[A,I,F]) = (BitsN.B(0x0,3))) orelse
14599 (BitsN.fromBitstring([im'0],1)) = (BitsN.B(0x0,1))
14626 BitsN.B(0x0,_) =>
14641 | _ => Undefined(BitsN.B(0x0,32))
14662 [BitsN.fromBitstring([P'0],1),BitsN.B(0x0,7),
14900 imm8'1,imm8'0],8),BitsN.B(0x0,1)))
14928 imm11'0],11),BitsN.B(0x0,1)))
14967 BitsN.B(0x0,_) =>
15038 handler'0],5),BitsN.B(0x0,5)))
15045 Undefined(BitsN.B(0x0,32))
15071 BitsN.B(0x0,5)))
15104 handler'0],5),BitsN.B(0x0,5)))
15129 BitsN.B(0x0,2)))
15193 BitsN.B(0x0,2)))
15230 BitsN.B(0x0,2)))
15299 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
15300 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
15306 [BitsN.B(0x0,1),BitsN.fromBitstring([M'0],1),
15307 BitsN.B(0x0,1),
15363 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
15364 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
15370 [BitsN.B(0x0,1),BitsN.fromBitstring([M'0],1),
15371 BitsN.B(0x0,1),
15429 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
15435 [P,M,BitsN.B(0x0,1),
15497 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
15503 [P,M,BitsN.B(0x0,1),
15577 (Set.mem(op',[BitsN.B(0x0,2),BitsN.B(0x3,2)])) andalso
15639 (Set.mem(op',[BitsN.B(0x0,2),BitsN.B(0x3,2)])) andalso
15697 imm8'1,imm8'0],8),BitsN.B(0x0,2)))
15738 imm8'1,imm8'0],8),BitsN.B(0x0,2)))
15849 (BitsN.B(0x0,4)))
15992 imm8'2,imm8'1,imm8'0],8),BitsN.B(0x0,2)))
16039 imm8'1,imm8'0],8),BitsN.B(0x0,2)))
16094 imm8'2,imm8'1,imm8'0],8),BitsN.B(0x0,2)))
16130 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
16140 (BitsN.B(0x0,_),(_,(BitsN.B(0xF,_),BitsN.B(0x1,_)))) =>
16148 (BitsN.B(0x0,2),(Rn,(Rm,(shift_t,shift_n)))))
16150 | (BitsN.B(0x0,_),_) =>
16160 (BitsN.B(0x0,4),
16176 ( if (typ = (BitsN.B(0x0,2))) andalso
16177 ((imm3 = (BitsN.B(0x0,3))) andalso
16178 (imm2 = (BitsN.B(0x0,2))))
16260 | (BitsN.B(0x6,_),(_,(_,BitsN.B(0x0,_)))) =>
16262 then Undefined(BitsN.B(0x0,32))
16369 | _ => Undefined(BitsN.B(0x0,32))
16409 (BitsN.B(0x0,_),(_,(BitsN.B(0xF,_),BitsN.B(0x1,_)))) =>
16415 (BitsN.B(0x0,2),(Rn,imm12)))
16417 | (BitsN.B(0x0,_),_) =>
16425 (BitsN.B(0x0,4),(setflags,(Rd,(Rn,imm12)))))
16544 | _ => Undefined(BitsN.B(0x0,32))
16711 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
16713 (BitsN.B(0x0,2)))
16761 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
16762 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
16780 (BitsN.fromBitstring([sh'0],1),BitsN.B(0x0,1)),
16817 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
16818 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
16873 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
16874 ((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1)))
16923 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
16925 (BitsN.B(0x0,2))) andalso
16928 (BitsN.B(0x0,4))))
16975 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
16977 (BitsN.B(0x0,2))) andalso
16980 sb'2'00000'0],5)) = (BitsN.B(0x0,5))))
16983 then ( if (mask = (BitsN.B(0x0,4))) orelse
17025 (((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1))) andalso
17026 ((BitsN.fromBitstring([sb'2'0'0],1)) = (BitsN.B(0x0,1))))
17069 (((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1))) andalso
17070 ((BitsN.fromBitstring([sb'2'0'0],1)) = (BitsN.B(0x0,1))))
17073 then ( if ((not(mode = (BitsN.B(0x0,5)))) andalso
17074 (M = (BitsN.B(0x0,1)))) orelse
17076 ((BitsN.concat[A,I,F]) = (BitsN.B(0x0,3)))) orelse
17133 (((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1))) andalso
17143 (J = (BitsN.B(0x0,1)))))
17186 (((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1))) andalso
17219 then Undefined(BitsN.B(0x0,32))
17222 ; Branch(BranchExchange(BitsN.B(0x0,4)))
17257 (((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1))) andalso
17264 ((imm8 = (BitsN.B(0x0,8))) andalso GOOD_MATCH)
17276 then Undefined(BitsN.B(0x0,32))
17311 ((BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))) andalso
17313 (BitsN.B(0x0,2))) andalso
17316 (BitsN.B(0x0,4))))
17371 (((BitsN.fromBitstring([sb'1'0'0],1)) = (BitsN.B(0x0,1))) andalso
17373 (BitsN.B(0x0,2))) andalso
17376 sb'3'00000'0],5)) = (BitsN.B(0x0,5)))))
17465 (BitsN.B(0x0,12))
17555 imm11'0],11),BitsN.B(0x0,1)])
17612 imm11'0],11),BitsN.B(0x0,1)])
17676 imm10L'1,imm10L'0],10),BitsN.B(0x0,2)])
17695 ; Branch(BranchExchange(BitsN.B(0x0,4)))
17719 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
17901 (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x0,1))
17993 (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x0,1))
18141 Undefined(BitsN.B(0x0,32))
18172 (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x0,1))
18242 (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x0,1))
18490 (BitsN.fromBitstring([S'0],1)) = (BitsN.B(0x0,1))
19011 (BitsN.fromBitstring([sb'0'0'0],1)) = (BitsN.B(0x0,1))
19027 BitsN.B(0x0,3)))
19031 BitsN.B(0x0,_) => Media(ExtendHalfword args)
19034 | BitsN.B(0x3,_) => Undefined(BitsN.B(0x0,32))
19072 BitsN.B(0x1,_) => BitsN.B(0x0,3)
19076 | BitsN.B(0x0,_) => BitsN.B(0x4,3)
19157 BitsN.B(0x0,_) => Media(ByteReverse(Rd,Rm))
19267 (BitsN.B(0x0,_),(BitsN.B(0xF,_),(false,false))) =>
19269 | (BitsN.B(0x0,_),(_,(false,false))) =>
19271 | (BitsN.B(0x0,_),(BitsN.B(0xF,_),(false,true))) =>
19273 ; Branch(BranchExchange(BitsN.B(0x0,4)))
19275 | (BitsN.B(0x0,_),(_,(false,true))) =>
19307 ; Branch(BranchExchange(BitsN.B(0x0,4)))
19315 | _ => Undefined(BitsN.B(0x0,32))
19405 (BitsN.B(0x0,1))
19437 | _ => Undefined(BitsN.B(0x0,32))
19456 val x0 = x
19457 val b3 = BitsN.bits(31,24) x0
19458 val b2 = BitsN.bits(23,16) x0
19459 val b1 = BitsN.bits(15,8) x0
19460 val b0 = BitsN.bits(7,0) x0
19462 case (b3 = (BitsN.B(0x0,8)),
19463 (b2 = (BitsN.B(0x0,8)),(b1 = (BitsN.B(0x0,8)),b0 = (BitsN.B(0x0,8))))) of
19464 (true,(true,(true,_))) => Option.SOME(BitsN.@@(BitsN.B(0x0,4),b0))
19489 if (BitsN.bits(31,8) x) = (BitsN.B(0x0,24))
19492 else if n = (BitsN.B(0x0,4))
19500 SRType_LSL => (BitsN.B(0x0,2),BitsN.fromNat(shift_n,5))
19503 if shift_n = 32 then BitsN.B(0x0,5) else BitsN.fromNat(shift_n,5))
19506 if shift_n = 32 then BitsN.B(0x0,5) else BitsN.fromNat(shift_n,5))
19508 | SRType_RRX => (BitsN.B(0x3,2),BitsN.B(0x0,5));
19512 SRType_LSL => BitsN.B(0x0,2)
19516 | SRType_RRX => BitsN.B(0x0,2);
19520 BitsN.B(0x0,_) => BitsN.B(0x1,3)
19528 then if ((BitsN.bits(18,0) imm64) = (BitsN.B(0x0,19))) andalso
19530 (BitsN.bits(29,25) imm64,[BitsN.B(0x0,5),BitsN.B(0x1F,5)])) andalso
19532 ((BitsN.bits(63,32) imm64) = (BitsN.B(0x0,32)))))
19538 else if ((BitsN.bits(47,0) imm64) = (BitsN.B(0x0,48))) andalso
19539 ((Set.mem(BitsN.bits(61,54) imm64,[BitsN.B(0x0,8),BitsN.B(0xFF,8)])) andalso
19614 [BitsN.B(0x2,2),J1,BitsN.B(0x0,1),J2,imm11])
19621 then Thumb(BitsN.concat[BitsN.B(0x8E,9),Rm,BitsN.B(0x0,3)])
19666 [BitsN.B(0x3,2),J1,BitsN.B(0x0,1),J2,imm10L,
19667 BitsN.B(0x0,1)])
19691 then Thumb(BitsN.concat[BitsN.B(0x8F,9),Rm,BitsN.B(0x0,3)])
19706 [BitsN.B(0xB,4),op',BitsN.B(0x0,1),i,BitsN.B(0x1,1),
19731 (((BitsN.bits(4,0) handler_offset) = (BitsN.B(0x0,5))) andalso
19743 (((BitsN.bits(4,0) handler_offset) = (BitsN.B(0x0,5))) andalso
19755 (((BitsN.bits(4,0) handler_offset) = (BitsN.B(0x0,5))) andalso
19784 BitsN.B(0x3,2),M,BitsN.B(0x0,1),Vm])
19807 BitsN.B(0x3,2),M,BitsN.B(0x0,1),Vm])
19820 BitsN.B(0x0,1),Vm])
19833 BitsN.B(0x1,1),M,BitsN.B(0x0,1),Vm])
19847 BitsN.B(0x0,4),BitsN.bits(3,0) v'0])
19860 BitsN.B(0x1,2),M,BitsN.B(0x0,1),Vm])
19902 BitsN.B(0x3,2),M,BitsN.B(0x0,1),Vm])
19914 BitsN.B(0x1,2),M,BitsN.B(0x0,1),Vm])
19926 BitsN.B(0x3,2),M,BitsN.B(0x0,1),Vm])
19940 BitsN.B(0x0,1),M,BitsN.B(0x0,1),Vm])
19954 BitsN.B(0x1,1),M,BitsN.B(0x0,1),Vm])
19968 BitsN.B(0x0,1),M,BitsN.B(0x0,1),Vm])
19980 [c,BitsN.B(0x1D,5),D,BitsN.B(0x0,2),Vn,Vd,
19982 BitsN.B(0x0,1),M,BitsN.B(0x0,1),Vm])
19996 | VFPNegMul_VNMLS => (BitsN.B(0x1,2),BitsN.B(0x0,1))
20000 BitsN.fromBit dp_operation,N,op2,M,BitsN.B(0x0,1),Vm])
20012 [c,BitsN.B(0x1C,5),D,BitsN.B(0x0,2),Vn,Vd,
20014 BitsN.fromBit(not add),M,BitsN.B(0x0,1),Vm])
20028 BitsN.fromBit(not add),M,BitsN.B(0x0,1),Vm])
20042 BitsN.fromBit(not add),M,BitsN.B(0x0,1),Vm])
20047 then if (not((BitsN.bits(1,0) imm32) = (BitsN.B(0x0,2)))) orelse
20048 (not((BitsN.bits(31,10) imm32) = (BitsN.B(0x0,22))))
20062 then if (not((BitsN.bits(1,0) imm32) = (BitsN.B(0x0,2)))) orelse
20063 (not((BitsN.bits(31,10) imm32) = (BitsN.B(0x0,22))))
20071 BitsN.B(0x0,2),n,Vd,BitsN.B(0x5,3),
20095 BitsN.fromBit wback,BitsN.B(0x0,1),n,Vd,
20120 [c,BitsN.B(0x6,5),H,BitsN.B(0x0,2),imm4,Rd,imm12])
20132 imm4],BitsN.concat[BitsN.B(0x0,1),imm3,Rd,imm8])
20144 [c,BitsN.B(0x7,5),N,BitsN.B(0x1,1),S,BitsN.B(0x0,4),
20147 else if ((BitsN.bits(11,8) imm12) = (BitsN.B(0x0,4))) andalso
20169 BitsN.concat[BitsN.B(0x0,1),imm3,Rd,imm8])
20182 [BitsN.B(0x1E,5),i,BitsN.B(0x1,1),BitsN.B(0x0,1),S,
20183 BitsN.B(0x0,1),S,BitsN.B(0x0,1),Rn],
20184 BitsN.concat[BitsN.B(0x0,1),imm3,Rd,imm8])
20190 [c,BitsN.B(0x6,5),op',BitsN.B(0x1,1),Rn,BitsN.B(0x0,4),
20193 (((BitsN.bits(11,8) imm12) = (BitsN.B(0x0,4))) andalso
20208 BitsN.B(0x0,_) => BitsN.B(0x0,4)
20216 [BitsN.B(0x1E,5),i,BitsN.B(0x0,1),opc,BitsN.B(0x1,1),
20218 BitsN.concat[BitsN.B(0x0,1),imm3,BitsN.B(0xF,4),imm8])
20231 (((BitsN.bits(11,3) imm12) = (BitsN.B(0x0,9))) andalso
20245 (((BitsN.bits(11,8) imm12) = (BitsN.B(0x0,4))) andalso
20256 ((imm12 = (BitsN.B(0x0,12))) andalso
20293 (((BitsN.bits(11,8) imm12) = (BitsN.B(0x0,4))) andalso
20310 BitsN.B(0x0,_) => BitsN.B(0x0,4)
20329 [BitsN.B(0x1E,5),i,BitsN.B(0x0,1),op',S,Rn],
20330 BitsN.concat[BitsN.B(0x0,1),imm3,Rd,imm8])
20343 [c,BitsN.B(0x0,3),opc,S,Rn,Rd,imm5,typ,
20344 BitsN.B(0x0,1),Rm])
20363 [BitsN.B(0x0,4),BitsN.B(0x1,4),BitsN.B(0x5,4),BitsN.B(0x6,4),
20399 BitsN.B(0x0,_) => BitsN.B(0x0,4)
20416 BitsN.concat[BitsN.B(0x0,1),imm3,Rd,imm2,typ,Rm])
20428 BitsN.B(0x0,4),imm5,typ,BitsN.B(0x0,1),Rm])
20460 BitsN.B(0x0,_) => BitsN.B(0x0,4)
20469 [BitsN.B(0x0,1),imm3,BitsN.B(0xF,4),imm2,typ,Rm])
20482 [c,BitsN.B(0x3,5),N,BitsN.B(0x1,1),S,BitsN.B(0x0,4),
20483 Rd,imm5,typ,BitsN.B(0x0,1),Rm])
20507 Thumb(BitsN.concat[BitsN.B(0x0,3),typ,imm5,Rm,Rd])
20535 BitsN.concat[BitsN.B(0x0,1),imm3,Rd,imm2,typ,Rm])
20551 [c,BitsN.B(0x0,3),opc,S,Rn,Rd,Rs,BitsN.B(0x0,1),typ,
20568 [c,BitsN.B(0x3,5),N,BitsN.B(0x1,1),S,BitsN.B(0x0,4),
20569 Rd,Rs,BitsN.B(0x0,1),typ,BitsN.B(0x1,1),Rm])
20586 | _ => BitsN.B(0x0,3)
20600 BitsN.concat[BitsN.B(0xF,4),Rd,BitsN.B(0x0,4),Rm])
20609 [c,BitsN.B(0x2,5),opc,BitsN.B(0x0,1),Rn,Rd,
20636 [BitsN.B(0x0,1),imm3,Rd,imm2,tb,BitsN.B(0x0,1),Rm])
20661 [BitsN.B(0xF3,8),U,BitsN.B(0x0,1),sh,BitsN.B(0x0,1),
20664 [BitsN.B(0x0,1),imm3,Rd,imm2,BitsN.B(0x0,1),sat_imm])
20683 BitsN.concat[BitsN.B(0x0,4),Rd,BitsN.B(0x0,4),sat_imm])
20748 (BitsN.concat[BitsN.B(0xB2,8),U,BitsN.B(0x0,1),Rm,Rd])
20770 [c,BitsN.B(0xD,5),U,BitsN.B(0x0,2),Rn,Rd,rotate,
20890 [BitsN.B(0x0,1),imm3,Rd,imm2,BitsN.B(0x0,1),widthm1])
20910 [BitsN.B(0x0,1),imm3,Rd,imm2,BitsN.B(0x0,1),msb])
21031 BitsN.B(0xF,4),imm5,typ,BitsN.B(0x0,1),Rm])
21098 imm5,typ,BitsN.B(0x0,1),Rm])
21133 | NONE => (BitsN.B(0x0,1),BitsN.B(0x0,5))
21144 [BitsN.B(0xF10,12),imod,M,BitsN.B(0x0,8),A,I,
21145 F,BitsN.B(0x0,1),mode])
21148 else if (not(e = Enc_Wide)) andalso (M = (BitsN.B(0x0,1)))
21156 (BitsN.concat[BitsN.B(0x5B3,11),im,BitsN.B(0x0,1),A,I,F])
21202 [c,BitsN.B(0x2,5),R,BitsN.B(0xF,6),Rd,BitsN.B(0x0,12)])
21206 BitsN.concat[BitsN.B(0x8,4),Rd,BitsN.B(0x0,8)])
21217 [c,BitsN.B(0x2,5),R,BitsN.B(0x0,2),m1,Rd,
21218 BitsN.B(0x1,3),m,BitsN.B(0x0,8)])
21223 [BitsN.B(0x8,4),Rd,BitsN.B(0x1,3),m,BitsN.B(0x0,4)])
21250 BitsN.concat[BitsN.B(0x8,4),mask,BitsN.B(0x0,8)])
21262 m,BitsN.B(0x0,4),Rn])
21267 [BitsN.B(0x8,4),m1,BitsN.B(0x1,3),m,BitsN.B(0x0,4)])
21281 [BitsN.B(0x7C,7),P,U,BitsN.B(0x0,1),W,
21288 [BitsN.B(0x74,7),U,U,BitsN.B(0x0,1),W,BitsN.B(0x1,1),Rn],
21316 [BitsN.B(0x74,7),U,U,BitsN.B(0x0,1),W,BitsN.B(0xD,5)],
21339 BitsN.B(0x0,9)])
21344 [BitsN.B(0xB65,12),BitsN.fromBit E,BitsN.B(0x0,3)])
21360 BitsN.concat[Ra,Rd,BitsN.B(0x0,4),Rm])
21370 [c,BitsN.B(0x0,7),S,Rd,BitsN.B(0x0,4),Rm,
21389 BitsN.concat[BitsN.B(0xF,4),Rd,BitsN.B(0x0,4),Rm])
21409 (BitsN.concat[BitsN.B(0x1F7,9),A,U,BitsN.B(0x0,1),Rn],
21410 BitsN.concat[Rdlo,Rdhi,BitsN.B(0x0,4),Rm])
21438 BitsN.B(0x0,1),Rn])
21442 BitsN.concat[Ra,Rd,BitsN.B(0x0,2),N,M,Rm])
21452 [c,BitsN.B(0x16,8),Rd,BitsN.B(0x0,4),Rm,
21453 BitsN.B(0x1,1),M,N,BitsN.B(0x0,1),Rn])
21457 BitsN.concat[BitsN.B(0xF,4),Rd,BitsN.B(0x0,2),N,M,Rm])
21467 BitsN.B(0x0,2),Rn])
21471 BitsN.concat[Ra,Rd,BitsN.B(0x0,3),M,Rm])
21480 [c,BitsN.B(0x12,8),Rd,BitsN.B(0x0,4),Rm,
21485 BitsN.concat[BitsN.B(0xF,4),Rd,BitsN.B(0x0,3),M,Rm])
21496 BitsN.B(0x0,1),Rn])
21512 [c,BitsN.B(0x70,8),Rd,Ra,Rm,BitsN.B(0x0,1),S,M,
21521 BitsN.concat[Ra,Rd,BitsN.B(0x0,3),M,Rm])
21532 [c,BitsN.B(0x74,8),Rdhi,Rdlo,Rm,BitsN.B(0x0,1),S,M,
21546 [c,BitsN.B(0x75,8),Rd,Ra,Rm,BitsN.B(0x0,2),R,
21551 BitsN.concat[Ra,Rd,BitsN.B(0x0,3),R,Rm])
21565 BitsN.concat[Ra,Rd,BitsN.B(0x0,3),R,Rm])
21582 BitsN.concat[BitsN.B(0xF,4),Rd,BitsN.B(0x0,4),Rm])
21668 val opc = if sub then BitsN.B(0x4,3) else BitsN.B(0x0,3)
21672 BitsN.concat[BitsN.B(0xF,4),Rd,BitsN.B(0x0,4),Rm])
21686 val opc = if sub then BitsN.B(0x4,3) else BitsN.B(0x0,3)
21704 val opc = if sub then BitsN.B(0x4,3) else BitsN.B(0x0,3)
21722 val opc = if sub then BitsN.B(0x4,3) else BitsN.B(0x0,3)
21740 val opc = if sub then BitsN.B(0x4,3) else BitsN.B(0x0,3)
21758 val opc = if sub then BitsN.B(0x4,3) else BitsN.B(0x0,3)
21772 BitsN.concat[Ra,Rd,BitsN.B(0x0,4),Rm])
21790 [c,BitsN.B(0x2,3),P,U,BitsN.B(0x0,1),W,
21857 [c,BitsN.B(0x3,3),P,U,BitsN.B(0x0,1),W,
21858 BitsN.B(0x1,1),Rn,Rt,imm5,typ,BitsN.B(0x0,1),Rm])
21882 BitsN.concat[Rt,BitsN.B(0x0,6),imm2,Rm])
21951 BitsN.B(0x0,1),Rm])
21979 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x1,1),W,
22045 BitsN.B(0x0,1),Rm])
22048 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x0,1),W,
22080 BitsN.concat[Rt,BitsN.B(0x0,6),imm2,Rm])
22150 BitsN.B(0x0,1),Rm])
22163 [c,BitsN.B(0x0,4),U,BitsN.B(0x7,3),Rn,Rt,imm4H,
22184 [c,BitsN.B(0x0,4),U,BitsN.B(0x3,3),Rn,Rt,
22204 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x1,1),W,
22268 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x0,1),W,
22299 BitsN.concat[Rt,BitsN.B(0x0,6),imm2,Rm])
22345 [c,BitsN.B(0x0,4),U,BitsN.B(0x7,3),Rn,Rt,imm4H,
22367 [c,BitsN.B(0x0,4),U,BitsN.B(0x3,3),Rn,Rt,
22380 [c,BitsN.B(0x4,3),P,U,BitsN.B(0x0,1),W,
22387 (((BitsN.bits(14,8) registers) = (BitsN.B(0x0,7))) andalso
22399 (((BitsN.bits(15,8) registers) = (BitsN.B(0x0,8))) andalso
22453 BitsN.B(0x0,1),registers])
22470 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x1,1),W,
22471 BitsN.B(0x0,1),Rn,Rt,imm4H,BitsN.B(0xD,4),
22496 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x0,1),W,
22497 BitsN.B(0x0,1),Rn,Rt,BitsN.B(0xD,8),Rm])
22529 then if imm32 = (BitsN.B(0x0,32))
22586 [c,BitsN.B(0x2,3),P,U,BitsN.B(0x0,1),W,
22587 BitsN.B(0x0,1),Rn,Rt,imm12])
22653 [c,BitsN.B(0x3,3),P,U,BitsN.B(0x0,1),W,
22654 BitsN.B(0x0,1),Rn,Rt,imm5,typ,BitsN.B(0x0,1),Rm])
22678 BitsN.concat[Rt,BitsN.B(0x0,6),imm2,Rm])
22713 BitsN.B(0x0,1),Rm])
22730 BitsN.B(0x0,1),Rn,Rt,imm12])
22786 BitsN.B(0x0,1),Rn,Rt,imm5,typ,BitsN.B(0x0,1),Rm])
22810 BitsN.concat[Rt,BitsN.B(0x0,6),imm2,Rm])
22846 BitsN.B(0x0,1),Rm])
22863 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x1,1),W,
22864 BitsN.B(0x0,1),Rn,Rt,imm4H,BitsN.B(0xB,4),
22919 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x0,1),W,
22920 BitsN.B(0x0,1),Rn,Rt,BitsN.B(0xB,8),Rm])
22946 BitsN.concat[Rt,BitsN.B(0x0,6),imm2,Rm])
22963 [c,BitsN.B(0x0,4),U,BitsN.B(0x6,3),Rn,Rt,imm4H,
22983 [c,BitsN.B(0x0,4),U,BitsN.B(0x2,3),Rn,Rt,
22996 [c,BitsN.B(0x4,3),P,U,BitsN.B(0x0,1),W,
22997 BitsN.B(0x0,1),Rn,registers])
23004 (((BitsN.bits(13,8) registers) = (BitsN.B(0x0,6))) andalso
23016 (((BitsN.bits(15,8) registers) = (BitsN.B(0x0,8))) andalso
23033 [BitsN.B(0x74,7),P,U,BitsN.B(0x0,1),W,BitsN.B(0x0,1),
23063 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x1,1),W,
23064 BitsN.B(0x0,1),Rn,Rt,imm4H,BitsN.B(0xF,4),
23076 [BitsN.B(0x74,7),P,U,BitsN.B(0x1,1),W,BitsN.B(0x0,1),
23089 [c,BitsN.B(0x0,3),P,U,BitsN.B(0x0,1),W,
23090 BitsN.B(0x0,1),Rn,Rt,BitsN.B(0xF,8),Rm])
23095 then if imm32 = (BitsN.B(0x0,32))
23176 [c,BitsN.B(0x2,5),B,BitsN.B(0x0,2),Rn,Rt,
23190 ((BitsN.bits(31,8) imm32) = (BitsN.B(0x0,24)))
23215 BitsN.B(0x0,_) => CPSR := (PSR_Z_rupd((!CPSR),true))
23376 | NONE => Option.SOME("immediate not encodable",BitsN.B(0x0,12)))
23378 Option.SOME("immediate too large",BitsN.B(0x0,12))
23385 Option.SOME("FP immediate too large",BitsN.B(0x0,64))
23390 Option.SOME("FP too large",BitsN.B(0x0,64))
23424 "eq" => Option.SOME(BitsN.B(0x0,4))
23469 "r0" => Option.SOME(BitsN.B(0x0,4))
23596 ((BitsN.&&(w,mask)) = (BitsN.B(0x0,16)))
23627 (BitsN.B(0x0,16),if r = "" then t else r :: t)
23656 ((BitsN.&&(w,mask)) = (BitsN.B(0x0,32)))
23679 if imm32 = (BitsN.B(0x0,32))
23705 case p_fp_registers_loop(true,(BitsN.B(0x0,32),l)) of
23708 (case p_fp_registers_loop(false,(BitsN.B(0x0,32),l)) of
23824 (true,(BitsN.B(0x0,4),(rn,(rm,(typ,rs))))))))
23925 (d,(BitsN.B(0xF,4),BitsN.B(0x0,12))))))))
23950 (InstrSet_ARM,BitsN.B(0x0,32)))))
23963 PENDING(label,(c,Branch(BranchTarget(BitsN.B(0x0,32)))))
23987 (InstrSet_Thumb,BitsN.B(0x0,32)))))
24523 (rn,immediate_form1(BitsN.B(0x0,32)))))))
24654 immediate_form1(BitsN.B(0x0,32))))))))))
24694 (unsigned,(false,(rt,BitsN.B(0x0,32))))
24746 immediate_form2(BitsN.B(0x0,32)))))))))))
24794 | PENDING(s,(c,Load(LoadLiteral(false,(_,BitsN.B(0x0,32)))))) =>
24795 PENDING(s,(c,Hint(PreloadDataLiteral(false,BitsN.B(0x0,32)))))
24815 OK(c,Load(LoadExclusive(rt,(rn,BitsN.B(0x0,32)))))
24849 OK(c,Store(StoreExclusive(rd,(rt,(rn,BitsN.B(0x0,32))))))
25054 (BitsN.@@(BitsN.B(0x0,2),BitsN.fromNat(BitsN.toNat i,3)))
25176 (case p_cxsf(BitsN.B(0x0,4),String.implode r) of
25180 (case p_cxsf(BitsN.B(0x0,4),String.implode r) of
25551 (d,(BitsN.B(0xF,4),BitsN.B(0x0,32)))))
25598 p_arith_logic(String.implode c,(BitsN.B(0x0,4),(true,l)))
25600 p_arith_logic(String.implode c,(BitsN.B(0x0,4),(false,l)))
25638 p_test_compare(String.implode c,(BitsN.B(0x0,2),l))
25775 p_sadd16_etc(String.implode c,(BitsN.B(0x0,2),l))
25783 p_qadd16_etc(String.implode c,(BitsN.B(0x0,2),l))
25792 p_shadd16_etc(String.implode c,(BitsN.B(0x0,2),l))
25813 p_uadd16_etc(String.implode c,(BitsN.B(0x0,2),l))
25822 p_uqadd16_etc(String.implode c,(BitsN.B(0x0,2),l))
25832 p_uhadd16_etc(String.implode c,(BitsN.B(0x0,2),l))
25857 p_qadd_etc(String.implode c,(BitsN.B(0x0,2),l))
26157 BitsN.B(0x0,_) => "eq"
26231 ([],(Nat.-(BitsN.size(BitsN.BV(0x0,N)),1),BitsN.toBitstring l))))) of
26249 if BitsN.<(imm32,BitsN.B(0x0,32))
26255 if add andalso (imm32 = (BitsN.B(0x0,32)))
26395 if add andalso (imm32 = (BitsN.B(0x0,32)))
26402 if add andalso (imm32 = (BitsN.B(0x0,32)))
26464 BitsN.B(0x0,_) => "tst"
26472 BitsN.B(0x0,_) => "and"
26881 BitsN.B(0x0,_) => "add16"
26928 BitsN.B(0x0,_) => "qadd"