Skip to content

Commit 8db89a9

Browse files
Tom Robertstomeroberts
Tom Roberts
authored and
tomeroberts
committed
[rtl] Add branch prediction signals to icache
These changes correspond to similar changes in the prefetch buffer to support branch prediction. A registered version of fill_ext_done was required to prevent a combinational loop from branch_i in to valid_o out. Multiplexing priorities for fifo_addr have been swapped to match fetch_addr_d in the same module and all similar multiplexing in the icache (prioritize incoming branch_i over branch_mispredict_i). Note however that it is not expected that these conditions will actually occur together, and an assertion has been added to check that. Signed-off-by: Tom Roberts <tomroberts@lowrisc.org>
1 parent 64ee9a9 commit 8db89a9

6 files changed

Lines changed: 177 additions & 113 deletions

File tree

‎dv/uvm/icache/dv/tb/tb.sv‎

Lines changed: 24 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -25,32 +25,34 @@ module tb #(parameter bit ICacheECC = 1'b0);
2525
ibex_icache #(
2626
.ICacheECC (ICacheECC)
2727
) dut (
28-
.clk_i (clk),
29-
.rst_ni (rst_n),
28+
.clk_i (clk),
29+
.rst_ni (rst_n),
3030

3131
// Connect icache <-> core interface
32-
.req_i (core_if.req),
33-
.branch_i (core_if.branch),
34-
.branch_spec_i (core_if.branch_spec),
35-
.addr_i (core_if.branch_addr),
36-
.ready_i (core_if.ready),
37-
.valid_o (core_if.valid),
38-
.rdata_o (core_if.rdata),
39-
.addr_o (core_if.addr),
40-
.err_o (core_if.err),
41-
.err_plus2_o (core_if.err_plus2),
42-
.icache_enable_i (core_if.enable),
43-
.icache_inval_i (core_if.invalidate),
44-
.busy_o (core_if.busy),
32+
.req_i (core_if.req),
33+
.branch_i (core_if.branch),
34+
.branch_spec_i (core_if.branch_spec),
35+
.predicted_branch_i (1'b0),
36+
.branch_mispredict_i (1'b0),
37+
.addr_i (core_if.branch_addr),
38+
.ready_i (core_if.ready),
39+
.valid_o (core_if.valid),
40+
.rdata_o (core_if.rdata),
41+
.addr_o (core_if.addr),
42+
.err_o (core_if.err),
43+
.err_plus2_o (core_if.err_plus2),
44+
.icache_enable_i (core_if.enable),
45+
.icache_inval_i (core_if.invalidate),
46+
.busy_o (core_if.busy),
4547

4648
// Connect icache <-> instruction bus interface
47-
.instr_req_o (mem_if.req),
48-
.instr_gnt_i (mem_if.gnt),
49-
.instr_addr_o (mem_if.addr),
50-
.instr_rdata_i (mem_if.rdata),
51-
.instr_err_i (mem_if.err),
52-
.instr_pmp_err_i (mem_if.pmp_err),
53-
.instr_rvalid_i (mem_if.rvalid)
49+
.instr_req_o (mem_if.req),
50+
.instr_gnt_i (mem_if.gnt),
51+
.instr_addr_o (mem_if.addr),
52+
.instr_rdata_i (mem_if.rdata),
53+
.instr_err_i (mem_if.err),
54+
.instr_pmp_err_i (mem_if.pmp_err),
55+
.instr_rvalid_i (mem_if.rvalid)
5456
);
5557

5658
// If the ICacheECC parameter is set in the DUT, generate another interface for each tag ram and

‎formal/icache/formal_tb.sv‎

Lines changed: 32 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -17,28 +17,31 @@
1717

1818
module formal_tb #(
1919
// DUT parameters
20-
parameter int unsigned BusWidth = 32,
21-
parameter int unsigned CacheSizeBytes = 4*1024,
22-
parameter bit ICacheECC = 1'b0,
23-
parameter int unsigned LineSize = 64,
24-
parameter int unsigned NumWays = 2,
25-
parameter bit BranchCache = 1'b0,
20+
parameter bit BranchPredictor = 1'b0,
21+
parameter int unsigned BusWidth = 32,
22+
parameter int unsigned CacheSizeBytes = 4*1024,
23+
parameter bit ICacheECC = 1'b0,
24+
parameter int unsigned LineSize = 64,
25+
parameter int unsigned NumWays = 2,
26+
parameter bit BranchCache = 1'b0,
2627

2728
// Internal parameters / localparams
28-
parameter int unsigned ADDR_W = 32,
29-
parameter int unsigned NUM_FB = 4,
30-
parameter int unsigned LINE_W = 3,
31-
parameter int unsigned BUS_BYTES = BusWidth/8,
32-
parameter int unsigned BUS_W = $clog2(BUS_BYTES),
33-
parameter int unsigned LINE_BEATS = 2,
34-
parameter int unsigned LINE_BEATS_W = 1
29+
parameter int unsigned ADDR_W = 32,
30+
parameter int unsigned NUM_FB = 4,
31+
parameter int unsigned LINE_W = 3,
32+
parameter int unsigned BUS_BYTES = BusWidth/8,
33+
parameter int unsigned BUS_W = $clog2(BUS_BYTES),
34+
parameter int unsigned LINE_BEATS = 2,
35+
parameter int unsigned LINE_BEATS_W = 1
3536
) (
3637
// Top-level ports
3738
input logic clk_i,
3839
input logic rst_ni,
3940
input logic req_i,
4041
input logic branch_i,
4142
input logic branch_spec_i,
43+
input logic predicted_branch_i,
44+
input logic branch_mispredict_i,
4245
input logic [31:0] addr_i,
4346
input logic ready_i,
4447
input logic valid_o,
@@ -65,7 +68,8 @@ module formal_tb #(
6568
input logic [NUM_FB-1:0] fill_hit_q,
6669
input logic [NUM_FB-1:0][LINE_BEATS_W:0] fill_ext_cnt_q,
6770
input logic [NUM_FB-1:0] fill_ext_hold_q,
68-
input logic [NUM_FB-1:0] fill_ext_done,
71+
input logic [NUM_FB-1:0] fill_ext_done_d,
72+
input logic [NUM_FB-1:0] fill_ext_done_q,
6973
input logic [NUM_FB-1:0][LINE_BEATS_W:0] fill_rvd_cnt_q,
7074
input logic [NUM_FB-1:0] fill_rvd_done,
7175
input logic [NUM_FB-1:0][LINE_BEATS_W:0] fill_out_cnt_q,
@@ -122,6 +126,17 @@ module formal_tb #(
122126
end
123127
end
124128

129+
// Reset assumptions
130+
//
131+
// We assume that req_i isn't asserted to the block when in reset (which avoids it making requests
132+
// on the external bus).
133+
`ASSUME_ZERO_IN_RESET(req_i)
134+
135+
// Parameter assumptions
136+
//
137+
// If BranchPredictor = 1'b0, the branch_mispredict_i signal will never go high
138+
`ASSUME(no_mispred_without_branch_pred, `IMPLIES(branch_mispredict_i, BranchPredictor))
139+
125140
// Protocol assumptions
126141
//
127142
// These are assumptions based on the top-level ports. They somewhat mirror the assertions in the
@@ -346,7 +361,7 @@ module formal_tb #(
346361
(fill_ext_cnt_q[fb] != '0) &&
347362
fill_older_q[fb][fb2] &&
348363
fill_busy_q[fb2]),
349-
fill_ext_done[fb2]))
364+
fill_ext_done_q[fb2]))
350365

351366
// Similarly, if J is older than I then we should see fill_rvd_done[J] before
352367
// fill_rvd_cnt_q[I] is nonzero.
@@ -656,7 +671,7 @@ module formal_tb #(
656671
// for beat b and the memory request was squashed by a PMP error.
657672
//
658673
// The former case is easy (bit b should be set in f_fill_rvd_mask). In the latter case,
659-
// fill_ext_done will be true, fill_ext_cnt_q will be less than LINE_BEATS, and fill_ext_off (the
674+
// fill_ext_done_d will be true, fill_ext_cnt_q will be less than LINE_BEATS, and fill_ext_off (the
660675
// next beat to fetch) will equal b. We define explicit masks for the bits allowed in each case.
661676
logic [NUM_FB-1:0][LINE_BEATS-1:0] f_rvd_err_mask, f_pmp_err_mask, f_err_mask;
662677
always_comb begin
@@ -665,7 +680,7 @@ module formal_tb #(
665680
for (int i = 0; i < NUM_FB; i++) begin
666681
f_rvd_err_mask[i] = f_fill_rvd_mask[i];
667682
for (int b = 0; b < LINE_BEATS; b++) begin
668-
f_pmp_err_mask[i][b] = (fill_ext_done[i] &&
683+
f_pmp_err_mask[i][b] = (fill_ext_done_d[i] &&
669684
!fill_ext_cnt_q[i][LINE_BEATS_W] &&
670685
(fill_ext_off[i] == b[LINE_BEATS_W-1:0]));
671686
end

‎formal/icache/formal_tb_frag.svh‎

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -8,18 +8,19 @@
88
// Using a wildcard (.*) for ports allows the testbench to inspect internal signals of the cache.
99

1010
formal_tb #(
11-
.BusWidth (BusWidth),
12-
.CacheSizeBytes (CacheSizeBytes),
13-
.ICacheECC (ICacheECC),
14-
.LineSize (LineSize),
15-
.NumWays (NumWays),
16-
.BranchCache (BranchCache),
11+
.BranchPredictor (BranchPredictor),
12+
.BusWidth (BusWidth),
13+
.CacheSizeBytes (CacheSizeBytes),
14+
.ICacheECC (ICacheECC),
15+
.LineSize (LineSize),
16+
.NumWays (NumWays),
17+
.BranchCache (BranchCache),
1718

18-
.ADDR_W (ADDR_W),
19-
.NUM_FB (NUM_FB),
20-
.LINE_W (LINE_W),
21-
.BUS_BYTES (BUS_BYTES),
22-
.BUS_W (BUS_W),
23-
.LINE_BEATS (LINE_BEATS),
24-
.LINE_BEATS_W (LINE_BEATS_W)
19+
.ADDR_W (ADDR_W),
20+
.NUM_FB (NUM_FB),
21+
.LINE_W (LINE_W),
22+
.BUS_BYTES (BUS_BYTES),
23+
.BUS_W (BUS_W),
24+
.LINE_BEATS (LINE_BEATS),
25+
.LINE_BEATS_W (LINE_BEATS_W)
2526
) tb_i (.*);

0 commit comments

Comments
 (0)