docs/examples/multiclk/dpmem.sv

   1 module dpmem (
   2         input            rc,
   3         input      [3:0] ra,
   4         output reg [3:0] rd,
   5
   6         input            wc,
   7         input            we,
   8         input      [3:0] wa,
   9         input      [3:0] wd
  10 );
  11         reg [3:0] mem [0:15];
  12
  13         always @(posedge rc) begin
  14                 rd <= mem[ra];
  15         end
  16
  17         always @(posedge wc) begin
  18                 if (we) mem[wa] <= wd;
  19         end
  20 endmodule
  21
  22 module top (
  23         input            rc,
  24         input      [3:0] ra,
  25         output     [3:0] rd,
  26
  27         input            wc,
  28         input            we,
  29         input      [3:0] wa,
  30         input      [3:0] wd
  31 );
  32         dpmem uut (
  33                 .rc(rc),
  34                 .ra(ra),
  35                 .rd(rd),
  36                 .wc(wc),
  37                 .we(we),
  38                 .wa(wa),
  39                 .wd(wd)
  40         );
  41
  42         reg shadow_valid = 0;
  43         reg [3:0] shadow_data;
  44         (* anyconst *) reg [3:0] shadow_addr;
  45
  46         reg init = 1;
  47         (* gclk *) reg gclk;
  48
  49         always @(posedge gclk) begin
  50                 assume ($stable(rc) || $stable(wc));
  51
  52                 if (!init) begin
  53                         if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin
  54                                 assert (shadow_data == rd);
  55                         end
  56
  57                         if ($rose(wc) && $past(we) && shadow_addr == $past(wa)) begin
  58                                 shadow_data <= $past(wd);
  59                                 shadow_valid <= 1;
  60                         end
  61                 end
  62
  63                 init <= 0;
  64         end
  65 endmodule