Assertions - Temporal LHS error in throughout operator

SystemVerilog
1

Hi,
I am trying to write an assertion which satisfies following scenario:

When start_address is 'h10 and iso_input is high, the counter should not toggle or it can be unknown(X), until iso_input is low.

The code that I wrote is:


     property gray_cnt_value_chk;
        @(posedge clk ) (start_addr == 'h10 && iso_input) |-> ##1 ($stable(gray_count) || gray_count === "X") throughout (iso_input[->0]);
    endproperty

I am getting this error:

Error-[SVATHTLHS] Temporal LHS of ‘throughout’ operator.
A temporal LHS is not allowed with the ‘throughout’ operator.
Expression: (##1 ($stable(gray_count) || gray_count === “X”) throughout (iso_input[->0]))

Please let me know how to resolve this.

Thanks
Shivam

2

In reply to shivamdec:


property gray_cnt_value_chk;
        @(posedge clk ) (start_addr == 'h10 && iso_input) |-> 
##1 ($stable(gray_count) || gray_count === "X")[*1:$] throughout (iso_input[->1]);
    endproperty

You’re checking a sequence throughout another sequence
Ben systemverilog.us

3

In reply to ben@SystemVerilog.us:

Thank you for replying Ben. I tried your suggestion but still getting same error:

Error-[SVATHTLHS] Temporal LHS of ‘throughout’ operator.
A temporal LHS is not allowed with the ‘throughout’ operator.
Expression: (( ##1 ((stable(gray_count) || (gray_count == "X")) [* 1:]))
throughout (iso_input [-> 1]))

One doubt: why did you suggest to use throughout (iso_input[->1]) instead of throughout (iso_input[->0])?

Intention is to check validity of sequence until iso_input is de-asserted.

Please let me know.
Thanks.

4

In reply to shivamdec:
My mistake on the troughout, see updated code below and sim results.
On [->0], that does not make sense.
b [->m] is equivalent to ( !b [*0:] ##1 b)[*m] Thus, b[->0] is same as (!b[*0:] ##1 b)[*0] , and that is empty

 
import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, b, iso_input;  
	logic[4:0] start_addr, gray_count;
	default clocking @(posedge clk); endclocking
		initial forever #10 clk=!clk;  
 
	ap_gray_cnt_value_chk: assert property(
		@(posedge clk ) (start_addr == 'h10 && iso_input) |-> 
		##1 ($stable(gray_count) || gray_count === "X") throughout (iso_input[->1]));
	

	initial begin 
		repeat(200) begin 
			@(posedge clk);   
			if (!randomize(start_addr, iso_input, gray_count)  with 
					{ start_addr dist {5'b10000:=3, 5'b01011:=1};
					  gray_count dist {3'b1:=101, 3'b111:=2};
					  iso_input dist {1'b0:=3, 1'b1:=1};

					}) `uvm_error("MYERR", "This is a randomize error")
					end 
					$stop; 
		end 
			
endmodule

1076×525 36 KB

1076×525 36 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

5

In reply to ben@SystemVerilog.us:

Thanks for explanation. But I am getting same error again :(

Error-[SVATHTLHS] Temporal LHS of ‘throughout’ operator.

A temporal LHS is not allowed with the ‘throughout’ operator.
Expression: (( ##1 ($stable(gray_count) || (gray_count === “X”))) throughout
(iso_input [-> 1]))

property p_gray_cnt_value_chk;
      @(posedge clk ) (start_addr == 'h11 && iso_input) |-> ##1 ($stable(gray_count) || gray_count === "X")  throughout (iso_input[->1]);
endproperty

Is it some tool issue?
Using this VCS_MX version: vcs-mx_vK-2015.09-SP2-13-T0428

Thanks for coping up.

6

In reply to shivamdec:
******* PLEASE SEE MY CORRECTIONS BELOW THIS POST ********
I see the issue here.
1800’2012 says that a sequence is

 
expression_or_dist throughout sequence_expr
// and it is NOT the following 
sequence  throughout sequence_expr // ILLEGAL !!!! 
What we have is 
##1 ($stable(gray_count) || gray_count === "X")  // a sequence 
throughout (iso_input[->1]) // thus it is illegal 
My tool is in error. 
************** NOTE *************
[Ben] Errata: My tool is not in error, see my last post below

The fix:

  
ap_gray_cnt_value_chk: assert property(
	@(posedge clk ) (start_addr == 'h10 && iso_input) |-> 
	##1 
        (  // expression_or_dist throughout sequence_expr
         ($stable(gray_count) || gray_count === "X") throughout 
         (iso_input[->1])
         )
       );
// ANOTHER FIX 
ap_gray_cnt_value_chk: assert property(
		@(posedge clk ) (start_addr == 'h10 && iso_input) |=> 
		($stable(gray_count) || gray_count === "X") throughout 
                 (iso_input[->1])
     );

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

7

In reply to ben@SystemVerilog.us:

The fixes worked. Thanks a lot Ben.

8

In reply to ben@SystemVerilog.us:
On

property p_gray_cnt_value_chk;
      @(posedge clk ) (start_addr == 'h11 && iso_input) |-> ##1 ($stable(gray_count) || gray_count === "X")  throughout (iso_input[->1]);
endproperty

Actually, my original code was OK.
​I was assuming that ##1 is ​ associated with the LHS of throughout which is not correct. Note that there is no issue of operator precedence here as there is no ambiguity in how the above sequence expression should be parsed. The ## has higher precedence than the throughout.
The error code that you got from your vendor is your vendor’s error; it is not my vendor.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr