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
171
172
173
174
|
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
(* Brian Campbell *)
(* Thomas Bauereiss *)
(* Anthony Fox *)
(* Jon French *)
(* Dominic Mulligan *)
(* Stephen Kell *)
(* Mark Wassell *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(**************************************************************************)
open Sail_lib;;
module P = Platform_impl;;
module Elf = Elf_loader;;
(* Platform configuration *)
let config_enable_dirty_update = ref false
let config_enable_misaligned_access = ref false
let config_mtval_has_illegal_inst_bits = ref false
(* 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 ()
(* Mapping to Sail externs *)
let bits_of_int i =
get_slice_int (Big_int.of_int 64, Big_int.of_int i, Big_int.zero)
let bits_of_int64 i =
get_slice_int (Big_int.of_int 64, Big_int.of_int64 i, Big_int.zero)
let rom_size_ref = ref 0
let make_rom start_pc =
let reset_vec = List.concat (List.map P.uint32_to_bytes (P.reset_vec_int start_pc)) in
let dtb = P.make_dtb (P.make_dts ()) 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_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 rom_base () = bits_of_int64 P.rom_base
let rom_size () = bits_of_int !rom_size_ref
let dram_base () = bits_of_int64 P.dram_base
let dram_size () = bits_of_int64 !P.dram_size_ref
let htif_tohost () =
bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ()))
let clint_base () = bits_of_int64 P.clint_base
let clint_size () = bits_of_int64 P.clint_size
let insns_per_tick () = Big_int.of_int P.insns_per_tick
(* 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"
(* 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
bits_of_int (int_of_char c)
(* returns starting value for PC, i.e. start of reset vector *)
let init elf_file =
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 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 (Big_int.of_int 64, rom_base, Big_int.zero)
)
|
