-
Notifications
You must be signed in to change notification settings - Fork 2
/
README.html
216 lines (158 loc) · 7.47 KB
/
README.html
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
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
<h1>RISCV ISA Formal Spec in BSV</h1>
<p>A formal spec of the RISC-V Instruction Set Architecture, written in Bluespec BSV (executable, synthesizable).</p>
<p>MIT License (see LICENSE.txt)</p>
<p>This is a formal specification, written in BSV, of (a subset of) the
RISC-V ISA. The original RISC-V specs (written in English text) are
the following two documents at <a href="https://riscv.org/">The RISC-V
Foundation</a>:</p>
<blockquote>
<p>The RISC-V Instruction Set Manual <br />
Volume I: User-Level ISA <br />
Document Version 2.2 <br />
Editors: Andrew Waterman , Krste Asanovic <br />
May 7, 2017</p>
<p>The RISC-V Instruction Set Manual <br />
Volume II: Privileged Architecture <br />
Privileged Architecture Version 1.10 <br />
Editors: Andrew Waterman , Krste Asanovic <br />
May 7, 2017</p>
</blockquote>
<p>This formal spec covers:</p>
<ul>
<li><p>RV32IM and RV64IM, i.e., the 32-bit and 64-bit user-level
instruction sets ("I"), including integer
multiply/ divide/ remainder ("M").</p></li>
<li><p>A subset of machine-level privileged instructions and CSRs,
including trap handling but excluding physical memory
protection and performance-monitoring.</p></li>
</ul>
<p>This formal spec will be extended in future to cover other user-level
features (A, F, D, etc.) and other privilege levels (supervisor).</p>
<hr />
<h2>Source codes</h2>
<p>The spec source code files are in the RISCV_Spec/ directory. The
source code contains detailed comments.</p>
<p><code>ISA_Decls.bsv</code> <br />
Specifies user-level instruction encodings.</p>
<p><code>ISA_Decls_Priv_M.bsv</code> <br />
Specifies machine-level privilege CSRs and instruction encodings.</p>
<p><code>RISCV_Spec.bsv</code> <br />
The top-level of the spec, specifying instruction semantics.</p>
<p><code>RegFiles.bsv</code> <br />
Specifies integer GPRs and CSRs</p>
<p><code>IntMulDivRem_ALU.bsv</code> <br />
Specifies ALU for "M" operation (Mul/Div/Rem)</p>
<p>In <code>RISCV_Spec.bsv</code>, the spec is encapsulated into module
<code>mkRISCV_Spec</code> whose parameters include a register file and a memory,
and whose interface includes hooks to control its execution from GDB.
Inside the module the main action is in rules <code>rl_fetch</code> and
<code>rl_exec</code>. The latter invokes the top-level semantic function
<code>fa_exec()</code>.</p>
<p>We deliberately split LD, ST, FENCE.I and FENCE instructions into two
phases (instead of treating them as pure functions) in order to allow
access to shared memory to be interleaved with other hardware threads.
The second phase of these instructions is seen in the rules
<code>rl_exec_LD_response</code>,
<code>rl_exec_ST_response</code>
<code>rl_exec_FENCE_I_response</code>,
and <code>rl_exec_FENCE_response</code>.</p>
<hr />
<h2>Executability</h2>
<p>This spec is executable, both in simulation and in hardware.
Simulation vehicles include Bluespec Bluesim and Verilog simulators.
Hardware execution would typically be on an FPGA, where it could be
used as a "tandem verifier" for an actual CPU implementation.</p>
<p>In this repo we provide a pre-built executable simulator:</p>
<blockquote>
<p><code>Simulator/exe_hw_d</code></p>
</blockquote>
<p>The executable was built and tested on Ubuntu 17.04, and also tested
on Debian 8.9 (jessie). Hopefully it should run on any x86 64-bit
Linux.</p>
<p>In this executable:</p>
<blockquote>
<p>The CPU connects to an I-Cache and a D-Cache <br />
The caches connect to an AXI4-like fabric <br />
The AXI4-like fabric connects to a Memory and a UART
(stdio of a program running on the CPU is directed to the UART)</p>
</blockquote>
<p>To avoid overwhelming the reader, we do not provide all this extra
infrastructure (which is quite substantial, including a Debug Module
that can connect to GDB, and more). The <code>RISCV_Spec/</code> directory only
contains the code for the CPU, and therefore you will not be able to
re-build the excutable.</p>
<hr />
<h2>Running the executable on example C programs</h2>
<p>We have provided a number of example C programs, and their
pre-compiled ELF files etc in directories like these:</p>
<blockquote>
<p><code>Test_Programs/hello</code> (Hello World!) <br />
<code>Test_Programs/qsort</code> (Quicksort) <br />
<code>Test_Programs/towers</code> (Towers of Hanoi) </p>
</blockquote>
<p>Each directory contains a number of files. For example, in the
<code>hello</code> directory you will see:</p>
<blockquote>
<p><code>hello.c</code></p>
</blockquote>
<p>This is the orginal C source code.</p>
<blockquote>
<p><code>hello</code></p>
</blockquote>
<p>This is an ELF file, produced by using gcc to compile the C program
for a bare-metal RISC-V RV32IM target (i.e., not Linux target). To
recreate an ELF file you will have to build yourself a RISC-V Gnu tool
chain. Our bare-metal ELF files have startup code that start
execution at PC = 0x200, and connect stdio to the UART.</p>
<blockquote>
<p><code>hello.text</code></p>
</blockquote>
<p>A text disassembly of the ELF program using the standard <code>objdump</code> Gnu
tool (part of the RISC-V Gnu tool chain).</p>
<blockquote>
<p><code>hello.mem_hex</code></p>
</blockquote>
<p>A memory contents file produced from the ELF file. This is in
standard Verilog 'Memory Hex' format, and represents the contents of
memory when the RISC-V CPU starts executing. See section below on
ELF-to-hex conversion.</p>
<p>To run an example program, in the top-level directory you can say:</p>
<blockquote>
<p><code>make test_hello</code> <br />
<code>make test_qsort</code> <br />
<code>make test_towers</code> </p>
</blockquote>
<p>As you will see from the simple Makefile in the top-level directory,
it makes a symbolic link from <code>Mem_Model.hex</code> to one of the test
program memhex files, and then runs <code>Simlator/exe_hw_d</code>.</p>
<p>The output is more interesting if you turn on simulation verbosity:</p>
<blockquote>
<p><code>make SIM_VERBOSITY=1 test_hello</code> PC and instruction trace <br />
<code>make SIM_VERBOSITY=2 test_hello</code> More detail </p>
</blockquote>
<p>In each test program directory you will see transcripts of running the
program at various verbosity levels:</p>
<blockquote>
<p><code>transcript_hello_verbosity_0</code> <br />
<code>transcript_hello_verbosity_1</code> <br />
<code>transcript_hello_verbosity_2</code> </p>
</blockquote>
<p>If you have a RISC-V toolchain, you can compile your own C program
into an ELF file, convert it into a memhex file, and run the simulator
on it. Please contact us for details of the boilerplate code to start
execution at PC 0x200 and to connect stdio to the UART.</p>
<hr />
<h2>ELF to Mem Hex file conversion</h2>
<p>Many ELF-to-hex tools exist on the Web, but we have also provided a
simple one in:</p>
<blockquote>
<p><code>Tool_elf_to_hex/elf_to_hex.c</code></p>
</blockquote>
<p>Compile this file, and then execute it with two command-line
arguments, the path/filename of the input ELF file, and the
path/filename of the output memhex file.</p>
<hr />
<h2>References</h2>
<p>Bluespec support: email <code>support@bluespec.com</code></p>
<p>Bluespec, Inc. web site <a href="http://www.bluespec.com">www.bluespec.com</a>.</p>
<p>RISC-V Foundation web site <a href="https://riscv.org">www.riscv.org</a></p>