Hi all,
I have written an assertion as below:
property data_check (int WIDTH, logic [31:0] address1, logic [31:0] address2, logic [31:0] address3, logic [31:0] address4, logic [31:0] signal_to_check_temp);
@(clk)
(($rose(write_cycle) && ((ADDR == address1) || (ADDR == address2) || (ADDR == address3) || (ADDR == address4) || (ADDR == 'h1234))),save_data()) |->
if (ADDR == 'h1234)
first_match (##[1:5] ((signal_to_check_temp == wdata_f0[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata_f1[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata[(WIDTH-1):0]) ||
(signal_to_check_temp == 0))) ##1
(((signal_to_check_temp == wdata_f0[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata_f1[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata[(WIDTH-1):0]) ||
(signal_to_check_temp == 0)) [*1:$] ##1
($rose(write_cycle) && ((ADDR == address1) ||
(ADDR == address2) ||
(ADDR == address3) ||
(ADDR == address4) ||
(ADDR == 'h1234))))
else
first_match (##[1:5] signal_to_check_temp == wdata[(WIDTH-1):0]) ##1 ((signal_to_check_temp == wdata[(WIDTH-1):0]) [*1:$] ##[1:6] ($rose(write_cycle) && ((ADDR == address1) || (ADDR == address2) || (ADDR == address3) || (ADDR == address4) || (ADDR == 'h1234))));
endproperty
Now I have asserted the property two times for 2 different set of arguments and signals as shown below:
inst1 : assert property (data_check (//all arguments set 1)) else $error();
inst2 : assert property (data_check (//all arguments set 2)) else $error();
While asserting the property only for 1 set of args (either set 1 or 2), the assertion works fine. But when these 2 are asserted then the assertion fails at many time stamps. Why this kind of behaviour? Is there any kind of dependency on both these instances?
In reply to atanubiswas:
save_data() function may be the culprit. Both the property might be sharing the same resource in this function.
In reply to Rahulkumar Patel:
In reply to atanubiswas:
save_data() function may be the culprit. Both the property might be sharing the same resource in this function.
Hi Rahul,
I checked it and you are correct. Is there any solution for that? I tried using automatic keyword for the function save_data… still the problem persists.
In reply to atanubiswas:
Hi Rahul,
I checked it and you are correct. Is there any solution for that? I tried using automatic keyword for the function save_data… still the problem persists.
Only variables declared inside the automatic function are automatic. your function still might be using some other variables which declared outside the function which are still common for both the property call.
In reply to Rahulkumar Patel:
The function save_data was doing the following:
function automatic void save_data();
wdata = DATA;
if (//condition)
wdata_f0 = DATA;
else if (//condition)
wdata_f1 = DATA;
endfunction
So now I moved it to the assertion property as shown below:
property data_check (int WIDTH, logic [31:0] address1, logic [31:0] address2, logic [31:0] address3, logic [31:0] address4, logic [31:0] signal_to_check_temp);
//initialization
int wdata = 0;
int wdata_f0 = 0;
int wdata_f1 = 0;
@(clk)
(($rose(write_cycle) && ((ADDR == address1) || (ADDR == address2) || (ADDR == address3) || (ADDR == address4) || (ADDR == 'h1234))),
wdata = DATA,
wdata_f0 = (//condition) ? DATA : wdata_f0,
wdata_f1 = (//condition) ? DATA : wdata_f1
) |->
if (ADDR == 'h1234)
first_match (##[1:5] ((signal_to_check_temp == wdata_f0[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata_f1[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata[(WIDTH-1):0]) ||
(signal_to_check_temp == 0))) ##1
(((signal_to_check_temp == wdata_f0[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata_f1[(WIDTH-1):0]) ||
(signal_to_check_temp == wdata[(WIDTH-1):0]) ||
(signal_to_check_temp == 0)) [*1:$] ##1
($rose(write_cycle) && ((ADDR == address1) ||
(ADDR == address2) ||
(ADDR == address3) ||
(ADDR == address4) ||
(ADDR == 'h1234))))
else
first_match (##[1:5] signal_to_check_temp == wdata[(WIDTH-1):0]) ##1 ((signal_to_check_temp == wdata[(WIDTH-1):0]) [*1:$] ##[1:6] ($rose(write_cycle) && ((ADDR == address1) || (ADDR == address2) || (ADDR == address3) || (ADDR == address4) || (ADDR == 'h1234))));
endproperty
But the assertion fails due to the initialization part inside the property. Had to do the initialization because I was getting compilation errors that the property variable has been assigned before getting initialized. Am I making some mistake in replicating that subroutine logic inside my property?