Hi,
I was wondering what is the best methodology for verifying a cache deep inside the design. Are there any specific methods / methodologies which can ensure that we have verified the cache functionality (reference counting, eviction, invalidation any livelocks etc) fully ?
I wanted to know of any methods other than white box verification.
Thanks in advance,
Madhu
One method is to use a black box approach with assertions written in the SystemVerilog Interface block. I demonstrate this concept in my SystemVerilog Assertions Handbook; thus,
// Example of requirements
//In the event of a cache read miss,
//the read request for the same address must be forwarded to the main memory within five clocks.
// Uding a module for demo:
module cache_mem;
timeunit 1ns;
timeprecision 1ns;
logic clk, cache_mem, cache_miss, main_mem_rd, cache_rd, reset_n;
int rd_addr, main_mem_rd_addr;
property p_cache_miss_2_main_mem_xfer (
cache_read, // read from cache control
cache_miss, // miss control from cache controller
rd_addr, // desired data address
main_mem_rd, // main memory read control
main_mem_rd_addr, // main memory read address
reset_n); // active low reset
int v_rd_addr_at_cache; // assertion variable to record and test the read address
disable iff (!reset_n) // abort if reset_n==0
((cache_read && cache_miss), v_rd_addr_at_cache =rd_addr) |=>
##[0:5] main_mem_rd && (main_mem_rd_addr == v_rd_addr_at_cache);
endproperty : p_cache_miss_2_main_mem_xfer
default clocking @(negedge clk);
endclocking
ap_cache_miss_2_main_mem_xfer : assert property // property instantiation
(@(posedge clk) p_cache_miss_2_main_mem_xfer ( cache_rd, cache_miss,
rd_addr, main_mem_rd, main_mem_rd_addr, reset_n));
endmodule : cache_mem
Another example using assertions
// For example, in a write-back policy-based cache coherency controller,
// once a write request to an address is found in the cache (i.e. a write hit),
// the following sequences of events should occur (possibly at varied time intervals):
// • The line is marked as “dirty”.
// • Any other caches having a copy of this address shall mark their copies as invalid.
// • Eventually, the dirty line shall be cleaned – i.e. modified data shall be written back to main memory.
module cache_wr_hit;
`define DIRTY 1'b0
`define INVALIDATE 1'b0
bit clk, bus_req, ack, cache_hit, wr;
typedef bit[15:0] data_t;
bit[9:0] addr_write;
data_t wr_data;
data_t[0:1023] cache, remote_cache;
default clocking cb_clk @ (posedge clk);
endclocking
sequence q_wr_hit;
@ (posedge clk) first_match(wr ##[1:2] cache_hit);
endsequence : q_wr_hit
sequence q_invalidate;
bus_req ##[1:2] ack ##1 remote_cache[addr_write]== `INVALIDATE;
endsequence : q_invalidate
ap_wr_hit: assert property(
q_wr_hit.triggered |=>
first_match(cache[addr_write] == `DIRTY ##1 q_invalidate
##[1:$] cache[addr_write]==wr_data) |->
remote_cache[addr_write]==wr_data
);
endmodule : cache_wr_hit
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks for the response. Could you point me to the book. I would be interested to read further and try out.
Thanks,
Madhu
In reply to mseyunni:
My book is “SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6”
However, the book is more about how to write assertions. and I used several examples and models to explain the concepts.
Thanks,
Ben
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us