SystemVerilog bind assertion sequence with variable

Question

I have to write a SystemVerilog assertion with binding.

The assertion should be something like:

assert property (@(posedge (mod_clk & clk_gen_enable)) ##delay (clk_sync == 1));

mod_clk, clk_gen_en and clk_sync are signals of the module which I bind to, and delay is a variable which is a result of a calculation and should be in "units" of st_clk, which is also signal of the module which I bind to.

How can I write it correctly?

Answer 1

For bind to work, all you need is encapsulate this assertion in a module

module my_module;
assert property (@(posedge (mod_clk & clk_gen_enable)) ##delay (clk_sync == 1));
endmodule

Then use the bind construct to insert my_module into your target module. Verilog search rules will search upwards to find your signal names.

bind my_target_module my_module my_instance_name();

##delay works on the clock edge you specified before it which you have as mod_clk & clk_gen_enable. I'm guessing you really mean to have clk_gen_enable as an implication.

property sync;
  int counter;
  @(posedge mod_clk) (clk_gen_enable, counter=delay)
        |-> @(posedge st_clk) (1,counter--)[*0:$] ##1 counter<0 ##0 (clk_sync == 1));
endproperty