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?
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