Stats

  • Locked Locked
  • Replies 3
  • Subscribers 63
  • Views 14564
  • 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

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

  • Hi Worldmaker, A quick question before I answer : Are you trying to verify your own custom memories? If yes, Conformal GXL can help. If you are designing/verifying your chip, and see instances of memories, then you should treat them as IPs thus black box them. For custom memory designs, memory equivalency check is done in three steps. First is to generate memory model for both equivalency checking and simulation purpose. Because traditional memory simulation models are not suitable for equivalence checking (due to structural difference in data/clock in sim latch vs wordline/bitline in schematic), user needs to use Conformal GXL memory primitive generator to help them develop a memory model that is both simulation/equivalency checking friendly. As a side note, you can also write structurally accurate simulation model (without using memory primitive), but that would incur big simulation runtime penalty. Second step is to abstract schematic. You are correct to say that abstraction engine will abstract the bit-cell schematic into latch. During this process, transistor netlist is transformed into a logic model (described in verilog primitives). By the way, Conformal GXL handles digital logic gates. Analog circuits, such as sense amplifiers may need special handling. Last step is to use Conformal equivalency checking to verify that RTL model and schematic abstraction is equivalent. During this step, Conformal will look at the memory primitive in RTL, and correctly synthesize a structural memory model that can be equivalency checked to the abstracted view of the schematic. For more details, you can log onto: trainingondemand.cadence.com, sign in with sourcelink id, then check out "Conformal Custom Equivalence Checker Jumpstart". Thanks, Sean

  • 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

  • Hi WorldMaker, Yes, you should be able to compare two RTL designs, using Conformal equivalency checker. However, this depends on whether two designs have similar structure - ie logic cone at all end points has to match cycle by cycle. I would recommend black boxing the core memory array in both, and make sure the wrapper logic is equivalent. As for the documentation or demo, it's available at sourcelink, as well as the full documentation at Conformal installation/doc directory. Please contact myself or your Cadence contact and see if you can get a hold of one of the above. You can email me at 'surlung@cadence.com' Thanks, Sean

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.