In reply to ben@SystemVerilog.us:
I made corrections to the code. I used 2 methods
* Uses associative array to store the last data written
* Stores data on write into a local variable. Another write to same address
causes the active assertion to be vacuous. A new asn is initiated with
that new write.
/*
Code for use with the book
"SystemVerilog Assertions Handbook, 2nd edition"ISBN 878-0-9705394-8-7
*/
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), $s ampled(raadata)); else
$error("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata));
// ** METHOD 2. Vacuity if 2nd write to same address
// NO associative array usage
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
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
Ben Cohen
http://www.systemverilog.us/
For training, consulting, services: contact
http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
...
1) SVA Package: Dynamic and range delays and repeats
https://rb.gy/a89jlh
2) Free books: Component Design by Example
https://rb.gy/9tcbhl
Real Chip Design and Verification Using Verilog and VHDL($3)
https://rb.gy/cwy7nb
3) Papers:
- Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
