Assigning a bit in SV Assertion

SystemVerilog
, , ,
21

Hi Ben,

In the below property I am trying to make some assignment as shown below after $rose(write_cycle):

property data_check;
logic [15:0] temp_data1, temp_data2;
@(clk) (@rose(write_cycle), 
 **if (condition1)
    temp_data1 = //something
  else if (condition2)
    temp_data2 = //something
  else
    //something else**
 ) |->
 first_match(##[1:5] signal_to_check == write_data) ##1
 ((signal_to_check == write_data)[*1:$] ##1 $rose(write_cycle));
endproperty

Is this the correct way to do it? I am getting syntax errors

22

In reply to atanu.biswas:

 
// property ::=
// if (expression_or_dist) property_expr1  
//.   else property_expr2 
// **** following is illegal 
// you have 
A_property |-> b_property 
// above is not a property. 
// study the syntax and operators for properties & sequences
property data_check; //  **** following is illegal 
logic [15:0] temp_data1, temp_data2;
   @(clk) (@rose(write_cycle),
if (condition1)
temp_data1 = //something
else if (condition2)
temp_data2 = //something
else
//something else
) |->
first_match(##[1:5] signal_to_check == write_data) ##1
((signal_to_check == write_data)[*1:$] ##1 $rose(write_cycle));
endproperty

Ben systemverilog.us

23

In reply to ben@SystemVerilog.us:

Hi Ben,

I have the below assertion for signals that checks that the value of a signal corresponding to an address remains same until next write to the same address is detected:

property data_check;
@(clk) @rose(write_cycle) |->
 first_match(##[1:5] signal_to_check == write_data) ##1
 ((signal_to_check == write_data)[*1:$] ##1 $rose(write_cycle));
endproperty

Now we have some registers which appear as single registers but the can have 2 types of data namely FSP0 data and FSP1 data. On the top module this appears as an 8bit signal but it can either have FSP0 or FSP1 data. This selection is done by specifying the FSP from another register. Suppose we have an FSP0 data currently in the register but if I select FSP1, then immediately FSP1 data will appear on that 16 bit register. So I have modified the above assertion as shown below:

property data_check (int WIDTH, LOWER_RANGE, UPPER_RANGE, logic [15:0] address1, logic [15:0] address2, logic [15:0] signal_to_check_temp);
    int wdata = 0;
    int fsp0_data = 0; 
    int fsp1_data = 0;
    @(mst_p.PCLK) disable iff (!(reset))
     (($rose(write_cycle) && ((mst_p.PADDR == address1) || (mst_p.PADDR == address2) ||(mst_p.PADDR == `fsp_select))), 
     wdata = mst_p.PWDATA, // <----
     fsp0_data = (mst_p.PADDR[13:12] == 0) ? mst_p.PWDATA : fsp0_data,
     fsp1_data = (mst_p.PADDR[13:12] == 1) ? mst_p.PWDATA : fsp1_data
     ) |->
     if (mst_p.PADDR == `fsp_select)
       first_match (##[LOWER_RANGE:UPPER_RANGE] 

      ((signal_to_check_temp == fsp0_data[(WIDTH-1):0]) || //FSP0 data
       (signal_to_check_temp == fsp1_data[(WIDTH-1):0]) || //FSP1 data
       (signal_to_check_temp == wdata[(WIDTH-1):0])     || //current data
       (signal_to_check_temp == 0))) ##1
        
       (((signal_to_check_temp == fsp0_data[(WIDTH-1):0]) || //FSP0 data
         (signal_to_check_temp == fsp1_data[(WIDTH-1):0]) || //FSP1 data
         (signal_to_check_temp == wdata[(WIDTH-1):0])     || //current data
         (signal_to_check_temp == 0)) 		 [*1:$] ##1 
         
         ($rose(write_cycle) && ((mst_p.PADDR == address1) || 
         			 (mst_p.PADDR == address2) ||  
        			 (mst_p.PADDR == `fsp_select))))
     else
       first_match (##[LOWER_RANGE:UPPER_RANGE] signal_to_check_temp == wdata[(WIDTH-1):0]) ##1 ((signal_to_check_temp == wdata[(WIDTH-1):0]) [*1:$] ##1 
       ($rose(write_cycle) && ((mst_p.PADDR == address1) || 
       			       (mst_p.PADDR == address2) || 
        		       (mst_p.PADDR == `fsp_select))));
  endproperty

address1 and address2 are the addresses for FSP0 and FSP1 data respectively which can appear in signal_to_check_temp based on what is selected with the fsp_select register. But this assertion fails. As shown above I am trying to store the FSP0 and FSP1 data in local variables so that I can compare with them.

24

In reply to atanu.biswas:
I generally provide guidelines. Your issue is too specific for me to follow. I suggest that you discuss this with a colleague in your organization.
Ben

25

In reply to atanu.biswas:
Please use code tags making your code easier to read. I have added them for you.

How about creating a small runnable example?