# SVA evaluation

**URL:** <https://verificationacademy.com/forums/t/sva-evaluation/33470>\
**Category:** SystemVerilog\
**Tags:** SystemVerilog\
**Created:** [September 9, 2017, 10:36am UTC](https://verificationacademy.com/forums/t/sva-evaluation/33470 "2017-09-09T10:36:01Z")\
**Posts on this page:** 1\
**Showing post:** 2

<div class="post-metadata">

**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\
**Post date:** [September 10, 2017, 7:14pm UTC](https://verificationacademy.com/forums/t/sva-evaluation/33470/2 "2017-09-10T19:14:10Z")

</div>

_In reply to [Harshit](https://verificationacademy.com/forums/t/sva-evaluation/33470):_

> 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](http://goo.gl/JOfuEB)  
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.

 ![](https://verificationacademy.com/forums/uploads/default/original/1X/29336b539514a1c55a258551712b19acaf25b283.png)

Example code: [http://SystemVerilog.us/fv/regions2.sv](http://SystemVerilog.us/fv/regions2.sv)

```verilog

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

 ![](https://verificationacademy.com/forums/uploads/default/original/1X/6ecae83f06207a9a7f3132c909cee2ebc6eb3208.png)

Ben Cohen  
[http://www.systemverilog.us/](http://www.systemverilog.us/) [ben@systemverilog.us](mailto:ben@systemverilog.us)  
For training, consulting, services: contact [Home - My cvcblr](http://cvcblr.com/home)

- [SVA Handbook 4th Edition, 2016 ISBN 978-1518681448](http://goo.gl/JOfuEB)
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- [Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712](https://goo.gl/d10QHh)
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

* * *

---

_[View the full topic](https://verificationacademy.com/forums/t/sva-evaluation/33470)._