How Can I Hold Off an Assertion Until Sync is Established Using a Local Variable?

SystemVerilog
, ,
1

I want to hold off an assertion until the first occurrence of a sync byte, then execute the assertion every byte thereafter. I thought that a local variable would be the ideal way to do this - but no! Every permutation I tried either fired intermittently (only when byte matched sync byte) or failed to compile. Some examples:

property data_parity_prop (clk, rst, d, available, parity);
bit flag = 0;
@(posedge clk) disable iff (rst !== 1)
((d == SYNC_DATA), flag = 1) || flag |-> ^d ^ available ^ parity;
endproperty

FAILED TO COMPILE - Syntax error

property data_parity_prop (clk, rst, d, available, parity);
@(posedge clk) disable iff (rst !== 1)
((d == SYNC_DATA), flag = 1) || flag |-> ^d ^ available ^ parity;
endproperty

FAILED TO COMPILE - flag not declared

bit flag;

property data_parity_prop (clk, rst, d, available, parity);
@(posedge clk) disable iff (rst !== 1)
((d == SYNC_DATA), flag = 1) || flag |-> ^d ^ available ^ parity;
endproperty

FAILED TO COMPILE - Can’t assign to variables other than local ones

I also tried putting flag in the sequence and passing it to the property and a bunch of other variants without success. Please help save what little hair I have left and tell me what I’m doing wrong. Thanks!

2

In reply to hal9e3:

Here’s the version that compiles OK but only fires when the data byte matches the sync value:

property data_parity_prop (clk, rst, d, available, parity);
	bit flag = 0;
	@(posedge clk) disable iff (rst !== 1)
		(flag || (d == SYNC_DATA), flag = 1) |-> ^d ^ available ^ parity;
	endproperty
3

You needed the property “or” operator.

property data_parity_prop (clk, rst, d, available, parity);
  bit flag = 0;
  @(posedge clk) disable iff (rst !== 1)
((d == SYNC_DATA), flag = 1) or flag |-> ^d ^ available ^ parity;
endproperty
// Could also use
property data_parity_prop (clk, rst, d, available, parity);
  bit flag = 0;
  @(posedge clk) disable iff (rst !== 1)
  ($rose(d == SYNC_DATA), flag = 1) or flag |-> ^d ^ available ^ parity;
endproperty
// Suggest you also use the default disable iff

property_expr ::=
sequence_expr
| strong ( sequence_expr )
| weak ( sequence_expr )
| ( property_expr )
| not property_expr
| property_expr or property_expr // <-----------
| property_expr and property_expr
| sequence_expr |-> property_expr
| sequence_expr |=> property_expr
…

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
  • 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 0-9705394-2-8
  • 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
4

In reply to ben@SystemVerilog.us:

Thanks, that cleared it up!

5

In reply to hal9e3:

My, mistake, this did NOT fix the problem, either variant. The assertion only fires when d == SYNC_DATA.

6

In reply to hal9e3:

Did you use this?
($rose(d == SYNC_DATA), flag = 1) or flag |-> ^d ^ available ^ parity;
This states that a new d==SYNC_DATA will set the flag.
To get A part of the property fired one and ONLY ONCE, you could do this

property data_parity_prop (clk, rst, d, available, parity);
  bit flag = 0;
  bit done= 0;
  @(posedge clk) disable iff (rst !== 1)
((d == SYNC_DATA && !done), flag = 1, done=1) or flag |-> ^d ^ available ^ parity;
endproperty
// or more simply with one variable 
property data_parity_prop (clk, rst, d, available, parity);
  bit flag = 0;
  @(posedge clk) disable iff (rst !== 1)
((d == SYNC_DATA && !flag), flag = 1) or flag |-> ^d ^ available ^ parity;
7

In reply to ben@SystemVerilog.us:

I tried both of your solutions. Also, both of them are trying to achieve my desired behaviour - hold off until first match, then fire every cycle after that.

8

In reply to hal9e3:

Another non-solution:

((d == SYNC_DATA) or flag, flag = 1) |-> ^d ^ available ^ parity;

Only fires when d == sync_data

9

In reply to hal9e3:

OK, solved this but had to go outside SVA to do it:

bit start_asserts;

always @(posedge clk) begin
	if (rst !== 1) begin
		#1 start_asserts <= 0;
		end
	else if ((d == SYNC_DATA) & !available) begin
		#1 start_asserts <= 1;
		end
	else begin
		#1 start_asserts <= start_asserts;;
		end
	end

property data_parity_prop (clk, rst, d, available, parity, start_asserts);
	@(posedge clk) disable iff (rst !== 1)
		start_asserts |-> (^d ^ available ^ parity);
	endproperty

Not pretty or elegant but it works.

10

In reply to hal9e3:

What you have done that is new is added the " !available"
The following options would work:

module test8;
bit start_asserts, available, parity, clk, rst;
logic[7:0] SYNC_DATA, d;
// property would show ONE pass (and only one) when ((d == SYNC_DATA)&&  !available )
// That may skew the statistic a tiny bit. 
// The other passes are when the consequent is true
property data_parity_prop (clk, rst, d, available, parity);
  bit flag = 0;
  @(posedge clk) disable iff (rst !== 1)
  ((d == SYNC_DATA) &&  !available, flag = 1) or flag |-> ^d ^ available ^ parity;
endproperty
ap_data_parity_prop: assert property(data_parity_prop
		(clk, rst, d, available, parity));
	
	
// If this is not acceptable, then you can write 2 separate properties and use the action block
ap_start: assert property(@(posedge clk) // disable iff (rst !== 1)
   (d == SYNC_DATA) && !available) start_asserts <= 1; 
   
property data_parity_prop_v2 (clk, rst, d, available, parity, start_asserts);
  @(posedge clk) disable iff (rst !== 1)
  start_asserts |-> (^d ^ available ^ parity);
endproperty
ap_data_parity_prop_v2: assert property(data_parity_prop_v2
			(clk, rst, d, available, parity, start_asserts));
	
endmodule

A side comment, from LRM

& | ^ ^~ ~^ Binary bitwise operators
&& || –> <–> Binary logical operators

You should use the logical operators when you are doing logical operations.

//Thus, instead of 
else if ((d == SYNC_DATA) & !available) 
// WRITE
else if ((d == SYNC_DATA) && !available)

Also, in your code, you should skip the last "else. Thus

always @(posedge clk) begin
  if (rst !== 1) begin
     #1 start_asserts <= 0;
  end
  else if ((d == SYNC_DATA) & !available) begin
     #1 start_asserts <= 1;
   end
   // else begin
   //  #1 start_asserts <= start_asserts;;
   // end
end

Ben SystemVerilog.us