forked from riscv/sail-riscv
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathrvfi_dii.sail
387 lines (348 loc) · 22.7 KB
/
rvfi_dii.sail
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
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
/*=======================================================================================*/
/* RISCV Sail Model */
/* */
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except for the snapshots of the Lem and Sail libraries */
/* in the prover_snapshots directory (which include copies of their */
/* licences), is subject to the BSD two-clause licence below. */
/* */
/* Copyright (c) 2017-2021 */
/* Prashanth Mundkur */
/* Rishiyur S. Nikhil and Bluespec, Inc. */
/* Jon French */
/* Brian Campbell */
/* Robert Norton-Wright */
/* Alasdair Armstrong */
/* Thomas Bauereiss */
/* Shaked Flur */
/* Christopher Pulte */
/* Peter Sewell */
/* Alexander Richardson */
/* Hesham Almatary */
/* Jessica Clarke */
/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */
/* Peter Rugg */
/* Aril Computer Corp., for contributions by Scott Johnson */
/* */
/* All rights reserved. */
/* */
/* This software was developed by the above within the Rigorous */
/* Engineering of Mainstream Systems (REMS) project, partly funded by */
/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */
/* Edinburgh. */
/* */
/* This software was developed by SRI International and the University of */
/* Cambridge Computer Laboratory (Department of Computer Science and */
/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */
/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */
/* SSITH research programme. */
/* */
/* This project has received funding from the European Research Council */
/* (ERC) under the European Union’s Horizon 2020 research and innovation */
/* programme (grant agreement 789108, ELVER). */
/* */
/* */
/* 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. */
/*=======================================================================================*/
// "RISC-V Formal Interface - Direct Instruction Injection" support
// For use with https://github.com/CTSRD-CHERI/TestRIG
$define RVFI_DII
bitfield RVFI_DII_Instruction_Packet : bits(64) = {
padding : 63 .. 56, // [7]
rvfi_cmd : 55 .. 48, // [6] This token is a trace command. For example, reset device under test.
rvfi_time : 47 .. 32, // [5 - 4] Time to inject token. The difference between this and the previous
// instruction time gives a delay before injecting this instruction.
// This can be ignored for models but gives repeatability for implementations
// while shortening counterexamples.
rvfi_insn : 31 .. 0, // [0 - 3] Instruction word: 32-bit instruction or command. The lower 16-bits
// may decode to a 16-bit compressed instruction.
}
register rvfi_instruction : RVFI_DII_Instruction_Packet
val rvfi_set_instr_packet : bits(64) -> unit effect {wreg}
function rvfi_set_instr_packet(p) =
rvfi_instruction = Mk_RVFI_DII_Instruction_Packet(p)
val rvfi_get_cmd : unit -> bits(8) effect {rreg}
function rvfi_get_cmd () = rvfi_instruction.rvfi_cmd()
val rvfi_get_insn : unit -> bits(32) effect {rreg}
function rvfi_get_insn () = rvfi_instruction.rvfi_insn()
val print_instr_packet : bits(64) -> unit
function print_instr_packet(bs) = {
let p = Mk_RVFI_DII_Instruction_Packet(bs);
print_bits("command ", p.rvfi_cmd());
print_bits("instruction ", p.rvfi_insn())
}
bitfield RVFI_DII_Execution_Packet_V1 : bits(704) = {
rvfi_intr : 703 .. 696, // [87] Trap handler: Set for first instruction in trap handler.
rvfi_halt : 695 .. 688, // [86] Halt indicator: Marks the last instruction retired
// before halting execution.
rvfi_trap : 687 .. 680, // [85] Trap indicator: Invalid decode, misaligned access or
// jump command to misaligned address.
rvfi_rd_addr : 679 .. 672, // [84] Write register address: MUST be 0 if not used.
rvfi_rs2_addr : 671 .. 664, // [83] otherwise set as decoded.
rvfi_rs1_addr : 663 .. 656, // [82] Read register addresses: Can be arbitrary when not used,
rvfi_mem_wmask : 655 .. 648, // [81] Write mask: Indicates valid bytes written. 0 if unused.
rvfi_mem_rmask : 647 .. 640, // [80] Read mask: Indicates valid bytes read. 0 if unused.
rvfi_mem_wdata : 639 .. 576, // [72 - 79] Write data: Data written to memory by this command.
rvfi_mem_rdata : 575 .. 512, // [64 - 71] Read data: Data read from mem_addr (i.e. before write)
rvfi_mem_addr : 511 .. 448, // [56 - 63] Memory access addr: Points to byte address (aligned if define
// is set). *Should* be straightforward.
// 0 if unused.
rvfi_rd_wdata : 447 .. 384, // [48 - 55] Write register value: MUST be 0 if rd_ is 0.
rvfi_rs2_data : 383 .. 320, // [40 - 47] above. Must be 0 if register ID is 0.
rvfi_rs1_data : 319 .. 256, // [32 - 39] Read register values: Values as read from registers named
rvfi_insn : 255 .. 192, // [24 - 31] Instruction word: 32-bit command value.
rvfi_pc_wdata : 191 .. 128, // [16 - 23] PC after instr: Following PC - either PC + 4 or jump/trap target.
rvfi_pc_rdata : 127 .. 64, // [08 - 15] PC before instr: PC for current instruction
rvfi_order : 63 .. 0, // [00 - 07] Instruction number: INSTRET value after completion.
}
bitfield RVFI_DII_Execution_Packet_InstMetaData : bits(192) = {
/// The rvfi_order field must be set to the instruction index. No indices
/// must be used twice and there must be no gaps. Instructions may be
/// retired in a reordered fashion, as long as causality is preserved
/// (register and memory write operations must be retired before the read
/// operations that depend on them).
rvfi_order : 63 .. 0,
/// rvfi_insn is the instruction word for the retired instruction. In case
/// of an instruction with fewer than ILEN bits, the upper bits of this
/// output must be all zero. For compressed instructions the compressed
/// instruction word must be output on this port. For fused instructions the
/// complete fused instruction sequence must be output.
rvfi_insn : 127 .. 64,
/// rvfi_trap must be set for an instruction that cannot be decoded as a
/// legal instruction, such as 0x00000000.
/// In addition, rvfi_trap must be set for a misaligned memory read or
/// write in PMAs that don't allow misaligned access, or other memory
/// access violations. rvfi_trap must also be set for a jump instruction
/// that jumps to a misaligned instruction.
rvfi_trap : 135 .. 128,
/// The signal rvfi_halt must be set when the instruction is the last
/// instruction that the core retires before halting execution. It should not
/// be set for an instruction that triggers a trap condition if the CPU
/// reacts to the trap by executing a trap handler. This signal enables
/// verification of liveness properties.
rvfi_halt : 143 .. 136,
/// rvfi_intr must be set for the first instruction that is part of a trap
/// handler, i.e. an instruction that has a rvfi_pc_rdata that does not
/// match the rvfi_pc_wdata of the previous instruction.
rvfi_intr : 151 .. 144,
/// rvfi_mode must be set to the current privilege level, using the following
/// encoding: 0=U-Mode, 1=S-Mode, 2=Reserved, 3=M-Mode
rvfi_mode : 159 .. 152,
/// rvfi_ixl must be set to the value of MXL/SXL/UXL in the current privilege level,
/// using the following encoding: 1=32, 2=64
rvfi_ixl : 167 .. 160,
/// When the core retires an instruction, it asserts the rvfi_valid signal
/// and uses the signals described below to output the details of the
/// retired instruction. The signals below are only valid during such a
/// cycle and can be driven to arbitrary values in a cycle in which
/// rvfi_valid is not asserted.
rvfi_valid : 175 .. 168,
// Note: since we only send these packets in the valid state, we could
// omit the valid signal, but we need 3 bytes of padding after ixl anyway
// so we might as well include it
padding : 191 .. 176,
}
bitfield RVFI_DII_Execution_Packet_PC : bits(128) = {
/// This is the program counter (pc) before (rvfi_pc_rdata) and after
/// (rvfi_pc_wdata) execution of this instruction. I.e. this is the address
/// of the retired instruction and the address of the next instruction.
rvfi_pc_rdata : 63 .. 0,
rvfi_pc_wdata : 127 .. 64,
}
bitfield RVFI_DII_Execution_Packet_Ext_Integer : bits(320) = {
magic : 63 .. 0, // must be "int-data"
/// rvfi_rd_wdata is the value of the x register addressed by rd after
/// execution of this instruction. This output must be zero when rd is zero.
rvfi_rd_wdata : 127 .. 64,
/// rvfi_rs1_rdata/rvfi_rs2_rdata is the value of the x register addressed
/// by rs1/rs2 before execution of this instruction. This output must be
/// zero when rs1/rs2 is zero.
rvfi_rs1_rdata : 191 .. 128,
rvfi_rs2_rdata : 255 .. 192,
/// rvfi_rd_addr is the decoded rd register address for the retired
/// instruction. For an instruction that writes no rd register, this output
/// must always be zero.
rvfi_rd_addr : 263 .. 256,
/// rvfi_rs1_addr and rvfi_rs2_addr are the decoded rs1 and rs1 register
/// addresses for the retired instruction. For an instruction that reads no
/// rs1/rs2 register, this output can have an arbitrary value. However, if
/// this output is nonzero then rvfi_rs1_rdata must carry the value stored
/// in that register in the pre-state.
rvfi_rs1_addr : 271 .. 264,
rvfi_rs2_addr : 279 .. 272,
padding : 319 .. 280,
}
bitfield RVFI_DII_Execution_Packet_Ext_MemAccess : bits(704) = {
magic : 63 .. 0, // must be "mem-data"
/// rvfi_mem_rdata is the pre-state data read from rvfi_mem_addr.
/// rvfi_mem_rmask specifies which bytes are valid.
/// CHERI-extension: widened to 32 bytes to allow reporting 129 bits
rvfi_mem_rdata : 319 .. 64,
/// rvfi_mem_wdata is the post-state data written to rvfi_mem_addr.
/// rvfi_mem_wmask specifies which bytes are valid.
/// CHERI-extension: widened to 32 bytes to allow reporting 129 bits
rvfi_mem_wdata : 575 .. 320,
/// rvfi_mem_rmask is a bitmask that specifies which bytes in rvfi_mem_rdata
/// contain valid read data from rvfi_mem_addr.
/// CHERI-extension: we extend rmask+wmask to 32 bits to allow reporting the
/// mask for CHERI/RV128 accesses here.
rvfi_mem_rmask : 607 .. 576,
/// rvfi_mem_wmask is a bitmask that specifies which bytes in rvfi_mem_wdata
/// contain valid data that is written to rvfi_mem_addr.
/// CHERI-extension: widened to 32 bits
rvfi_mem_wmask : 639 .. 608,
/// For memory operations (rvfi_mem_rmask and/or rvfi_mem_wmask are
/// non-zero), rvfi_mem_addr holds the accessed memory location.
rvfi_mem_addr : 703 .. 640,
}
bitfield RVFI_DII_Execution_PacketV2 : bits(512) = {
magic : 63 .. 0, // must be set to 'trace-v2'
trace_size : 127 .. 64, // total size of the trace packet + extensions
basic_data : 319 .. 128, // RVFI_DII_Execution_Packet_InstMetaData
pc_data : 447 .. 320, // RVFI_DII_Execution_Packet_PC
// available_fields : 511 .. 448,
integer_data_available: 448, // Followed by RVFI_DII_Execution_Packet_Ext_Integer if set
memory_access_data_available: 449, // Followed by R VFI_DII_Execution_Packet_Ext_MemAccess if set
floating_point_data_available: 450, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_FP if set
csr_read_write_data_available: 451, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_CSR if set
cheri_data_available: 452, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_CHERI if set
cheri_scr_read_write_data_available: 453, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_CHERI_SCR if set
trap_data_available: 454, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_Trap if set
unused_data_available_fields : 511 .. 455, // To be used for additional RVFI_DII_Execution_Packet_Ext_* structs
}
register rvfi_inst_data : RVFI_DII_Execution_Packet_InstMetaData
register rvfi_pc_data : RVFI_DII_Execution_Packet_PC
register rvfi_int_data : RVFI_DII_Execution_Packet_Ext_Integer
register rvfi_int_data_present : bool
register rvfi_mem_data : RVFI_DII_Execution_Packet_Ext_MemAccess
register rvfi_mem_data_present : bool
// Reset the trace
val rvfi_zero_exec_packet : unit -> unit effect {wreg}
function rvfi_zero_exec_packet () = {
rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(EXTZ(0b0));
rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(EXTZ(0b0));
rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(EXTZ(0x0));
// magic = "int-data" -> 0x617461642d746e69 (big-endian)
rvfi_int_data = update_magic(rvfi_int_data, 0x617461642d746e69);
rvfi_int_data_present = false;
rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(EXTZ(0x0));
// magic = "mem-data" -> 0x617461642d6d656d (big-endian)
rvfi_mem_data = update_magic(rvfi_mem_data, 0x617461642d6d656d);
rvfi_mem_data_present = false;
}
// FIXME: most of these will no longer be necessary once we use the c2 sail backend.
val rvfi_halt_exec_packet : unit -> unit effect {wreg}
function rvfi_halt_exec_packet () =
rvfi_inst_data->rvfi_halt() = 0x01
val rvfi_get_v2_support_packet : unit -> bits(704)
function rvfi_get_v2_support_packet () = {
let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(EXTZ(0b0));
// Returning 0x3 (using the unused high bits) in halt instead of 0x1 means
// that we support the version 2 wire format. This is required to keep
// backwards compatibility with old implementations that do not support
// the new trace format.
let rvfi_exec = update_rvfi_halt(rvfi_exec, 0x03);
return rvfi_exec.bits();
}
val rvfi_get_exec_packet_v1 : unit -> bits(704) effect {rreg}
function rvfi_get_exec_packet_v1 () = {
let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(EXTZ(0b0));
// Convert the v2 packet to a v1 packet
let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data.rvfi_intr());
let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data.rvfi_halt());
let v1_packet = update_rvfi_trap(v1_packet, rvfi_inst_data.rvfi_trap());
let v1_packet = update_rvfi_insn(v1_packet, rvfi_inst_data.rvfi_insn());
let v1_packet = update_rvfi_order(v1_packet, rvfi_inst_data.rvfi_order());
let v1_packet = update_rvfi_pc_wdata(v1_packet, rvfi_pc_data.rvfi_pc_wdata());
let v1_packet = update_rvfi_pc_rdata(v1_packet, rvfi_pc_data.rvfi_pc_rdata());
let v1_packet = update_rvfi_rd_addr(v1_packet, rvfi_int_data.rvfi_rd_addr());
let v1_packet = update_rvfi_rs2_addr(v1_packet, rvfi_int_data.rvfi_rs2_addr());
let v1_packet = update_rvfi_rs1_addr(v1_packet, rvfi_int_data.rvfi_rs1_addr());
let v1_packet = update_rvfi_rd_wdata(v1_packet, rvfi_int_data.rvfi_rd_wdata());
let v1_packet = update_rvfi_rs2_data(v1_packet, rvfi_int_data.rvfi_rs2_rdata());
let v1_packet = update_rvfi_rs1_data(v1_packet, rvfi_int_data.rvfi_rs1_rdata());
let v1_packet = update_rvfi_mem_wmask(v1_packet, truncate(rvfi_mem_data.rvfi_mem_wmask(), 8));
let v1_packet = update_rvfi_mem_rmask(v1_packet, truncate(rvfi_mem_data.rvfi_mem_rmask(), 8));
let v1_packet = update_rvfi_mem_wdata(v1_packet, truncate(rvfi_mem_data.rvfi_mem_wdata(), 64));
let v1_packet = update_rvfi_mem_rdata(v1_packet, truncate(rvfi_mem_data.rvfi_mem_rdata(), 64));
let v1_packet = update_rvfi_mem_addr(v1_packet, rvfi_mem_data.rvfi_mem_addr());
return v1_packet.bits();
}
val rvfi_get_v2_trace_size : unit -> bits(64) effect {rreg}
function rvfi_get_v2_trace_size () = {
let trace_size : bits(64) = to_bits(64, 512);
let trace_size = if (rvfi_int_data_present) then trace_size + 320 else trace_size;
let trace_size = if (rvfi_mem_data_present) then trace_size + 704 else trace_size;
return trace_size >> 3; // we have to return bytes not bits
}
val rvfi_get_exec_packet_v2 : unit -> bits(512) effect {rreg}
function rvfi_get_exec_packet_v2 () = {
// TODO: add the other data
// TODO: find a way to return a variable-length bitvector
let packet = Mk_RVFI_DII_Execution_PacketV2(EXTZ(0b0));
let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE)
let packet = update_basic_data(packet, rvfi_inst_data.bits());
let packet = update_pc_data(packet, rvfi_pc_data.bits());
let packet = update_integer_data_available(packet, bool_to_bits(rvfi_int_data_present));
let packet = update_memory_access_data_available(packet, bool_to_bits(rvfi_mem_data_present));
// To simplify the implementation (so that we can return a fixed-size vector)
// we always return a max-size packet from this function, and the C emulator
// ensures that only trace_size bits are sent over the socket.
let packet = update_trace_size(packet, rvfi_get_v2_trace_size());
return packet.bits();
}
val rvfi_get_int_data : unit -> bits(320) effect {rreg}
function rvfi_get_int_data () = {
assert(rvfi_int_data_present, "reading uninitialized data");
return rvfi_int_data.bits();
}
val rvfi_get_mem_data : unit -> bits(704) effect {rreg}
function rvfi_get_mem_data () = {
assert(rvfi_mem_data_present, "reading uninitialized data");
return rvfi_mem_data.bits();
}
val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. atom('n) -> bits(32)
function rvfi_encode_width_mask(width) =
(0xFFFFFFFF >> (32 - width))
val print_rvfi_exec : unit -> unit effect {rreg}
function print_rvfi_exec () = {
print_bits("rvfi_intr : ", rvfi_inst_data.rvfi_intr());
print_bits("rvfi_halt : ", rvfi_inst_data.rvfi_halt());
print_bits("rvfi_trap : ", rvfi_inst_data.rvfi_trap());
print_bits("rvfi_rd_addr : ", rvfi_int_data.rvfi_rd_addr());
print_bits("rvfi_rs2_addr : ", rvfi_int_data.rvfi_rs2_addr());
print_bits("rvfi_rs1_addr : ", rvfi_int_data.rvfi_rs1_addr());
print_bits("rvfi_mem_wmask: ", rvfi_mem_data.rvfi_mem_wmask());
print_bits("rvfi_mem_rmask: ", rvfi_mem_data.rvfi_mem_rmask());
print_bits("rvfi_mem_wdata: ", rvfi_mem_data.rvfi_mem_wdata());
print_bits("rvfi_mem_rdata: ", rvfi_mem_data.rvfi_mem_rdata());
print_bits("rvfi_mem_addr : ", rvfi_mem_data.rvfi_mem_addr());
print_bits("rvfi_rd_wdata : ", rvfi_int_data.rvfi_rd_wdata());
print_bits("rvfi_rs2_data : ", rvfi_int_data.rvfi_rs2_rdata());
print_bits("rvfi_rs1_data : ", rvfi_int_data.rvfi_rs1_rdata());
print_bits("rvfi_insn : ", rvfi_inst_data.rvfi_insn());
print_bits("rvfi_pc_wdata : ", rvfi_pc_data.rvfi_pc_wdata());
print_bits("rvfi_pc_rdata : ", rvfi_pc_data.rvfi_pc_rdata());
print_bits("rvfi_order : ", rvfi_inst_data.rvfi_order());
}