In reply to vk7715:
The bind construct is just a syntactic shortcut making it easier to add assertions if that is what works for you.
//`define USE_BIND
module tb_top;
bit clk;
initial repeat(10) #5 clk=!clk;
device dut(.*);
`ifdef USE_BIND
bind subunit sva_module s(.clk, .A(sig1),.B(sig2));
`else
sva_module sva1(dut.u1.clk, dut.u1.sig1,dut.u1.sig2);
sva_module sva2(dut.u2.clk, dut.u2.sig1,dut.u2.sig2);
sva_module svaN(dut.uN.clk, dut.uN.sig1,dut.uN.sig2);
`endif
endmodule
module device(input bit clk);
subunit u1(.*);
subunit u2(.*);
subunit uN(.*);
endmodule
module subunit(input bit clk);
wire sig1=0,sig2=1;
endmodule
module sva_module(input bit clk, wire A,B);
A1: assert property (@(posedge clk) A == B);
A2: assert property (@(posedge clk) B == A);
endmodule
You should try this both ways and look at the differences in the reported paths. The you can try different methods of controlling assertions.