I want to write an assertion for the below requirement.
Requirement:
AWPROT[0] value should be stored at one clock tick with AWID and should be compared with TPROT[0] after a certain(random) clock ticks with the same TWID.
I am trying to use an associative array but It is not helping out. Also tried the same approach with the queue but no luck.
Thanks for the prompt response.
If a local variable doesn’t accumulate values, Is there any way that can store value at one clock tick and we can use it to compare on any other clock tick?
Using an assertion woth ultple antecedents is not recommended.
a |-> seq |-> seq2 // not recommended
here is an example of assertions using associative arrays for simulation.
From my SVA book
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
// ** Using an associative array to store the last data written **
// If a write, save addr into v_wraddr, data is saved into the associative array
// by support logic.
// if at some time we have a read, and the address exists in the associative array
property p_read_after_write;
bit [31:0] v_wraddr;
(write, v_wraddr=addr) ##1 // if write, save data and addr
(read && mem_aarray_exists && addr==v_wraddr) [->1] |-> // @read and data there at same written addr
rddata==raadata; // *** 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));
// ** METHOD 2. Vacuity if 2nd write to same address
property p_read_after_1_write;
bit [31:0] v_wraadata, v_wraddr;
(write, v_wraddr=addr, v_wraadata= wdata) ##1 // if write, save data and addr
(!write && addr==v_wraddr)[*1:$] ##1 (read && addr==v_wraddr) [->1]
// @read and data there at same written addr
// and NO 2nd write to same address
|-> rddata==v_wraadata; // *** read data from IO is same as what was written
endproperty : p_read_after_1_write
ap_read_after_1_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
// *** Testbench needs to be updated, it is not correct
class c_xactn;
rand bit write; // memory write
rand bit read; // memory read
rand int wdata; // data written to memory
rand bit[31:0] addr; // memory address
rand bit [31:0] rddata; // memory data
constraint addr_range_cst { addr dist {111:=1, 2222:=1};} //, 3333:=1};}
constraint no_wr_and_rd_cst { !(read && write);}
constraint rddata_cst {rddata dist {32'hF:=1, 32'hFFFF:=1};} //, 32'hFFFF:=1};}
constraint wrdata_cst {wdata dist {32'hF:=1, 32'hFFFF:=1};} //, 32'hFFFF:=1};}
endclass : c_xactn
module top;
timeunit 1ns; timeprecision 100ps;
bit write; // memory write
bit read; // memory read
int wdata; // data written to memory
bit [31:0] rddata; // memory data
bit[31:0] addr; // memory address
bit reset_n=1'b1; // active low reset
bit clk=1'b1; // clock
// Because you have used “c1” as a variable name and a block name.
// Normal search rules say the block name hides the name of the variable name.
c_xactn c1;
memory_data_integrity_check mem_check1 (.*);
initial forever #5 clk=!clk;
initial begin : i1
c1=new();
repeat(300) begin :r1
@ (posedge clk) begin :cl1
if(!c1.randomize()) $error("c1 randomization failure");
write <= c1.write;
read <= c1.read;
wdata <= c1.wdata;
addr <= c1.addr;
rddata <= c1.rddata;
end :cl1
end :r1
$finish;
end : i1
endmodule : top
en Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
You don’t need associative array. Keep in mind that assertion is parallel process. That is, different check processes are invoked every time whenever the condition AVALID && AREADY meets.