Searched refs:rd (Results 1 - 25 of 57) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/
H A Driscv.spec1244 -- new value for rd for ALU ops, LOAD, LOAD_FP, LR, SC, CSR ops
1604 inline unit writeRD(rd::reg, val::regType) =
1605 { GPR(rd) <- val
1623 unit writeFPRS(rd::reg, val::word) =
1624 { FPRS(rd) <- val
1630 unit writeFPRD(rd::reg, val::regType) =
1631 { FPRD(rd) <- val
2023 -- ADDI rd, rs1, imm
2025 define ArithI > ADDI(rd::reg, rs1::reg, imm::imm12) =
2026 writeRD(rd, GP
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_opsemScript.sml44 reg_update ii rd f s1 s2 =
45 seqT (parT s1 s2) (\(x,y). write_reg ii (PPC_IR rd) (f x y))`;
48 uint_reg_update ii rd f s1 s2 =
50 (\(x,y). parT_unit (write_reg ii (PPC_IR rd) (f x y)) (ppc_uint_cmp ii (f x y) 0w))`;
53 sint_reg_update ii rd f s1 s2 =
55 (\(x,y). parT_unit (write_reg ii (PPC_IR rd) (f x y)) (ppc_sint_cmp ii (f x y) 0w))`;
82 read_ireg ii rd = read_reg ii (PPC_IR rd)`;
114 reg_store ii size rd s1 s2 =
115 seqT (parT (effective_address s1 s2) (read_ireg ii rd))
[all...]
H A Dppc_seq_monadScript.sml18 val PREAD_R_def = Define `PREAD_R rd ((r,s,m):ppc_state) = r rd`;
19 val PREAD_S_def = Define `PREAD_S rd ((r,s,m):ppc_state) = s rd`;
20 val PREAD_M_def = Define `PREAD_M rd ((r,s,m):ppc_state) = m rd`;
22 val PWRITE_R_def = Define `PWRITE_R rd x (r,s,m) = ((rd =+ x) r,s,m):ppc_state`;
23 val PWRITE_S_def = Define `PWRITE_S rd x (r,s,m) = (r,(rd
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/
H A Driscv.sml3754 fun writeFPRS (rd,val') =
3755 ( write'FPRS(val',rd)
3777 fun writeFPRD (rd,val') =
3778 ( write'FPRD(val',rd)
4400 fun dfn'ADDI (rd,(rs1,imm)) =
4401 ( write'GPR(BitsN.+(GPR rs1,BitsN.signExtend 64 imm),rd)
4411 fun dfn'ADDIW (rd,(rs1,imm)) =
4417 ( write'GPR(BitsN.signExtend 64 (BitsN.bits(31,0) temp),rd)
4430 fun dfn'SLTI (rd,(rs1,imm)) =
4438 (BitsN.fromBool 64 (BitsN.<(v1,BitsN.signExtend 64 imm)),rd)
[all...]
H A DriscvScript.sml4164 ("writeFPRS",TP[Var("rd",FTy 5),Var("val",F32)],
4172 TP[Var("val",F32),Var("rd",FTy 5)]),qVar"state"),
4222 ("writeFPRD",TP[Var("rd",FTy 5),Var("val",F64)],
4230 TP[Var("val",F64),Var("rd",FTy 5)]),qVar"state"),
5652 ("dfn'ADDI",TP[Var("rd",FTy 5),Var("rs1",FTy 5),Var("imm",FTy 12)],
5662 Var("rd",FTy 5)]),qVar"state")))
5665 ("dfn'ADDIW",TP[Var("rd",FTy 5),Var("rs1",FTy 5),Var("imm",FTy 12)],
5685 LN 0,F32)),Var("rd",FTy 5)]),qVar"s")))))
5688 ("dfn'SLTI",TP[Var("rd",FTy 5),Var("rs1",FTy 5),Var("imm",FTy 12)],
5709 Var("rd",FT
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/
H A Dfloat3.c27 double rd; local
50 ffi_call(&cif, FFI_FN(floating_1), &rd, values);
52 CHECK(rd - floating_1(f, d, ld) < DBL_EPSILON);
67 ffi_call(&cif, FFI_FN(floating_2), &rd, values);
69 CHECK(rd - floating_2(ld, d, f) < DBL_EPSILON);
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A Darm_evalScript.sml544 `!cond op s rd rn Op2. ~(op ' 3) \/ (op ' 2) ==>
545 (DECODE_ARM (data_proc_encode cond op s rn rd Op2) = data_proc)`,
550 `!cond op s rd rn Op2.
551 (DECODE_ARM (data_proc_encode cond op T rd 0w Op2) = data_proc)`,
561 (!cond s rd rn Op2. DECODE_ARM (enc (f cond s rd rn Op2)) = data_proc)`,
574 (!cond s rd Op2. DECODE_ARM (enc (f cond s rd Op2)) = data_proc)`,
580 `(!cond s rd rm rs.
581 DECODE_ARM (enc (instruction$MUL cond s rd r
[all...]
H A DinstructionSyntax.sml126 ``rd:word4`` |-> mk_register (#Rd y),
128 ``(f (c:condition) (s:bool) (rd:word4)
135 ``rd:word4`` |-> mk_register (#Rd y),
138 ``(f (c:condition) (s:bool) (rd:word4) (rn:word4)
150 ``rd:word4`` |-> mk_register (#Rd y),
155 (false,_,false) => ``MUL c s rd rm rs``
156 | (false,_,true) => ``MLA c s rd rm rs rn``
157 | (true,false,false) => ``UMULL c s rn rd rm rs``
158 | (true,false,true) => ``UMLAL c s rn rd rm rs``
159 | (true,true,false) => ``SMULL c s rn rd r
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/model/
H A Dmips.sml3290 fun dfn'MOVF (rd,(rs,cc)) =
3294 then write'GPR(GPR rs,rd)
3337 fun dfn'MOVT (rd,(rs,cc)) =
3341 then write'GPR(GPR rs,rd)
3796 fun dfn'ADD (rs,(rt,rd)) =
3806 else write'GPR(BitsN.signExtend 64 (BitsN.bits(31,0) temp),rd)
3810 fun dfn'ADDU (rs,(rt,rd)) =
3818 write'GPR(BitsN.signExtend 64 temp,rd)
3822 fun dfn'SUB (rs,(rt,rd)) =
3832 else write'GPR(BitsN.signExtend 64 (BitsN.bits(31,0) temp),rd)
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_parserLib.sml1358 fun add_sub_literal m (rd,i) =
1364 val narrow_okay = q <> Wide andalso narrow_register rd andalso
1379 mk_Add_Sub (mk_bool add,mk_word4 15,rd,imm12)))
1385 mk_Add_Sub (mk_bool (opc = mk_word4 4),mk_word4 15,rd,imm12))
1389 fun narrow_okay_imm m i (rd,rn) =
1394 if is_SP rd then
1397 narrow_register rd andalso ~1020 <= v andalso v <= 1020 andalso
1401 if rd = rn then
1406 m = RSB andalso v = 0 andalso narrow_registers [rd,rn]
1410 (rd,r
1564 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn) value
1574 val (rd,rn) = if m = MOV orelse m = MVN then (rdn,r0) else (r0,rdn) value
1598 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn) value
1607 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r0) else (r0,rdn) value
[all...]
H A Darm_decoderScript.sml30 ``\opc setflags rn rd mode1.
31 DataProcessing (Data_Processing opc setflags rn rd mode1)``);
446 (let rd = (3 :+ b7) (r 0) in
448 (rd = 15w) /\ InITBlock /\ ~LastInITBlock
452 DP 0b1101w F 0w rd (REG 0w 0w (r4 3)))
723 let S = a 4 and rn = ra 0 and rd = rb 8 value
727 (if rd = 15w then
733 DP 0b0000w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)))
735 DP 0b1110w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))
737 DP (if rn = 15w then 0b1101w else 0b1100w) S rn rd
837 let S = a 4 and rn = ra 0 and rd = rb 8 value
[all...]
/seL4-l4v-10.1.1/HOL4/src/real/
H A DisqrtLib.sml32 (SOME rn, SOME rd) =>
37 val SOME rd = sqrt d
42 val ry = mk_ge_thm rd
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/step/
H A Dmips_stepLib.sml174 [[``rd <> 0w: word5``, ``rs <> 0w: word5``, ``rt <> 0w: word5``,
176 (all_comb [`rt` |-> r0, `rs` |-> r0, `rd` |-> r0])
184 [[``rd <> 0w: word5``, ``rs <> 0w: word5``, ``rt <> 0w: word5``,
186 (all_comb [`rt` |-> r0, `rs` |-> r0, `rd` |-> r0])
192 [[``rd <> 0w: word5``, ``rt <> 0w: word5``,
194 (all_comb [`rt` |-> r0, `rd` |-> r0])
199 [[``rd <> 0w: word5``, ``^st.hi = SOME vHI``, ``^st.lo = SOME vLO``]]
200 [[], [`rd` |-> r0]]
288 val ADD = pEV ``dfn'ADD (rs, rt, rd)``
289 val SUB = pEV ``dfn'SUB (rs, rt, rd)``
[all...]
/seL4-l4v-10.1.1/isabelle/lib/browser/GraphBrowser/
H A DGraphBrowser.java58 Reader rd;
63 rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
65 rd = new FileReader(path + fname);
67 br = new BufferedReader(rd);
/seL4-l4v-10.1.1/l4v/isabelle/lib/browser/GraphBrowser/
H A DGraphBrowser.java58 Reader rd;
63 rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
65 rd = new FileReader(path + fname);
67 br = new BufferedReader(rd);
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/
H A Darm_decoderScript.sml30 ``\opc setflags rn rd mode1.
31 DataProcessing (Data_Processing opc setflags rn rd mode1)``);
446 (let rd = (3 :+ b7) (r 0) in
448 (rd = 15w) /\ InITBlock /\ ~LastInITBlock
452 DP 0b1101w F 0w rd (REG 0w 0w (r4 3)))
723 let S = a 4 and rn = ra 0 and rd = rb 8 value
727 (if rd = 15w then
733 DP 0b0000w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)))
735 DP 0b1110w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))
737 DP (if rn = 15w then 0b1101w else 0b1100w) S rn rd
837 let S = a 4 and rn = ra 0 and rd = rb 8 value
[all...]
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DRJBConv.sml14 (* DATE : 3rd February 1993 *)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A Dcodegen_armLib.sml93 val rd = "r" ^ int_to_string i value
96 val code = ["cmp " ^ rd ^ ", " ^ f j]
104 val rd = "r" ^ int_to_string i value
107 val code = ["tst " ^ rd ^ ", " ^ f j]
H A Dcodegen_x64Lib.sml107 val rd = x64_reg i value
110 val code = ["cmp " ^ rd ^ ", " ^ f j]
118 val rd = x64_reg i value
121 val code = ["test " ^ rd ^ ", " ^ f j]
H A Dcodegen_x86Lib.sml114 val rd = x86_reg i value
117 val code = ["cmp " ^ rd ^ ", " ^ f j]
125 val rd = x86_reg i value
128 val code = ["test " ^ rd ^ ", " ^ f j]
/seL4-l4v-10.1.1/HOL4/examples/dev/booth/
H A DboothScript.sml24 (* mul,mul2,borrow2,mshift,rm,rd *)
54 let rd = if a then alub else 0w
59 BOOTH mul mul2 borrow2 mshift rm rd`;
64 NEXT (BOOTH mul mul2 borrow2 mshift rm rd) =
67 and alua = rd
70 let rd' = ALU borrow2 mul alua alub
76 BOOTH mul' mul2' borrow2' mshift' rm rd'`;
102 PROJ_RD (BOOTH mul mul2 borrow2 mshift rm rd) = rd`;
H A DboothDevScript.sml203 (mul:num, mul2:num, borrow2:bool, mshift:num, rm:word,rd:word).
204 The variable rd stores the result of the multiplication.
227 `NEXTd(mul,mul2,borrow2,mshift,rm:word,rd) =
235 ALUd(borrow2,mul,rd,rm << mshift))`;
293 mshift:num, rm:word32, rd:word32) = rd`;
392 (rd' = ALU q2 q r alub)` by RW_TAC arith_ss []
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DPrecAnalysis.sml211 | (ld,rd,lsp:mini_lspec)::more_lsps =>
223 if tk' = rd then
234 (A |> c1 rel |> c1 TM |> inc) (lsp, [#3 A]) rd
236 else if sep' = rd then
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/
H A Dx64_codegen_x64Lib.sml108 val rd = x64_reg i value
111 val code = ["cmp " ^ rd ^ ", " ^ f j]
119 val rd = x64_reg i value
122 val code = ["test " ^ rd ^ ", " ^ f j]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/
H A DcheriScript.sml3973 TP[Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),Var("imm5",FTy 5),
3975 CC[LW(0,6),Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),
3984 TP[Var("function",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),
3986 CC[LW(16,6),Var("function",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),
3996 TP[Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),
3998 CC[LW(28,6),Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),LW(0,5),
4002 ("form6",TP[Var("rt",FTy 5),Var("rd",FTy 5),Var("function",FTy 6)],
4003 CC[LW(31,6),LW(0,5),Var("rt",FTy 5),Var("rd",FTy 5),LW(0,5),
7577 ("dfn'MOVF",TP[Var("rd",FTy 5),Var("rs",FTy 5),Var("cc",FTy 3)],
7597 qVar"state"),Var("rd",FT
[all...]

Completed in 334 milliseconds

123