Searched refs:bits (Results 1 - 25 of 170) sorted by path

1234567

/seL4-l4v-master/HOL4/Manual/Description/
H A DHolBdd.tex876 Encoding is done with the least significant bits first in the BDD ordering. For example, if variables
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A DHolBdd.tex876 Encoding is done with the least significant bits first in the BDD ordering. For example, if variables
H A Dtheories.tex2461 \holtxt{word\_slice} & \holtxt{''} & \num\rarr\num\rarr\worda\rarr\worda & Set bits outside field to zero \\
/seL4-l4v-master/HOL4/examples/ARM/v4/
H A Darm_evalLib.sml651 fun bits h l n = (n mod pow(two,plus1 h)) div (pow(two,l)) function
655 map (fn (i,j) => num2byte (bits (fromInt i) (fromInt j) w))
H A DassemblerML.sml68 fun bits h l (n:bool list) = List.take(List.drop(n,l),h + 1 - l); function
69 fun bit b n = (bits b b n = [true]);
149 val Rn = list2register o bits 19 16;
150 val Rd = list2register o bits 15 12;
151 val Rs = list2register o bits 11 8;
152 val Rm = list2register o bits 3 0;
165 mk_immediate (list2int (bits 11 8 l)) (list2num (bits 7 0 l))
169 let val imm = list2int (bits 11 7 l) in
170 {Rm = Rm l, Imm = imm, Sh = list2shift (bits
[all...]
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Darm_opsemScript.sml2964 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields>
2965 <bits> is nzcvq, g, or nzcvqg
2982 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields>
2983 <bits> is nzcvq, g, or nzcvqg
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Demit_eval.sml280 | armML.DataProcessing (armML.Reverse_Bits _) => "reverse bits"
/seL4-l4v-master/HOL4/examples/ARM_security_properties/model/
H A Darm_opsemScript.sml2988 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields>
2989 <bits> is nzcvq, g, or nzcvqg
3006 where <spec_reg> is APSR_<bits>, CPSR_<fields> or SPSR_<fields>
3007 <bits> is nzcvq, g, or nzcvqg
/seL4-l4v-master/HOL4/examples/Crypto/MARS/
H A DMARS_keyExpansionScript.sml142 (* Record the two lowest bits of K[i], by setting j = K[i] & 3, and then
143 consider the word with these two bits set to 1, w = K[i] | 3 *)
/seL4-l4v-master/HOL4/examples/Crypto/Serpent/Reference/
H A DSerpent_Reference_TransformationScript.sml560 (* compute the parity on select bits *)
/seL4-l4v-master/HOL4/examples/Crypto/TEA/
H A DteaScript.sml6 (* causes all bits of the key and data to be mixed repeatedly.The number of *)
9 (* authors suggest 32. The key is set at 128 bits. *)
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/
H A DtwofishScript.sml5 up to 256 bits. The cipher is a 16-round Feistel network with a
290 (* argument, with an extra rotate over 8 bits. The values Ai and Bi are *)
291 (* combined in a PHT. One of the results is further rotated by 9 bits. *)
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DbddTools.sml38 (* and it would be inefficient to unwind the higher order bits *)
/seL4-l4v-master/HOL4/examples/HolCheck/examples/
H A Dalu.sml25 val aw = 1; (* address space width in bits *)
26 val d = 1; (* datapath width in bits *)
49 (* where the address space is wsize bits wide *)
58 (* generates bitwise conjunction of equality tests for registers r1 and r2, each w bits wide *)
91 (* width d, and with an address space of aw bits. The ctl_wff's are CTL formulae expressing the *)
H A Damba_ahbScript.sml402 (* decoder, decodes higher order address bits to figure out which slave is being targeted *)
H A Damba_apbScript.sml16 (* note: psel_x is a family signals, where x identifies the slave, so the x is not bits e.g. psel_2 is a valid signal *)
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A Dhol_defaxiomsScript.sml3498 |- signed_byte_p bits x =
3500 [integerp bits; less (nat 0) bits;
3501 integer_range_p (unary_minus (expt (nat 2) (add (int ~1) bits)))
3502 (expt (nat 2) (add (int ~1) bits)) x],
3507 |- unsigned_byte_p bits x =
3509 [integerp bits; not (less bits (nat 0));
3510 integer_range_p (nat 0) (expt (nat 2) bits) x],
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dhol_defaxiomsScript.sml3460 |- signed_byte_p bits x =
3462 [integerp bits; less (nat 0) bits;
3463 integer_range_p (unary_minus (expt (nat 2) (add (int ~1) bits)))
3464 (expt (nat 2) (add (int ~1) bits)) x],
3469 |- unsigned_byte_p bits x =
3471 [integerp bits; not (less bits (nat 0));
3472 integer_range_p (nat 0) (expt (nat 2) bits) x],
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dhol_defaxiomsScript.sml3456 |- signed_byte_p bits x =
3458 [integerp bits; less (nat 0) bits;
3459 integer_range_p (unary_minus (expt (nat 2) (add (int ~1) bits)))
3460 (expt (nat 2) (add (int ~1) bits)) x],
3465 |- unsigned_byte_p bits x =
3467 [integerp bits; not (less bits (nat 0));
3468 integer_range_p (nat 0) (expt (nat 2) bits) x],
H A DsignedintScript.sml297 (* extend r l : Sign extend an integer i to fit in l bits *)
/seL4-l4v-master/HOL4/examples/dev/AES/curried/
H A Dword8Script.sml11 (* 8 bits per byte, represented as an 8-tuple of truth values. *)
26 (* variables, or as 256 tuples of bits. The former is useful for symbolic *)
197 Compare bits and bytes as if they were numbers. Not currently used
/seL4-l4v-master/HOL4/examples/dev/AES/tupled/
H A Dword8Script.sml11 (* 8 bits per byte, represented as an 8-tuple of truth values. *)
23 (* variables, or as 256 tuples of bits. The former is useful for symbolic *)
173 Compare bits and bytes as if they were numbers. Not currently used
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DpreARMScript.sml28 (* CPSR, In user programs only the top 4 bits of the CPSR are relevant *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DpreARMScript.sml25 (* CPSR, In user programs only the top 4 bits of the CPSR are relevant *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DpreARMScript.sml24 (* CPSR, In user programs only the top 4 bits of the CPSR are relevant *)

Completed in 269 milliseconds

1234567