Skip to content

Commit 8c3859e

Browse files
TheMightyDuckOfDoomTheMightyDuckOfDoom
committed
formal: instruction_cache
1 parent fd6a84e commit 8c3859e

File tree

2 files changed

+137
-15
lines changed

2 files changed

+137
-15
lines changed

‎formal/instruction_cache.sby‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ prove
55
[options]
66
cover: mode cover
77
prove: mode prove
8-
depth 20
8+
depth 10
99
smtc startup_reset.smtc
1010

1111
[engines]
@@ -14,7 +14,7 @@ smtbmc yices
1414
[script]
1515
plugin -i slang-sva.so
1616
read_slang --top instruction_cache -F formal.f \
17-
--compat-mode --keep-hierarchy \
17+
--compat-mode \
1818
--allow-use-before-declare --ignore-unknown-modules
1919
prep -top instruction_cache
2020

‎rtl/compute_unit/instruction_cache.sv‎

Lines changed: 135 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -8,23 +8,22 @@
88
// Simple direct mapped cache
99
module instruction_cache #(
1010
/// Width of the Program Counter
11-
parameter int unsigned PcWidth = 32,
11+
parameter int unsigned PcWidth = 8,
1212
/// Number of warps per compute unit
1313
parameter int unsigned NumWarps = 8,
1414
/// Number of threads per warp
1515
parameter int unsigned WarpWidth = 32,
1616
/// Encoded instruction width
1717
parameter int unsigned EncInstWidth = 4,
1818
/// Encoded instructions per cacheline -> Also determines the memory interface width
19-
parameter int unsigned CachelineIdxBits = 1,
19+
parameter int unsigned CachelineIdxBits = 2,
2020
/// Number of cachelines in the instruction cache
21-
parameter int unsigned NumCachelines = 2,
21+
parameter int unsigned NumCachelines = 8,
2222

