How to verify whether the RAM model is correct?

hi,

In my design the verilog model of RAM. This model is only a behavior model and it aims to make the design functionally work. For synthesis, another ram model is used to replace this verilog model. The problem I'm facing is how to verify whether the synthesis ram model (real ram code) has the same behavior as the verilog model? If there are mismatches, the design will have faults when use the real ram model.

I think the following approaches can work for this:
* netlist simulation ----> drawback is could be time consuming, and can only run a limited number of tests
* run simulation with design RTL + synthesis ram code ----> drawback is only run a limited number of tests

Both the two approaches cannot provide sufficient testing vs. ram behavior model vs. synthesis model. Do you have better suggestions? Would formal equivalence checking or formal verification approaches help on this?

Thanks.

Well for simulation, the verilog RAM model are usually quite simple to understand and to check versus the data sheet.
Could you clarify which RAM verilog model you used for synthesis? the synthesis tool need a liberty file, no?
And the liberty file is also "quite" simple. A liberty describe timing arc between i/o which also available on data sheet.

Which is your provider, perhap someone else have some experiences with?