Resolving Race Condition

SystemVerilog
1

Hi,
I am trying to understand behaviour of simulation and resolve the race condition for following code snippet:


	
wire pclk;
wire [31:0] reg_check;
reg [31:0] reg_check_ref = 32'h0;
wire reg_check_en;
	   	
assign reg_check = {PWDATA_FROM_DESIGN}  //Concatenation of some signals to compare

always @ (posedge pclk) begin
	if ( SOME_TRIGGER_SIGNAL == 32'h123) begin
		reg_check_ref <= pwdata;        // LINE-X
	end 	
end

property myproperty;
    @(posedge pclk) disable iff (~reg_check_en)
        reg_check == reg_check_ref;             // LINE-Y
endproperty

myproperty_assert : assert property(myproperty) else begin
   $warning("myproperty failed");
end

myproperty_assert is failing due to the fact that when LINE-Y is executed, assignment of reg_check_ref in LINE-X is not executed prior to it, given SOME_TRIGGER_SIGNAL was 'h123 in previous clock cycle. I want to make sure that “reg_check_ref” is updated before LINE-Y is executed. Any suggestions to resolve this?

I am learning SV and any help much be appreciated.

Thanks.

2

In reply to stupidkris1010:

You can end up in race conditions, if you are mixing up signals from TB & DUT and using them in assertions.

Could you give more details of what reg_check_en, SOME_TRIGGER_SIGNAL, pclk are? Are you also assigning the DUT values like you did for reg_check? Or, are they generated with in testbench?

3

In reply to S.P.Rajkumar.V:

Hi, thanks for feedback. Sorry for not providing entire code. Here’s the explanation for these signals:

  • pclk: reference clock of APB interface from DUT
  • reg_check_en : trigger signal from TB, this is getting high for one clock cycle after every 7 posedge of pclk
  • SOME_TRIGGER_SIGNAL: combination of APB interface signals from DUT to catch write transaction

Thanks.

4

In reply to stupidkris1010:

Why dont you disable property when SOME_TRIGGER_SIGNAL != 32’h123?


property myproperty;
    @(posedge pclk) disable iff (~reg_check_en || (SOME_TRIGGER_SIGNAL != 32’h123))
        reg_check == reg_check_ref;
endproperty
5

In reply to cuonghl:

Hi Chris,
I think that would not resolve the problem. Let’s say, LINE-X would get executed in cycle N. Simulator would schedule this NBA event for cycle N+1. Now considering that “reg_check_en” is scheduled to be high in cycle N+1 before “reg_check_ref” is schedule, then this would not work. Cheers.

6

In reply to stupidkris1010:

In reply to cuonghl:
Hi Chris,
I think that would not resolve the problem. Let’s say, LINE-X would get executed in cycle N. Simulator would schedule this NBA event for cycle N+1. Now considering that “reg_check_en” is scheduled to be high in cycle N+1 before “reg_check_ref” is schedule, then this would not work. Cheers.

I’m not sure I fully understand this explaination. I guess you were talking the delay of reg_check_ref 1 cycle after SOME_TRIGGER_SIGNAL equal 32’h123, right?

Here is some updates:


wire trigger_en;
reg trigger_en_dly;

assign trigger_en = (SOME_TRIGGER_SIGNAL == 32'h123);

/* The trigger_en_dly will delay 1 cycle after trigger
   That mean reg_check_ref is updated at same clock as trigger_en_dly */

always @(posedge pclk or negedge presetn) begin
  if(!presetn) 
    trigger_en_dly <= 1'b0;
  else 
    trigger_en_dly <= trigger_en;
end

/* The propery is enable when trigger_en_dly asserted */
property myproperty;
  @(posedge pclk) disable iff (~reg_check_en || ~trigger_en_dly)
  reg_check == reg_check_ref;
endproperty
7

In reply to cuonghl:

Thanks, this suggestion was helpful.