memory LEC

Hi all,

We always model the RAM as a flop in RTL simulation, can verplex LEC check the equivalence between the RAM RTL(shown below) and the RTL using verplex built-in RAM primitives?

/////////////Example/////////////////////////////////////////////////////

module mem2p (wclk,wadr,wdin,rclk,radr,rdout);

parameter adrbits=7;

parameter databits=8;

parameter adrmax = (1<<adrbits)-1;

input wclk;

input [adrbits-1:0] wadr;

input[databits-1:0] wdin;

input rclk;

input [adrbits-1:0] radr;

output[databits-1:0] rdout;

reg[databits-1:0] rdout;

reg[databits-1:0] mem[0:adrmax];

always @(negedge wclk) mem[wadr] = wdin;

always @(posedge rclk) rdout=mem[radr];

endmodule

thanks,

worldmaker