2323
/// Dependent parameter, do **not** overwrite.
24-
parameter int unsigned SubwarpIdWidth = WarpWidth > 1 ? $clog2(WarpWidth) : 1,
25-
parameter int unsigned WidWidth = NumWarps > 1 ? $clog2(NumWarps) : 1,
26-
parameter int unsigned CachelineAddrWidth = CachelineIdxBits > 0 ? PcWidth - CachelineIdxBits
27-
: PcWidth,
24+
parameter int unsigned SubwarpIdWidth = WarpWidth > 1 ? $clog2(WarpWidth) : 1,
25+
parameter int unsigned WidWidth = NumWarps > 1 ? $clog2(NumWarps) : 1,
26+
parameter int unsigned CachelineAddrWidth = PcWidth - CachelineIdxBits,
2827
parameter type cache_addr_t = logic [CachelineAddrWidth-1:0],
2928
parameter type wid_t = logic [ WidWidth-1:0],
3029
parameter type pc_t = logic [ PcWidth-1:0],
@@ -468,6 +467,13 @@ module instruction_cache #(
468467
assert property (@(posedge clk_i) disable iff (!rst_ni)
469468
!(mem_req_o && mem_ready_i) || (state_d == WAIT_FOR_MEM)
470469
) else $fatal(1, "Memory request sent, but did not go to WAIT_FOR_MEM state.");
470+
471+
// If decoder is not ready, the output must stay stable and valid
472+
assert property (@(posedge clk_i)
473+
!$past(ic_valid_o && !dec_ready_i && rst_ni) || !rst_ni
474+
|| (ic_valid_o && $stable({ic_pc_o, ic_act_mask_o, ic_warp_id_o,
475+
ic_subwarp_id_o, ic_inst_o}))
476+
) else $fatal(1, "Decoder not ready, but output changed.");
471477
`endif
472478

473479
// #######################################################################################
@@ -509,6 +515,9 @@ module instruction_cache #(
509515
// Check that we can perform memory requests
510516
cover property (@(posedge clk_i) disable iff (!rst_ni) (mem_req_o && mem_ready_i));
511517
cover property (@(posedge clk_i) disable iff (!rst_ni) (!mem_req_o && mem_ready_i));
518+
// Check that we can receive memory responses
519+
cover property (@(posedge clk_i) disable iff (!rst_ni) (mem_valid_i));
520+
cover property (@(posedge clk_i) disable iff (!rst_ni) (!mem_valid_i));
512521
// Check that we can receive a new instruction
513522
cover property (@(posedge clk_i) disable iff (!rst_ni) (fe_valid_i && ic_ready_o));
514523
cover property (@(posedge clk_i) disable iff (!rst_ni) (fe_valid_i && !ic_ready_o));
@@ -517,23 +526,136 @@ module instruction_cache #(
517526
cover property (@(posedge clk_i) disable iff (!rst_ni) (!ic_valid_o && dec_ready_i));
518527

519528
/// Memory Latency Model
520-
localparam int unsigned FormalMemLatency = 5;
521-
logic [FormalMemLatency-1:0] mem_valid_shift;
529+
localparam int unsigned FormalMemLatency = 3;
530+
logic [FormalMemLatency-1:0] fv_mem_req_shift;
531+
cache_addr_t [FormalMemLatency-1:0] fv_mem_addr_shift;
522532
always_ff @(posedge clk_i or negedge rst_ni) begin
523533
if (!rst_ni) begin
524-
mem_valid_shift <= '0;
534+
fv_mem_req_shift <= '0;
535+
fv_mem_addr_shift <= '0;
525536
end else begin
526-
mem_valid_shift <= {mem_valid_shift[FormalMemLatency-2:0],
537+
fv_mem_req_shift <= {fv_mem_req_shift[FormalMemLatency-2:0],
527538
mem_req_o && mem_ready_i};
539+
fv_mem_addr_shift <= {fv_mem_addr_shift[FormalMemLatency-2:0],
540+
mem_addr_o};
528541
end
529542
end
530543

531544
// Memory valid signal must be delayed version of mem_req_o && mem_ready_i
532545
assume property (@(posedge clk_i) disable iff (!rst_ni)
533-
(mem_valid_i == mem_valid_shift[FormalMemLatency-1]));
546+
(mem_valid_i == fv_mem_req_shift[FormalMemLatency-1]));
534547

535548
// There can only be one active memory request at a time
536-
assert property (@(posedge clk_i) $onehot0(mem_valid_shift));
549+
assert property (@(posedge clk_i) $onehot0(fv_mem_req_shift));
550+
551+
// New request
552+
cache_addr_t f_mem_addr;
553+
cache_data_t f_mem_data;
554+
act_mask_t f_act_mask;
555+
wid_t f_warp_id;
556+
subwarp_id_t f_subwarp_id;
557+
558+
assign f_mem_addr = $anyconst;
559+
assign f_mem_data = $anyconst;
560+
assign f_act_mask = $anyconst;
561+
assign f_warp_id = $anyconst;
562+
assign f_subwarp_id = $anyconst;
563+
564+
// Assume that if the fetcher request the instruction with f_pc, we have a request with f_* signals
565+
logic fetcher_request_matches_f_pc;
566+
assign fetcher_request_matches_f_pc =
567+
fe_valid_i && (fe_pc_i[PcWidth-1:CachelineIdxBits] == f_mem_addr);
568+
assume property (@(posedge clk_i) disable iff (!rst_ni)
569+
!fetcher_request_matches_f_pc || (fe_act_mask_i == f_act_mask)
570+
);
571+
assume property (@(posedge clk_i) disable iff (!rst_ni)
572+
!fetcher_request_matches_f_pc || (fe_warp_id_i == f_warp_id)
573+
);
574+
assume property (@(posedge clk_i) disable iff (!rst_ni)
575+
!fetcher_request_matches_f_pc || (fe_subwarp_id_i == f_subwarp_id)
576+
);
577+
578+
// Assert that valid cachelines that match the assumed memory address return the correct data
579+
cache_addr_t [NumCachelines-1:0] cacheline_addrs;
580+
logic [NumCachelines-1:0] cacheline_matches;
581+
for (genvar i = 0; i < NumCachelines; i++) begin : gen_cacheline_addrs
582+
assign cacheline_addrs[i] = {
583+
i_tag_mem.sram[i],
584+
cache_select_t'(i)
585+
};
586+
assign cacheline_matches[i] = (cacheline_addrs[i] == f_mem_addr) && cache_valids_q[i];
587+
588+
assert property (@(posedge clk_i) disable iff (!rst_ni)
589+
!(cacheline_matches[i]) || (f_mem_data == i_inst_mem.sram[i])
590+
) else $fatal(1, "Memory data does not match cache data for matching addresses.");
591+
end
592+
593+
logic request_matches_addr;
594+
assign request_matches_addr = mem_valid_i
595+
&& (fv_mem_addr_shift[FormalMemLatency-1] == f_mem_addr);
596+
assume property (@(posedge clk_i) disable iff (!rst_ni)
597+
!request_matches_addr || (mem_data_i == f_mem_data)
598+
) else $fatal(1, "Memory data does not match assumed data.");
599+
600+
// If instruction has the same address as our assumed memory address, the data must match
601+
logic result_matches_mem_addr;
602+
assign result_matches_mem_addr = ic_valid_o
603+
&& (ic_pc_o[PcWidth-1:CachelineIdxBits] == f_mem_addr);
604+
enc_inst_t result_exp_inst;
605+
assign result_exp_inst = f_mem_data[
606+
ic_pc_o[CachelineIdxBits-1:0]
607+
];
608+
assert property (@(posedge clk_i) disable iff (!rst_ni)
609+
!result_matches_mem_addr || (ic_inst_o == result_exp_inst)
610+
) else $fatal(1, "Instruction data does not match memory data for matching addresses.");
611+
612+
// Other signals must also match the f_* signals
613+
assert property (@(posedge clk_i) disable iff (!rst_ni)
614+
!result_matches_mem_addr || (ic_act_mask_o == f_act_mask)
615+
) else $fatal(1, "Active mask does not match assumed data.");
616+
assert property (@(posedge clk_i) disable iff (!rst_ni)
617+
!result_matches_mem_addr || (ic_warp_id_o == f_warp_id)
618+
) else $fatal(1, "Warp ID does not match assumed data.");
619+
assert property (@(posedge clk_i) disable iff (!rst_ni)
620+
!result_matches_mem_addr || (ic_subwarp_id_o == f_subwarp_id)
621+
) else $fatal(1, "Subwarp ID does not match assumed data.");
622+
623+
logic active_req_matches_mem_addr;
624+
assign active_req_matches_mem_addr =
625+
(active_req_q.pc[PcWidth-1:CachelineIdxBits] == f_mem_addr);
626+
627+
// Cache miss -> data came from memory
628+
assert property (@(posedge clk_i) disable iff (!rst_ni)
629+
!(active_req_matches_mem_addr && state_q == WAIT_FOR_DECODER)
630+
|| (mem_data_q == f_mem_data)
631+
) else $fatal(1, "Stored memory data does not match assumed data.");
632+
633+
// Data in active request must match f_* signals
634+
assert property (@(posedge clk_i) disable iff (!rst_ni)
635+
!(active_req_matches_mem_addr && (state_q != IDLE))
636+
|| (active_req_q.act_mask == f_act_mask)
637+
) else $fatal(1, "Active mask does not match assumed data on cache miss.");
638+
639+
assert property (@(posedge clk_i) disable iff (!rst_ni)
640+
!(active_req_matches_mem_addr && (state_q != IDLE))
641+
|| (active_req_q.warp_id == f_warp_id)
642+
) else $fatal(1, "Warp ID does not match assumed data on cache miss.");
643+
644+
assert property (@(posedge clk_i) disable iff (!rst_ni)
645+
!(active_req_matches_mem_addr && (state_q != IDLE))
646+
|| (active_req_q.subwarp_id == f_subwarp_id)
647+
) else $fatal(1, "Subwarp ID does not match assumed data on cache miss.");
648+
649+
// Cache hit -> data came from cache
650+
logic cache_hit_matches_mem_addr;
651+
assign cache_hit_matches_mem_addr = cache_valid_q
652+
&& (cache_tag_q == active_req_q.pc[PcWidth-1-:CacheTagBits])
653+
&& active_req_matches_mem_addr;
654+
655+
assert property (@(posedge clk_i) disable iff (!rst_ni)
656+
!(state_q == HANDLE_INSTR && ic_valid_o && cache_hit_matches_mem_addr)
657+
|| (cache_data == f_mem_data)
658+
) else $fatal(1, "Cache data does not match assumed data.");
537659
`endif
538660

539661
endmodule : instruction_cache

0 commit comments

Comments
 (0)