Skip to content

Commit 35ec4cd

Browse files
TheMightyDuckOfDoomTheMightyDuckOfDoom
committed
formal: basic instruction_cache assertions
1 parent c358b99 commit 35ec4cd

File tree

9 files changed

+140
-57
lines changed

9 files changed

+140
-57
lines changed

‎Bender.yml‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -32,10 +32,6 @@ vendor_package:
3232
sources:
3333
- rtl/bgpu_pkg.sv
3434

35-
- target: formal
36-
files:
37-
- formal/fv_reset.sv
38-
3935
- target: not(any(post_synth, post_layout))
4036
files:
4137
- rtl/compute_unit/fetcher/warp_its_unit.sv

‎Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ formal-%: formal/formal.f formal/%.sby
7979
mkdir -p formal/work
8080
cd formal && sby $*.sby -f --prefix work/$*
8181

82-
formal: formal-tag_queue formal-reg_table
82+
formal: formal-tag_queue formal-reg_table formal-instruction_cache
8383

8484
####################################################################################################
8585
# Verilator simulation

‎formal/fv_reset.sv‎

Lines changed: 0 additions & 32 deletions
This file was deleted.

‎formal/instruction_cache.sby‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
[tasks]
2+
cover
3+
prove
4+
5+
[options]
6+
cover: mode cover
7+
prove: mode prove
8+
depth 20
9+
smtc startup_reset.smtc
10+
11+
[engines]
12+
smtbmc yices
13+
14+
[script]
15+
plugin -i slang-sva.so
16+
read_slang --top instruction_cache -F formal.f \
17+
--compat-mode --keep-hierarchy \
18+
--allow-use-before-declare --ignore-unknown-modules
19+
prep -top instruction_cache
20+
21+
[files]
22+
formal.f
23+
24+
[file startup_reset.smtc]
25+
initial
26+
assume (= [rst_ni] false)

‎formal/reg_table.sby‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ prove
66
cover: mode cover
77
prove: mode prove
88
depth 20
9+
smtc startup_reset.smtc
910

1011
[engines]
1112
smtbmc boolector
@@ -19,3 +20,7 @@ prep -top reg_table
1920

2021
[files]
2122
formal.f
23+
24+
[file startup_reset.smtc]
25+
initial
26+
assume (= [rst_ni] false)

‎formal/tag_queue.sby‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ prove
66
cover: mode cover
77
prove: mode prove
88
depth 20
9+
smtc startup_reset.smtc
910

1011
[engines]
1112
smtbmc boolector
@@ -19,3 +20,7 @@ prep -top tag_queue
1920

2021
[files]
2122
formal.f
23+
24+
[file startup_reset.smtc]
25+
initial
26+
assume (= [rst_ni] false)

‎rtl/compute_unit/dispatcher/reg_table.sv‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -372,13 +372,5 @@ module reg_table #(
372372
assume property (@(posedge clk_i) disable iff (!rst_ni)
373373
!(insert_i && space_available_o) || !(insert_tag_in_table))
374374
else $error("Assumption failed: Inserting tag %d that is already in the table", tag_i);
375-
376-
// Reset at beginning
377-
fv_reset #(
378-
.RESET_CYCLES( 1 )
379-
) i_fv_reset (
380-
.clk_i ( clk_i ),
381-
.rst_ni( rst_ni )
382-
);
383375
`endif
384376
endmodule : reg_table

‎rtl/compute_unit/dispatcher/tag_queue.sv‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -125,14 +125,6 @@ module tag_queue #(
125125

126126
// Can only free used tags
127127
assume property (@(posedge clk_i) disable iff (!rst_ni) free_i == tags_used_q[tag_i]);
128-
129-
// Reset at beginning
130-
fv_reset #(
131-
.RESET_CYCLES( 1 )
132-
) i_fv_reset (
133-
.clk_i ( clk_i ),
134-
.rst_ni( rst_ni )
135-
);
136128
`endif
137129

138130
endmodule : tag_queue

‎rtl/compute_unit/instruction_cache.sv‎

Lines changed: 103 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,11 @@ module instruction_cache #(
1414
/// Number of threads per warp
1515
parameter int unsigned WarpWidth = 32,
1616
/// Encoded instruction width
17-
parameter int unsigned EncInstWidth = 32,
17+
parameter int unsigned EncInstWidth = 4,
1818
/// Encoded instructions per cacheline -> Also determines the memory interface width
19-
parameter int unsigned CachelineIdxBits = 2,
19+
parameter int unsigned CachelineIdxBits = 1,
2020
/// Number of cachelines in the instruction cache
21-
parameter int unsigned NumCachelines = 8,
21+
parameter int unsigned NumCachelines = 2,
2222

2323
/// Dependent parameter, do **not** overwrite.
2424
parameter int unsigned SubwarpIdWidth = WarpWidth > 1 ? $clog2(WarpWidth) : 1,
@@ -431,10 +431,109 @@ module instruction_cache #(
431431
// # Assertions #
432432
// #######################################################################################
433433

