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.