SVA evaluation

Why SystemVerilog assertions are evaluated in observed region, although the values are sampled in preponed region ?

1 Like

In reply to Harshit:

Why SystemVerilog assertions are evaluated in observed region, although the values are sampled in preponed region ?

Keep in mind that SystemVerilog must emulate concurrency using a sequencial non-concurret processing computer. Before getting into an example that explains the regions, let me review the regions, as explained from my SVA Handbook 4th Edition
The bottom line:

  1. In an assertion, all signals are sampled in the Preponed region
    Thus, with (1, y=q), the module variable “q” is sampled,
    and every “q” referenced is the sampled value
  2. If within the sequence-matched-item, I update my property local variable with the return of a function call, like (1, w=getq()), that call is made in the Observed region, past the Active and NBA regions. Thus, in this model (below) w gets the updated value of q.
    390 sampled q= 25, current q= 25, past q= 8, var w= 31

Go over the example and think about the results. It all makes sense.

Example code: http://SystemVerilog.us/fv/regions2.sv


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a;  
	int q, qin, k;
	
	always_comb k=q+1'b1; 
	
	default clocking @(posedge clk); endclocking
		initial forever #10 clk=!clk;  
 
	always_ff  @(posedge clk)  begin 
		q <= qin;
	end 
	
	function automatic int getq(); 
		automatic int v; 
		v=k; 
		return v; 
	endfunction : getq
	
	property test;
		int y, w; 
		a |-> 
			(1, y=q, $display("%t sampled q=%d, current q=%d, past q=%d, var y=%d", $time, $sampled(q), q, $past(q), y)) ##0 
			(1, w=getq(), $display("%t sampled q=%d, current q=%d, past q=%d, var w=%d", $time, $sampled(q), q, $past(q), w));
	endproperty 
	ap_test: assert property(test);  

	initial begin 
		repeat(200) begin 
			@(posedge clk); #3;   
			if (!randomize(a, qin)  with 
					{ a dist {1'b1:=1, 1'b0:=3};
					  qin dist {[1:10]:=1, [20:30]:=2};
					}) `uvm_error("MYERR", "This is a randomize error")
					end 
					$stop; 
		end 
endmodule 	 

Sim results

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


@Ben
Thanks for your inputs.

In which region immediate assertions are sampled and evaluated ?

In reply to Harshit:

The signals in an immediate assertion are never sampled; they are evaluated at the point in the procedural process they appear.

The action block of a simple immediate assertion executes at that point as well. It’s the same an if-statement except you get the coverage recorded with pass/fail statistics.

The action block of a deferred immediate assertion gets postponed. This is to avoid glitches in combinational logic where the immediate assertion could get evaluated multiple times in the same time slot. Only the last evaluation of the assertion is considered.

In reply to ben@SystemVerilog.us:

Hi Ben,

Can you explain why “%t sampled q=%d, current q=%d, past q=%d, var w=%d” is getting printed before “%t sampled q=%d, current q=%d, past q=%d, var y=%d” although it has ##0 delay ?

In assertion the $display will get evaluated in active region or re-active region?

In reply to samirxd:

In reply to ben@SystemVerilog.us:
Can you explain why “%t sampled q=%d, current q=%d, past q=%d, var w=%d” is getting printed before “%t sampled q=%d, current q=%d, past q=%d, var y=%d” although it has ##0 delay ?

NO, but I believe it is how the tool handles the printing.
I tried the model at Edit code - EDA Playground
got what you expected, the “y” print before the “w” print


# 210 sampled q=         30, current q=         30, past q=         27, var y=         30
# 210 sampled q=         30, current q=         30, past q=         27, var w=         10
# 250 sampled q=         25, current q=         25, past q=          9, var y=         25
# 250 sampled q=         25, current q=         25, past q=          9, var w=          2q

In assertion the $display will get evaluated in active region or re-active region?

  • In immediate assertions, the $display is evaluated at the point in the procedural process they appear. Thus,

module m;
bit a, b, d, clk;
always_comb begin
a_ab: assert(a==b) else $display("%t a=%b, b=%b", $realtime, a, b);
// $display is evaluated in the Active Region.
end

  • Concurrent assertion

property p;
bit v;
(a, v=d) |-> ##1
(v, $display("%t EVALUATED IN OBSERVED REGION a=%b, b=%b", $realtime, a, b)) ##0 b;
endproperty
ap_p: assert property(@(posedge clk) p) else   $display("%t ACTION BLOCK IN RACTIVE REGION : a=%b, b=%b", $realtime, a, b);

In reply to ben@SystemVerilog.us:

Thanks Ben.

In reply to samirxd:

##0 is sequence concatenation indicating the beginning of the second sequence is in the same clock tick as the end of the first sequence. Since these are both single clock sequences, they are concurrently true .There is no implied ordering between the sequence match items. However within a list, the statements get executed in the order they appear. So you should write this as:

property test;
		int y, w; 
		a |-> 
		   (1, y=q,      $display("%t sampled q=%d, current q=%d, past q=%d, var y=%d", $time, $sampled(q), q, $past(q), y),
		       w=getq(), $display("%t sampled q=%d, current q=%d, past q=%d, var w=%d", $time, $sampled(q), q, $past(q), w));
endproperty

In reply to dave_59:

Thanks Dave.

In reply to ben@SystemVerilog.us:

Hi Ben ,

If I were to define the subroutine as ::


       function automatic int getq(); 
		return k ;  // Simply  return ' k '  without  defining  variables .
	endfunction : getq

I observe the updated value of k is assigned to local variable w .

Are there any additional advantages of defining the variables within the subroutine as automatic ?

My understanding is that if the subroutine were to be called in parallel from
multiple places each call will have their own copy .

So if I pass different values as input to the subroutine from different places
at the same time , each invocation would return an appropriate value due to the automatic variables defined within the subroutine .

In reply to hisingh:

In reply to ben@SystemVerilog.us:


function automatic int getq(); 
return k ;  // Simply  return ' k '  without  defining  variables .
endfunction : getq

I observe the updated value of k is assigned to local variable w .


   function bit test();
    $display("%t sampled(w)= %b", $realtime, $sampled(w));
    $display("%t Observed(w)= %b",$realtime,  w);
    return w;      
   endfunction
   property p; 
    bit v; 
    @(posedge clk) (a, v=test()) |-> b; // test(b);  
   endproperty 
   ap_p: assert property(p);  

Properties are executed in the Observed region. The function should return the value of w in the Observed Region, which could have been updated in the NBA Region.

Are there any additional advantages of defining the variables within the subroutine as automatic ?

NO. BTW, it is bad practice to do what you are proposing.

My understanding is that if the subroutine were to be called in parallel from
multiple places each call will have their own copy .
So if I pass different values as input to the subroutine from different places
at the same time , each invocation would return an appropriate value due to the automatic variables defined within the subroutine .

Function will return the value seen in the Observed Region.
Any, bad practice.

In reply to ben@SystemVerilog.us:

Hi Ben ,

I am a little confused about the clocking event ( @ posedge clk ) in the property A2C .

Concurrent assertion is evaluated in Observed region whereas the event i.e @ posedge clk occurs in Active Region .

So by Observed region the event trigger has passed by then .
So what triggers the property A2C if it’s being evaluated in Observed Region ?

Can I say the clocking event triggers the property , but the expression is checked
later in observed region using the values sampled in pre-poned region

In reply to hisingh:

In reply to ben@SystemVerilog.us:
I am a little confused about the clocking event ( @ posedge clk ) in the property A2C .
Concurrent assertion is evaluated in Observed region whereas the event i.e @ posedge clk occurs in Active Region .

Every clocking event has these main regions in order to emulate concurrency while using an evaluation machine that is sequential in operation.
Thus, ap: assert property(@ (posedge clk) a |-> b ); the simulator considers that clocking event (the @(posedge clk)) and before doing anything else stores the value of a and b (that’s the Preponed Region).
The simulator then does other things in the other regions at the same time period. In other words, time stops. Following the completions of whatever needs to be done in the NBA, it stars pressing the assertion using those stored values in the Preponed region.
Sorry, but saying @ posedge clk occurs in Active Region does not make sense. @(posedge clk) is an event that starts the chain of things in these defined regions.

So by Observed region the event trigger has passed by then .
So what triggers the property A2C if it’s being evaluated in Observed Region ?

All these regions are at the same time period. The split of regions is just to have a simulator do its calculations to emulate concurrency. When you watch a movie, let’s say a traffic accident, what do you see? 1) car coming, then person walking, then car coming then person walking, then accident. All these things occur at the same time, but you see them sequentially. So in movies, the emulation is to split the scene into Regions (or small scenes) to emulate concurrency.

Can I say the clocking event triggers the property , but the expression is checked
later in observed region using the values sampled in pre-poned region

YES!