AXI ARID issues multiple reads and device responds with data out of order with matching RID.
Is there an assertion code to check if master is reusing an ARID of an outstanding read?
In reply to cmtanbon:
Looking at the generic question: assertion code to check if master is reusing an ARID of an outstanding read?, I am suggesting the use of associative arrays to store the address and later on check if it was used. It was a long time ago since I looked at the protocol, thus I am giving you a generic response that I demonstrated in my SVA 4th Edition book.
Data Integrity in memory: data read from memory should be same as what was last written
Given a large memory (or a port), the following properties must be verified:
- Data should never be read before it is first written; thus only valid data must be read.
- Data read from the memory is what was last written into it.
Data integrity can easily be checked using a scoreboard that emulates the behavior of the DUT’s memory, and then compare the read data results of both memories. However, because the DUT memory is very large, using a memory for the scoreboard can be expensive in terms of resources used by the simulator. In this solution, an associative array is used to maintain the scoreboarding because it is more efficient. This model also brings up some interesting issues in the construction of properties.
Here are the assertions
// If a write, save addr into v_wraddr, save data write into v_wraadata
// if at some time we have a read, and the address exists in the associative array
// and the address is the one used in a previous write then
// the IO eddata==what was previously written
property p_read_after_write;
bit [31:0] v_wraadata, v_wraddr;
(write, v_wraddr=addr, v_wraadata= wdata) |-> // if write, save data and addr
(read && mem_aarray_exists && addr==v_wraddr) [->1] |-> // @read and data there at same written addr
rddata==v_wraadata; // *** read data from IO is same as what was written
endproperty : p_read_after_write
ap_read_after_write : assert property (p_read_after_write)
$info("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata)); else
$error("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata));
property p_read_before_write;
not (read && !mem_aarray_exists); // never a read on an non written address
endproperty : p_read_before_write
ap_read_before_write : assert property (p_read_before_write);
Full code
module memory_data_integrity_check (
input bit write, // memory write
input bit read, // memory read
input bit[31:0] wdata, // data written to memory
input bit [31:0] rddata, // ** NEW: data read from memory
input bit[31:0] addr, // memory address -- small for simulation
input bit reset_n, // active low reset
input bit clk); // clock
timeunit 1ns; timeprecision 100ps;
default clocking cb_clk @ (posedge clk); endclocking
int mem_aarray[*]; // associative array (AA) to be used by property
bit [31:0] raadata; // data read from AA
bit mem_aarray_exists; // exists at specified address
assign mem_aarray_exists = mem_aarray.exists(addr);
always_comb
if(mem_aarray_exists)
raadata = mem_aarray[addr]; //
always@ (posedge clk)
if (reset_n==1'b0) mem_aarray.delete; // Clears AA elements
else if (write) mem_aarray[addr] = wdata; // store data
// If a write, save addr into v_wraddr, save data write into v_wraadata
// if at some time we have a read, and the address exists in the associative array
// and the address is the one used in a previous write then
// the IO eddata==what was previously written
property p_read_after_write;
bit [31:0] v_wraadata, v_wraddr;
(write, v_wraddr=addr, v_wraadata= wdata) |-> // if write, save data and addr
(read && mem_aarray_exists && addr==v_wraddr) [->1] |-> // @read and data there at same written addr
rddata==v_wraadata; // *** read data from IO is same as what was written
endproperty : p_read_after_write
ap_read_after_write : assert property (p_read_after_write)
$info("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata)); else
$error("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata));
property p_read_before_write;
not (read && !mem_aarray_exists); // never a read on an non written address
endproperty : p_read_before_write
ap_read_before_write : assert property (p_read_before_write);
endmodule : memory_data_integrity_check
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
thanks for the information. how about more specific to ARID functionality wrt assertion checks? how would this be implemented?