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.