-
Notifications
You must be signed in to change notification settings - Fork 25
/
rvfi_cover_check.sv
108 lines (94 loc) · 3.2 KB
/
rvfi_cover_check.sv
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
// Copyright (C) 2017 Claire Xenia Wolf <[email protected]>
//
// Permission to use, copy, modify, and/or distribute this software for any
// purpose with or without fee is hereby granted, provided that the above
// copyright notice and this permission notice appear in all copies.
//
// THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
// WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
// MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
// ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
// WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
// ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
// OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
module rvfi_cover_check (
input clock, reset, check,
`RVFI_INPUTS
);
`ifdef RISCV_FORMAL_ROLLBACK
(* keep *) integer cnt_rollback;
integer cnt_rollback_q;
always @(posedge clock) begin
cnt_rollback_q <= cnt_rollback;
end
always @* begin
if (reset)
cnt_rollback = 0;
else
cnt_rollback = cnt_rollback_q + rvfi_rollback_valid;
end
`endif
genvar channel_idx;
generate for (channel_idx = 0; channel_idx < `RISCV_FORMAL_NRET; channel_idx=channel_idx+1) begin:channel
`RVFI_GETCHANNEL(channel_idx)
(* keep *) integer cnt_insns;
(* keep *) integer cnt_trap_insns;
(* keep *) integer cnt_intr_insns;
(* keep *) integer cnt_norm_insns;
`ifdef RISCV_FORMAL_ROLLBACK
// "arb" = after rollback
(* keep *) integer arb_cnt_insns;
(* keep *) integer arb_cnt_trap_insns;
(* keep *) integer arb_cnt_intr_insns;
(* keep *) integer arb_cnt_norm_insns;
`endif
integer cnt_insns_q;
integer cnt_trap_insns_q;
integer cnt_intr_insns_q;
integer cnt_norm_insns_q;
`ifdef RISCV_FORMAL_ROLLBACK
integer arb_cnt_insns_q;
integer arb_cnt_trap_insns_q;
integer arb_cnt_intr_insns_q;
integer arb_cnt_norm_insns_q;
`endif
always @(posedge clock) begin
cnt_insns_q <= cnt_insns;
cnt_trap_insns_q <= cnt_trap_insns;
cnt_intr_insns_q <= cnt_intr_insns;
cnt_norm_insns_q <= cnt_norm_insns;
`ifdef RISCV_FORMAL_ROLLBACK
arb_cnt_insns_q <= arb_cnt_insns;
arb_cnt_trap_insns_q <= arb_cnt_trap_insns;
arb_cnt_intr_insns_q <= arb_cnt_intr_insns;
arb_cnt_norm_insns_q <= arb_cnt_norm_insns;
`endif
end
always @* begin
if (reset) begin
cnt_insns = 0;
cnt_trap_insns = 0;
cnt_intr_insns = 0;
cnt_norm_insns = 0;
`ifdef RISCV_FORMAL_ROLLBACK
arb_cnt_insns = 0;
arb_cnt_trap_insns = 0;
arb_cnt_intr_insns = 0;
arb_cnt_norm_insns = 0;
`endif
end else begin
cnt_insns = cnt_insns_q + valid;
cnt_trap_insns = cnt_trap_insns_q + (valid && trap);
cnt_intr_insns = cnt_intr_insns_q + (valid && intr);
cnt_norm_insns = cnt_norm_insns_q + (valid && !{trap,intr});
`ifdef RISCV_FORMAL_ROLLBACK
arb_cnt_insns = arb_cnt_insns_q + (valid && cnt_rollback);
arb_cnt_trap_insns = arb_cnt_trap_insns_q + (valid && cnt_rollback && trap);
arb_cnt_intr_insns = arb_cnt_intr_insns_q + (valid && cnt_rollback && intr);
arb_cnt_norm_insns = arb_cnt_norm_insns_q + (valid && cnt_rollback && !{trap,intr});
`endif
end
end
end endgenerate
`include "cover_stmts.vh"
endmodule