Searched refs:bits (Results 51 - 75 of 165) sorted by relevance

1234567

/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dio.tex153 PCI identifier of the device as the low 16 bits of the \texttt{badge} argument, and
154 a Domain ID as the high 16 bits of the \texttt{badge} argument.
157 a 16-bit quantity. The first 8 bits identify the bus that the device is on.
158 The next 5 bits are the device identifier: the number of the device on
159 the bus. The last 3 bits are the function number. A single device may
H A Dvspace.tex40 The size and type of structure at each level, and the number of bits in the virtual address resolved
65 Structures at both levels are indexed by 10 bits in the virtual address.
77 defined, as shown in the table below. All structures are indexed with 9 bits of the virtual
108 \texttt{PageGlobalDirectory}. All paging structures are index by 9 bits of the virtual address.
126 32-bit RISC-V \texttt{PageTables} are indexed by 10 bits of virtual address.
137 64-bit RISC-V follows the SV39 model, where \texttt{PageTables} are indexed by 9 bits of virtual address.
H A Dipc.tex69 \ipcparam{seL4\_Word}{}{receiveDepth}{Number of bits of
132 Only the low 28 bits of the badge are available for use. The kernel will
133 silently ignore any usage of the high 4 bits.
151 These fields specify the root CNode, capability address and number of bits to resolve, respectively, to find
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/
H A Darm8.sml918 tcr_el1'rst = BitsN.@@(BitsN.bits(36,0) x,BitsN.bits(63,39) x)};
924 [BitsN.bits(24,0) tcr_el1'rst,BitsN.fromBit TBI1,
925 BitsN.fromBit TBI0,BitsN.bits(61,25) tcr_el1'rst];
933 tcr_el2_el3'rst = BitsN.@@(BitsN.bits(19,0) x,BitsN.bits(31,21) x)};
939 [BitsN.bits(10,0) tcr_el2_el3'rst,BitsN.fromBit TBI,
940 BitsN.bits(30,11) tcr_el2_el3'rst];
951 [BitsN.bits(0,0) x,BitsN.bits(
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/
H A DBitstring.sml158 fun bits (h, l) = function
167 fun bit (a, n) = bits (n, n) a = [true]
H A DBitsN.sml61 else raise Fail ("Tried to resize bits(" ^ Nat.toString j ^
62 ") to bits(" ^ Int.toString i ^ ")")
76 fun bits (h, l) = function
H A DBitsN.sig69 val bits: Nat.nat * Nat.nat -> nbit -> nbit value
H A DFP64.sml21 val byte = Word8.fromLargeInt o BitsN.toNat o L3.uncurry BitsN.bits
/seL4-l4v-10.1.1/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-10.1.1/HOL4/examples/hardware/hol88/mos-count/
H A Ddataabs.ml5 % logic to boolean logic for single bits and for %
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/
H A Dm0AssemblerLib.sml17 fun hex32 w = hex (BitsN.bits (31, 16) w) ^ " " ^ hex (BitsN.bits (15, 0) w)
195 if BitsN.toNat (BitsN.bits (15, 12) opc) = 13
197 val code = BitsN.bits (11, 8) opc
/seL4-l4v-10.1.1/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-10.1.1/HOL4/polyml/basis/
H A DWord8.sml33 that the top 22/23 bits are always zero and mask them after every
35 we could allow these bits to be undefined and mask them before any
53 (* Not the same as Word.notb because it only affects the bottom 8 bits. *)
H A DInt32.sml28 open LargeInt (* We need LargeInt on 32-bits. *)
H A DASN1.sml102 (* The type is encoded in the top two bits of the first byte. *)
112 (* The tag is the bottom five bits except that if it is 0x1f
/seL4-l4v-10.1.1/graph-refine/
H A Dlogic.py370 def split_out_cast (expr, target_typ, bits):
373 have the property that expr' && mask bits = cast expr,
375 bottom n bits, e.g. (1 << n) - 1, and cast is WordCast."""
378 if x.typ.num >= bits and expr.typ.num >= bits:
379 return split_out_cast (x, target_typ, bits)
388 full_mask = (1 << bits) - 1
390 return split_out_cast (x, target_typ, bits)
395 # at a smaller number of bits than we'll eventually report
396 if expr.typ.num >= bits
[all...]
H A Dpseudo_compile.py434 bits = s.split ('.')
435 if len (bits) != 2:
437 if all ([x in '0123456789' for x in bits[1]]):
438 return bits[0]
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DBase.sml302 (* Int should be 32-bits on Windows. *)
304 orelse raise Fail "unsigned int is not 32-bits"
307 orelse raise Fail "unsigned long is not 32-bits"
561 able to handle multiple bits. Patterns with more than one bit set
562 MUST be placed later than those with a subset of those bits. *)
574 bit entries preceded those with fewer bits but it's much easier to lay
583 | fromInt [] (SOME(res, bits)) x = (* Found something - remove it from the set. *)
584 (res :: fromInt table NONE (andb(x, notb bits)))
586 | fromInt ((res, bits)::tl) sofar x =
587 if bits <>
[all...]
H A DMenu.sml334 (* The options are the other bits in the type field. *)
350 val (bits, typeData, cch, bmp) = value
357 val mtype = Word32.orb(fromMFT menuOptions, bits)
371 val (bits, typeData, cch, bmp) = value
378 val mtype = Word32.orb(fromMFT menuOptions, bits)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/
H A DarmAssemblerLib.sml231 val c = BitsN.bits (31, 28) w
350 (BitsN.bits (3, 2) opc = BitsN.fromNat (2, 2) orelse d = d')
359 val c = BitsN.bits (31, 28) w
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/tamarack2/
H A Ddiv.ml4 % The following bits are needed to make this proof run in HOL88. %
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/
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-10.1.1/seL4/include/arch/x86/arch/
H A Dmachine.h295 static inline void clearMemory(void* ptr, unsigned int bits) argument
297 memzero(ptr, BIT(bits));
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DMD5.sml121 val bits = packLittle [lo,hi] value
125 val {digest= {A,B,C,D},...} = update (state,bits)
/seL4-l4v-10.1.1/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. *)

Completed in 211 milliseconds

1234567