• Skip to main content
  • Skip to search
  • Skip to footer
Cadence Home
  • This search text may be transcribed, used, stored, or accessed by our third-party service providers per our Cookie Policy and Privacy Policy.

  1. Community Forums
  2. Logic Design
  3. Help: memory equivalence check between RTL and schemati...

Stats

  • Locked Locked
  • Replies 3
  • Subscribers 63
  • Views 14566
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

Help: memory equivalence check between RTL and schematic

WorldMaker
WorldMaker over 15 years ago

Hi,

It mentions that encounter conformal equivalence checker can do memory equivalence check between schematic and RTL, but I cannot any example or demo. Is there anyone can demo how to do memory EC? I am wondering how the EC engine deal with the bit-cell array, treating it as black box and ignoring it? or the EC engine abstract the bit-cell schematic into latch and compare the abstracted memory verilog with the memory primitive?

Can the replica bit-line style memory be checked by EC?

thanks,

Worldmaker

  • Cancel
Parents
  • WorldMaker
    WorldMaker over 15 years ago

    Hi Sean,

    I am trying to check the equivalence between the schematic and the RTL simulation model for custom memories which has testing logic designed inside (traditionally, we model the ram as flop in RTL simulations). As you mentioned, Conformal GXL can generate a verplex memory model which is actually the memory core using the GXL memory primitives. Now we can build a wrapper model which instances the generated verplex model and the testing logic. Can Conformal GXL check the equivalence between the wrapper model and the RTL simulation model? If yes, both the memory core and testing logic are verified. If not, can the testing logic be verified seperately by black boxing the memory core?

    Could you please demo a "dofile" which can fulfil the task or point me to somewhere where I can find some similar demos? I cannot log onto the sourcelink now, and thus I cannot check if there are similar demos on sourcelink.

    Here is an example RTL simulation model for a dual port SRAM:

    /////////////////////////////////////////////////////////////////////

    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

    • Cancel
    • Vote Up 0 Vote Down
    • Cancel
Reply
  • WorldMaker
    WorldMaker over 15 years ago

    Hi Sean,

    I am trying to check the equivalence between the schematic and the RTL simulation model for custom memories which has testing logic designed inside (traditionally, we model the ram as flop in RTL simulations). As you mentioned, Conformal GXL can generate a verplex memory model which is actually the memory core using the GXL memory primitives. Now we can build a wrapper model which instances the generated verplex model and the testing logic. Can Conformal GXL check the equivalence between the wrapper model and the RTL simulation model? If yes, both the memory core and testing logic are verified. If not, can the testing logic be verified seperately by black boxing the memory core?

    Could you please demo a "dofile" which can fulfil the task or point me to somewhere where I can find some similar demos? I cannot log onto the sourcelink now, and thus I cannot check if there are similar demos on sourcelink.

    Here is an example RTL simulation model for a dual port SRAM:

    /////////////////////////////////////////////////////////////////////

    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

    • Cancel
    • Vote Up 0 Vote Down
    • Cancel
Children
No Data

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.

© 2025 Cadence Design Systems, Inc. All Rights Reserved.

  • Terms of Use
  • Privacy
  • Cookie Policy
  • US Trademarks
  • Do Not Sell or Share My Personal Information