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
|
// "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 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 : 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.
}
register rvfi_exec : RVFI_DII_Execution_Packet
val rvfi_zero_exec_packet : unit -> unit effect {wreg}
function rvfi_zero_exec_packet () =
rvfi_exec = Mk_RVFI_DII_Execution_Packet(sail_zero_extend(0b0,704))
val rvfi_halt_exec_packet : unit -> unit effect {wreg}
function rvfi_halt_exec_packet () =
rvfi_exec->rvfi_halt() = 0x01
val rvfi_get_exec_packet : unit -> bits(704) effect {rreg}
function rvfi_get_exec_packet() = rvfi_exec.bits()
val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 8. atom('n) -> bits(8)
function rvfi_encode_width_mask(width) =
(0xFF >> (8 - width))
val print_rvfi_exec : unit -> unit effect {rreg}
function print_rvfi_exec () = {
print_bits("rvfi_intr : ", rvfi_exec.rvfi_intr());
print_bits("rvfi_halt : ", rvfi_exec.rvfi_halt());
print_bits("rvfi_trap : ", rvfi_exec.rvfi_trap());
print_bits("rvfi_rd_addr : ", rvfi_exec.rvfi_rd_addr());
print_bits("rvfi_rs2_addr : ", rvfi_exec.rvfi_rs2_addr());
print_bits("rvfi_rs1_addr : ", rvfi_exec.rvfi_rs1_addr());
print_bits("rvfi_mem_wmask: ", rvfi_exec.rvfi_mem_wmask());
print_bits("rvfi_mem_rmask: ", rvfi_exec.rvfi_mem_rmask());
print_bits("rvfi_mem_wdata: ", rvfi_exec.rvfi_mem_wdata());
print_bits("rvfi_mem_rdata: ", rvfi_exec.rvfi_mem_rdata());
print_bits("rvfi_mem_addr : ", rvfi_exec.rvfi_mem_addr());
print_bits("rvfi_rd_wdata : ", rvfi_exec.rvfi_rd_wdata());
print_bits("rvfi_rs2_data : ", rvfi_exec.rvfi_rs2_data());
print_bits("rvfi_rs1_data : ", rvfi_exec.rvfi_rs1_data());
print_bits("rvfi_insn : ", rvfi_exec.rvfi_insn());
print_bits("rvfi_pc_wdata : ", rvfi_exec.rvfi_pc_wdata());
print_bits("rvfi_pc_rdata : ", rvfi_exec.rvfi_pc_rdata());
print_bits("rvfi_order : ", rvfi_exec.rvfi_order());
}
|
