1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
open Sail_lib;;
module P = Platform_impl;;
module Elf = Elf_loader;;
(* Platform configuration *)
let config_enable_rvc = ref true
let config_enable_next = ref false
let config_enable_writable_misa = ref true
let config_enable_dirty_update = ref false
let config_enable_misaligned_access = ref false
let config_mtval_has_illegal_inst_bits = ref false
let config_enable_pmp = ref false
let platform_arch = ref P.RV64
(* logging *)
let config_print_instr = ref true
let config_print_reg = ref true
let config_print_mem_access = ref true
let config_print_platform = ref true
let print_instr s =
if !config_print_instr
then print_endline s
else ()
let print_reg s =
if !config_print_reg
then print_endline s
else ()
let print_mem_access s =
if !config_print_mem_access
then print_endline s
else ()
let print_platform s =
if !config_print_platform
then print_endline s
else ()
let get_config_print_instr () = !config_print_instr
let get_config_print_reg () = !config_print_reg
let get_config_print_mem () = !config_print_mem_access
let get_config_print_platform () = !config_print_platform
(* Mapping to Sail externs *)
let cur_arch_bitwidth () =
match !platform_arch with
| P.RV64 -> Big_int.of_int 64
| P.RV32 -> Big_int.of_int 32
let arch_bits_of_int i =
get_slice_int (cur_arch_bitwidth (), Big_int.of_int i, Big_int.zero)
let arch_bits_of_int64 i =
get_slice_int (cur_arch_bitwidth (), Big_int.of_int64 i, Big_int.zero)
let rom_size_ref = ref 0
let make_rom arch start_pc =
let reset_vec =
List.concat (List.map P.uint32_to_bytes (P.reset_vec_int arch start_pc)) in
let dtb = P.make_dtb (P.make_dts arch) in
let rom = reset_vec @ dtb in
( rom_size_ref := List.length rom;
(*
List.iteri (fun i c ->
print_mem_access "rom[0x%Lx] <- %x\n"
(Int64.add P.rom_base (Int64.of_int i))
c
) rom;
*)
rom )
let enable_writable_misa () = !config_enable_writable_misa
let enable_rvc () = !config_enable_rvc
let enable_next () = !config_enable_next
let enable_fdext () = false
let enable_dirty_update () = !config_enable_dirty_update
let enable_misaligned_access () = !config_enable_misaligned_access
let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
let enable_pmp () = !config_enable_pmp
let enable_zfinx () = false
let rom_base () = arch_bits_of_int64 P.rom_base
let rom_size () = arch_bits_of_int !rom_size_ref
let dram_base () = arch_bits_of_int64 P.dram_base
let dram_size () = arch_bits_of_int64 !P.dram_size_ref
let clint_base () = arch_bits_of_int64 P.clint_base
let clint_size () = arch_bits_of_int64 P.clint_size
let insns_per_tick () = Big_int.of_int P.insns_per_tick
let htif_tohost () =
arch_bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ()))
(* Entropy Source - get random bits *)
(* This function can be changed to support deterministic sequences of
pseudo-random bytes. This is useful for testing. *)
let get_16_random_bits () = arch_bits_of_int (Random.int 0xFFFF)
(* load reservation *)
let speculate_conditional () = true
let reservation = ref "none" (* shouldn't match any valid address *)
let load_reservation addr =
print_platform (Printf.sprintf "reservation <- %s\n" (string_of_bits addr));
reservation := string_of_bits addr
let match_reservation addr =
print_platform (Printf.sprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr));
string_of_bits addr = !reservation
let cancel_reservation () =
print_platform (Printf.sprintf "reservation <- none\n");
reservation := "none"
let read_mem (rk, addrsize, addr, len) =
Sail_lib.fast_read_ram (len, addr)
let write_mem_ea _ = ()
let write_mem (wk, addrsize, addr, len, value) =
Sail_lib.write_ram' (len, Sail_lib.uint addr, value); true
let excl_res _ = true
let barrier _ = ()
(* terminal I/O *)
let term_write char_bits =
let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in
P.term_write (char_of_int (Big_int.to_int big_char))
let term_read () =
let c = P.term_read () in
arch_bits_of_int (int_of_char c)
(* physical memory *)
let get_mem_bytes addr len =
read_mem_bytes addr len
(* returns starting value for PC, i.e. start of reset vector *)
let init arch elf_file =
platform_arch := arch;
Elf.load_elf elf_file;
print_platform (Printf.sprintf "\nRegistered htif_tohost at 0x%Lx.\n" (Big_int.to_int64 (Elf.elf_tohost ())));
print_platform (Printf.sprintf "Registered clint at 0x%Lx (size 0x%Lx).\n%!" P.clint_base P.clint_size);
let start_pc = Elf.Big_int.to_int64 (Elf.elf_entry ()) in
let rom = make_rom arch start_pc in
let rom_base = Big_int.of_int64 P.rom_base in
let rec write_rom ofs = function
| [] -> ()
| h :: tl -> let addr = Big_int.add rom_base (Big_int.of_int ofs) in
(wram addr h);
write_rom (ofs + 1) tl
in ( write_rom 0 rom;
get_slice_int (cur_arch_bitwidth (), rom_base, Big_int.zero)
)
|
