1open HolKernel boolLib bossLib 2open stateLib set_sepTheory progTheory riscv_stepTheory 3 4val () = new_theory "riscv_prog" 5 6(* ------------------------------------------------------------------------ *) 7 8val _ = stateLib.sep_definitions "riscv" [] 9 (List.map Lib.list_of_singleton 10 ["c_update", "log", "totalCore", "done", "clock", "c_tlb", 11 "c_instret", "c_cycles", "c_UCSR", "c_SCSR", "c_ReserveLoad", 12 "c_HCSR", "c_ExitCode"]) 13 riscv_stepTheory.NextRISCV_def 14 15val riscv_instr_def = Define` 16 riscv_instr (a, i: word32) = 17 { (riscv_c_MEM8 a, riscv_d_word8 ((7 >< 0) i)); 18 (riscv_c_MEM8 (a + 1w), riscv_d_word8 ((15 >< 8) i)); 19 (riscv_c_MEM8 (a + 2w), riscv_d_word8 ((23 >< 16) i)); 20 (riscv_c_MEM8 (a + 3w), riscv_d_word8 ((31 >< 24) i)) }`; 21 22val riscv_proj_def = DB.definition "riscv_proj_def" 23 24val RISCV_MODEL_def = Define` 25 RISCV_MODEL = 26 (STATE riscv_proj, NEXT_REL (=) NextRISCV, riscv_instr, 27 ($= :riscv_state -> riscv_state -> bool), K F : riscv_state -> bool)` 28 29val RISCV_IMP_SPEC = Theory.save_thm ("RISCV_IMP_SPEC", 30 stateTheory.IMP_SPEC 31 |> Q.ISPECL [`riscv_proj`, `NextRISCV`, `riscv_instr`] 32 |> REWRITE_RULE [GSYM RISCV_MODEL_def] 33 ) 34 35val RISCV_IMP_TEMPORAL = Theory.save_thm ("RISCV_IMP_TEMPORAL", 36 temporal_stateTheory.IMP_TEMPORAL 37 |> Q.ISPECL [`riscv_proj`, `NextRISCV`, `riscv_instr`, 38 `(=) : riscv_state -> riscv_state -> bool`, 39 `K F : riscv_state -> bool`] 40 |> REWRITE_RULE [GSYM RISCV_MODEL_def] 41 ) 42 43(* ------------------------------------------------------------------------ *) 44 45val riscv_ID_def = Define` 46 riscv_ID id mcsr = 47 riscv_exception NoException * riscv_procID id * riscv_c_NextFetch id NONE * 48 riscv_c_MCSR id mcsr * cond (mcsr.mstatus.VM = 0w)` 49 50val riscv_ID_PC_def = Define` 51 riscv_ID_PC id pc = riscv_c_PC id pc * cond (aligned 2 pc)` 52 53(* ------------------------------------------------------------------------ 54 Specialize to RV64I, core 0 55 ------------------------------------------------------------------------ *) 56 57val riscv_RV64I_def = Define` 58 riscv_RV64I mcsr = cond (mcsr.mcpuid.ArchBase = 2w) * riscv_ID 0w mcsr` 59 60val riscv_REG_def = Define`riscv_REG = riscv_c_gpr 0w` 61val riscv_PC_def = Define`riscv_PC = riscv_ID_PC 0w` 62 63(* ------------------------------------------------------------------------ *) 64 65val RISCV_PC_INTRO = Q.store_thm("RISCV_PC_INTRO", 66 `SPEC m (p1 * riscv_ID_PC c pc) code (p2 * riscv_c_PC c pc') ==> 67 (aligned 2 pc ==> aligned 2 pc') ==> 68 SPEC m (p1 * riscv_ID_PC c pc) code (p2 * riscv_ID_PC c pc')`, 69 REPEAT STRIP_TAC 70 \\ FULL_SIMP_TAC std_ss 71 [riscv_ID_PC_def, SPEC_MOVE_COND, STAR_ASSOC, SEP_CLAUSES] 72 ) 73 74val RISCV_TEMPORAL_PC_INTRO = Q.store_thm("RISCV_TEMPORAL_PC_INTRO", 75 `TEMPORAL_NEXT m (p1 * riscv_ID_PC c pc) code (p2 * riscv_c_PC c pc') ==> 76 (aligned 2 pc ==> aligned 2 pc') ==> 77 TEMPORAL_NEXT m (p1 * riscv_ID_PC c pc) code (p2 * riscv_ID_PC c pc')`, 78 REPEAT STRIP_TAC 79 \\ FULL_SIMP_TAC std_ss 80 [riscv_ID_PC_def, temporal_stateTheory.TEMPORAL_NEXT_MOVE_COND, 81 STAR_ASSOC, SEP_CLAUSES] 82 ) 83 84val cond_branch_aligned = Q.store_thm("cond_branch_aligned", 85 `(aligned 2 (pc: word64) ==> 86 aligned 2 87 (if b then 88 pc + 89 sw2sw (v2w [x0; x21; x1; x2; x3; x4; 90 x5; x6; x17; x18; x19; x20] : word12) << 1 91 else pc + 4w)) = (aligned 2 pc /\ b ==> ~x20)`, 92 rw [alignmentTheory.aligned_extract] 93 \\ blastLib.FULL_BBLAST_TAC 94 ) 95 96val jal_aligned = Q.store_thm("jal_aligned", 97 `(aligned 2 (pc: word64) ==> aligned 2 (pc + sw2sw (a: word20) << 1)) = 98 aligned 2 pc ==> ~word_lsb a`, 99 rw [alignmentTheory.aligned_extract] 100 \\ blastLib.BBLAST_TAC 101 ) 102 103val jalr_aligned = Q.store_thm("jalr_aligned", 104 `~(a: word12) ' 1 /\ (b \/ aligned 2 (v: word64)) /\ 105 (c ==> aligned 2 (if b then sw2sw a && 0xFFFFFFFFFFFFFFFEw 106 else v + sw2sw a && 0xFFFFFFFFFFFFFFFEw)) = 107 ~(a: word12) ' 1 /\ (b \/ aligned 2 (v: word64))`, 108 rw [alignmentTheory.aligned_extract] 109 \\ blastLib.FULL_BBLAST_TAC 110 ) 111 112(* ------------------------------------------------------------------------ *) 113 114val c_gpr_frame = Q.store_thm("c_gpr_frame", 115 `!c_gpr a b w s x. 116 riscv_c_c_gpr a b IN x ==> 117 (FRAME_STATE riscv_proj x 118 (s with c_gpr := (a =+ (b =+ w) (c_gpr a)) c_gpr) = 119 FRAME_STATE riscv_proj x (s with c_gpr := c_gpr))`, 120 rw [stateTheory.FRAME_STATE_def, stateTheory.SELECT_STATE_def, 121 set_sepTheory.fun2set_def, pred_setTheory.EXTENSION] 122 \\ eq_tac 123 \\ rw [] 124 \\ Cases_on `a'` 125 \\ rw [combinTheory.APPLY_UPDATE_THM, riscv_proj_def] 126 \\ Cases_on `b = c0` 127 \\ fs [] 128 ) 129 130(* ------------------------------------------------------------------------ *) 131 132val riscv_opcode_bytes = Theory.save_thm("riscv_opcode_bytes", 133 blastLib.BBLAST_PROVE 134 ``(d @@ ((c @@ ((b @@ a) : word16)) : word24) = r: word32) = 135 (a = ( 7 >< 0) r : word8) /\ 136 (b = (15 >< 8) r : word8) /\ 137 (c = (23 >< 16) r : word8) /\ 138 (d = (31 >< 24) r : word8)``) 139 140val () = export_theory() 141