SystemVerilog assertions in synthesized design

SystemVerilog
, , ,
1

Hello,
I used SystemVerilog Assertions (SVA ) to verify my design in simulation.
Now the problem is the post-synthesis verification. I want to make sure that the synthesized design behaves exactly as it was during the simulation in for functional verification.
**Is it possible to used SVA to verify the synthesized design?

**Any suggestion is warm welcomed.

Thanks.

2

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

3

In reply to basheer55:

Thank you Mr. Baser

I appreciate your explanation. This helps a lot.
I normally write SVA assertions in separate modules.

Thanks once again.

Victor

4

Hate to necro this thread, but is this still the best solution?

Do synthesis tools still not preserve assertions, or is there a way to have the synthesis tools transform the assertions for use in a post synthesis netlist?

5

In reply to basheer55:

Thanks for this. So it seems XMRs won’t work with QFormal either. Maybe there is a magic switch that I haven’t found yet to enable this somehow? I’m working to integrate the RISC-V formal interface (RVFI) into a 5 stage RISC-V pipeline and need XMRs to get all that’s needed for that, collecting bits and pieces from within the RTL. I’d hate to have to hack up the DUT RTL (not my RTL) to punch thru all the signals I need up to the top…