13 always @(posedge rc) begin
17 always @(posedge wc) begin
18 if (we) mem[wa] <= wd;
43 reg [3:0] shadow_data;
44 (* anyconst *) reg [3:0] shadow_addr;
49 always @(posedge gclk) begin
51 assume ($stable(rc) || $stable(wc));
53 if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin
54 assert (shadow_data == rd);
57 if ($rose(wc) && $past(we) && shadow_addr == $past(wa)) begin
58 shadow_data <= $past(wd);