434+
// TODO: These are not exhaustive
434435
`ifndef SYNTHESIS
436+
/// Check if new state is valid given the current state
437+
// From IDLE state
435438
assert property (@(posedge clk_i) disable iff (!rst_ni)
436-
mem_valid_i |-> state_q == WAIT_FOR_MEM
439+
!(state_q == IDLE) || (state_d == IDLE || state_d == HANDLE_INSTR)
440+
) else $fatal(1, "Invalid state transition from IDLE state to %0d", state_d);
441+
// From HANDLE_INSTR state
442+
assert property (@(posedge clk_i) disable iff (!rst_ni)
443+
!(state_q == HANDLE_INSTR) || (state_d == IDLE || state_d == HANDLE_INSTR
444+
|| state_d == WAIT_FOR_MEM)
445+
) else $fatal(1, "Invalid state transition from HANDLE_INSTR state to %0d", state_d);
446+
// From WAIT_FOR_MEM state
447+
assert property (@(posedge clk_i) disable iff (!rst_ni)
448+
!(state_q == WAIT_FOR_MEM) || (state_d == WAIT_FOR_MEM || state_d == WAIT_FOR_DECODER)
449+
) else $fatal(1, "Invalid state transition from WAIT_FOR_MEM state to %0d", state_d);
450+
// From WAIT_FOR_DECODER state
451+
assert property (@(posedge clk_i) disable iff (!rst_ni)
452+
!(state_q == WAIT_FOR_DECODER) || (state_d == IDLE || state_d == HANDLE_INSTR
453+
|| state_d == WAIT_FOR_DECODER)
454+
) else $fatal(1, "Invalid state transition from WAIT_FOR_DECODER state to %0d", state_d);
455+
456+
/// Memory interface assertions
457+
// Ensure that we only receive memory responses in the WAIT_FOR_MEM state
458+
assert property (@(posedge clk_i) disable iff (!rst_ni)
459+
!mem_valid_i || (state_q == WAIT_FOR_MEM)
437460
) else $fatal(1, "Memory response received, but not in WAIT_FOR_MEM state.");
461+
462+
// Ensure that we only send memory requests in the HANDLE_INSTR state
463+
assert property (@(posedge clk_i) disable iff (!rst_ni)
464+
!mem_req_o || (state_q == HANDLE_INSTR)
465+
) else $fatal(1, "Memory request sent, but not in HANDLE_INSTR state.");
466+
467+
// If we sent out a memory request, we must got to the WAIT_FOR_MEM state
468+
assert property (@(posedge clk_i) disable iff (!rst_ni)
469+
!(mem_req_o && mem_ready_i) || (state_d == WAIT_FOR_MEM)
470+
) else $fatal(1, "Memory request sent, but did not go to WAIT_FOR_MEM state.");
471+
`endif
472+
473+
// #######################################################################################
474+
// # Formal Properties #
475+
// #######################################################################################
476+
477+
`ifdef FORMAL
478+
/// Check that we can reach all states
479+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == IDLE));
480+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == HANDLE_INSTR));
481+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == WAIT_FOR_MEM));
482+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == WAIT_FOR_DECODER));
483+
484+
/// Check that we can perform all transitions
485+
// IDLE state
486+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == IDLE)
487+
&& (state_d == HANDLE_INSTR));
488+
// HANDLE_INSTR state
489+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == HANDLE_INSTR)
490+
&& (state_d == IDLE));
491+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == HANDLE_INSTR)
492+
&& (state_d == HANDLE_INSTR));
493+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == HANDLE_INSTR)
494+
&& (state_d == WAIT_FOR_MEM));
495+
// WAIT_FOR_MEM state
496+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == WAIT_FOR_MEM)
497+
&& (state_d == WAIT_FOR_MEM));
498+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == WAIT_FOR_MEM)
499+
&& (state_d == WAIT_FOR_DECODER));
500+
// WAIT_FOR_DECODER state
501+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == WAIT_FOR_DECODER)
502+
&& (state_d == IDLE));
503+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == WAIT_FOR_DECODER)
504+
&& (state_d == HANDLE_INSTR));
505+
cover property (@(posedge clk_i) disable iff (!rst_ni) (state_q == WAIT_FOR_DECODER)
506+
&& (state_d == WAIT_FOR_DECODER));
507+
508+
/// Cover Handshakes
509+
// Check that we can perform memory requests
510+
cover property (@(posedge clk_i) disable iff (!rst_ni) (mem_req_o && mem_ready_i));
511+
cover property (@(posedge clk_i) disable iff (!rst_ni) (!mem_req_o && mem_ready_i));
512+
// Check that we can receive a new instruction
513+
cover property (@(posedge clk_i) disable iff (!rst_ni) (fe_valid_i && ic_ready_o));
514+
cover property (@(posedge clk_i) disable iff (!rst_ni) (fe_valid_i && !ic_ready_o));
515+
// Check that we can send an instruction to the decoder
516+
cover property (@(posedge clk_i) disable iff (!rst_ni) (ic_valid_o && dec_ready_i));
517+
cover property (@(posedge clk_i) disable iff (!rst_ni) (!ic_valid_o && dec_ready_i));
518+
519+
/// Memory Latency Model
520+
localparam int unsigned FormalMemLatency = 5;
521+
logic [FormalMemLatency-1:0] mem_valid_shift;
522+
always_ff @(posedge clk_i or negedge rst_ni) begin
523+
if (!rst_ni) begin
524+
mem_valid_shift <= '0;
525+
end else begin
526+
mem_valid_shift <= {mem_valid_shift[FormalMemLatency-2:0],
527+
mem_req_o && mem_ready_i};
528+
end
529+
end
530+
531+
// Memory valid signal must be delayed version of mem_req_o && mem_ready_i
532+
assume property (@(posedge clk_i) disable iff (!rst_ni)
533+
(mem_valid_i == mem_valid_shift[FormalMemLatency-1]));
534+
535+
// There can only be one active memory request at a time
536+
assert property (@(posedge clk_i) $onehot0(mem_valid_shift));
438537
`endif
439538

440539
endmodule : instruction_cache

0 commit comments

Comments
 (0)