In reply to vico:
When writing SVA in RTL level, you should write the SVA assertions into a separate module and use bind to bind the assertions into the selected instance/module in your design.
If you do this way, later you can re-use the SVA that written into separate module and re-bind them to the signals that has been changed in your netlist. The most hard part is to find a equivalent signals of the post-synthesis with the pre-synthesis RTL.
But, if you keep minimum flattening option, the hierarchy that you have in pre-synthesis should be as same as your pre-synthesis RTL. Then then same binding should work as it is.
But, if you are using any internal wire/reg/logic under a module in your SVA, then you need to re-map them with the new signal name of the post synthesis netlist.
Hence, you should AVOID of writing a SVA definition module as below BAD example(where it is using a XMR of a signals under the module it is going to be bound in to).
A module that will be an instance under top DUT:
module mydut(
input clk,
input rst_n,
input data_in,
output data_out
);
mydut_aa u_inst (...);
Bad SVA module example:
module mydut_sva (
input clk,
input rst_n,
input data_in,
input data_out
);
MY_ASSERTION_A : assert property (@(posedge clk) disable iff (!rst_n) (u_inst.sig_a != data_in));
// referring to a internal signal u_inst.sig_a can be written as above.
// This will work in RTL. But, this signal will change in netlist.
// Hence, the reuse is not possible.
Good SVA module example:
module mydut_sva (
input clk,
input rst_n,
input data_in,
input data_out,
input u_inst_sig // declare a port to be connected to the signal of a internal hierarchy.
);
MY_ASSERTION_A : assert property (@(posedge clk) disable iff (!rst_n) (u_inst_sig_a != data_in));
Bind syntax for above good example in RTL mode:
bind mydut mydut_sva (
.u_inst_sig (u_inst.sig),
.*);
Bind syntax for above good example in netlist mode with some hierarchy is preserved:
bind mydut mydut_sva (
.u_inst_sig (new.path.to.the.u_inst.sig),
.*);
Hope this helps.
-Baser