Assertion for checking connectivity

SystemVerilog
,
1

write an assertion to check connectivity between two signals. E.g, Signal a= signal b.
Property should be reusable.

2

Hi,
The below definition meets your requirement and it is reusable as well.


property ppt(bit x, bit y);
	@(x) y==x;
endproperty
	
AB: assert property (ppt(a,b));

CD: assert property (ppt(c,d));

Hope this helps.
Putta Satish

3

In reply to puttasatish:

Dear Satish,

I’m getting Syntax errors. please let me know the full code.

4

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
5

In reply to Alokpati:

Hey, i do not think sva are meant to be used for connectivity check because:

  1. Using a clocked property you are adding load to the entire simulation
  2. There are tools that runs connectivity checks for you diving into the hier
  3. The clocked properties on your side are free running meaning that will check the equality every time eval point, instead connectivity checks claims: a change of a specific signal should propagate up to the load through the hier.

Anyway if you do not have clock dep then i would suggest:

Always_comb
Con_ck: assert #0 y==x; else $error(“connectivity not satisfied”);

If the context requires a clock then there is not choice rather then using a property but i would say trigger your property only when the driver changes (not using a @x bit like !stable in one or more cycle before activating the property)

Regards

6

In reply to Rsignori92:

Yes… There are tools to do the connectivity check. And if assertion is required to be added then immediate assertion, using

always_comb

would be a good approach. But writing concurrent assertion must require clock otherwise it will miss the CASE_2 mentioned in my earlier reply.