In reply to puttasatish:
property ppt(bit x, bit y);
@(x) y==x;
endproperty
AB: assert property (ppt(a,b));
AC: assert property (ppt(a,c));
this assertion will work well when ‘a’ is toggling from 0->1 and 1->0 … CASE-1
But, assertion will not work if ‘a’ is toggling only once… CASE-2
bit a,b,c;
//'b' is driven by 'a', 'c' doesn't have any driver
assign b = a;
CASE-1
…t1…t2…
a |‘’‘’|__
b |‘’‘’|__
c ______________
at t1, AC will pass as captured value for both a & c are 0
at t2, AC will fail as captured value for a=1 & c=0
CASE-2
…t1…
a ___|‘’‘’‘’‘’‘’’
b ___|‘’‘’‘’‘’‘’’
c _______________
at t1, AC will pass as captured value for both a & c are 0
‘a’ is not toggling further, so property can’t be invoked again to check the connectivity.
better approach to write connectivity check will be to incorporate clock also.
module top();
bit clk;
bit a,b,c,d;
always #1 clk = !clk;
initial begin
#3; a = 1;
//#5; a = 0;
//#8; a = 1;
//#2; a = 0;
#5; $finish;
end
assign b = a;
//assign #1 c = a;
property ppt(x, y);
@(x) y==x;
endproperty
property ppt1(clk, x, y);
@(clk) y==x;
endproperty
AB: assert property (ppt(a,b));
AC: assert property (ppt(a,c));
AB1: assert property (ppt1(clk,a,b));
AC1: assert property (ppt1(clk,a,c));
endmodule