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
|
/* Platform and devices */
/* Current constraints on this implementation are:
- it cannot access memory directly, but instead provides definitions for the physical memory model
- it can access system register state, needed to manipulate interrupt bits
- it relies on externs to get platform address information and doesn't hardcode them.
*/
/* Main memory */
val plat_ram_base = {ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
val plat_ram_size = {ocaml: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
/* ROM holding reset vector and device-tree DTB */
val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits
val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit -> xlenbits
/* Location of clock-interface, which should match with the spec in the DTB */
val plat_clint_base = {ocaml: "Platform.clint_base", lem: "plat_clint_base"} : unit -> xlenbits
val plat_clint_size = {ocaml: "Platform.clint_size", lem: "plat_clint_size"} : unit -> xlenbits
val phys_mem_segments : unit -> list((xlenbits, xlenbits))
function phys_mem_segments() =
(plat_rom_base (), plat_rom_size ()) ::
(plat_ram_base (), plat_ram_size ()) ::
[||]
val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick"} : unit -> int
/* CLINT clock device interface, based on Spike. */
// assumes a single hart, since this typically is a vector of per-hart registers.
register mtimecmp : xlenbits // memory-mapped internal clint register.
/* CLINT memory-mapped IO */
let MSIP_BASE : xlenbits = 0x0000000000000000
let MTIMECMP_BASE : xlenbits = 0x0000000000004000
let MTIME_BASE : xlenbits = 0x000000000000bff8
/* 0000 msip hart 0
* 0004 msip hart 1
* 4000 mtimecmp hart 0 lo
* 4004 mtimecmp hart 0 hi
* 4008 mtimecmp hart 1 lo
* 400c mtimecmp hart 1 hi
* bff8 mtime lo
* bffc mtime hi
*/
val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
function clint_load(addr, width) = {
/* FIXME: For now, only allow exact aligned access.
I couldn't make the more general access pass the type-checker.
*/
if addr == MSIP_BASE & ('n == 8 | 'n == 4)
then MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n)))
/* FIXME:
else if addr == MTIMECMP_BASE & ('n == 8)
then MemValue(mtimecmp)
*/
/* FIXME:
else if addr == MTIME_BASE & ('n == 8)
then MemValue(mtime)
*/
else MemException(E_Load_Access_Fault)
}
val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wreg}
function clint_store(addr, width, data) = {
if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
mip->MSI() = data[0] == 0b1;
MemValue(())
} else if addr == MTIMECMP_BASE & 'n == 8 then {
/* FIXME:
mtimecmp = data;
*/
MemValue(())
} else MemException(E_SAMO_Access_Fault)
}
/* Spike's HTIF device interface. */
bitfield htif_cmd : bits(64) = {
device : 63 .. 56,
cmd : 55 .. 48,
payload : 47 .. 0
}
// no support yet for terminal input
val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n))
function htif_load(addr, width) = MemValue(EXTZ(0b0))
val htif_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit)
function htif_store(addr, width, data) = {
// since htif is only available at a single address, we'll assume here that physical memory
// model has correctly dispatched the address.
let cbits : xlenbits = /* if 'n == 4 then EXTZ(data) else data */ EXTZ(0b0);
let cmd = Mk_htif_cmd(cbits);
match cmd.device() {
0x00 => { /* syscall-proxy */
if cmd.payload()[0] == 0b1
then /* TODO: exit command
* for e.g. set a flag that's checked by the top-level loop.
* but that might appear to be a register write effect triggered by a memory write.
*/
()
else ()
},
0x01 => { /* terminal */
match cmd.cmd() {
0x00 => /* input */ (),
0x01 => /* TODO: output data */ (),
c => print("Unknown term cmd: " ^ BitStr(c))
}
},
d => print("Unknown htif device:" ^ BitStr(d))
};
MemValue(())
}
|
