Assertion to check if A does not rise between pulse B and Pulse C

SystemVerilog
,
1

Signal B pulse should be followed by Signal C pulse, with no fixed clock cycles between them. Pulse A should not fall between these two pulses(B and C). It be either before B or after C.

How would you write an assertion to check this?

2

Signal B pulse should be followed by Signal C pulse, with no fixed clock cycles between them. Pulse A should not fall between these two pulses(B and C). It be either before B or after C.

If the tool supports reject_on, you could do something like the following. Thus, if a==0 between b and c, the assertion fails. Code was tested with this quick and dirty testbench

module pulse; 
	bit a, a1, b, c, c1; 	
	// Signal B pulse should be followed by Signal C pulse, with no fixed clock cycles between them. 
	// Pulse A should not fall between these two pulses(B and C). It be either before B or after C. 
	
    ap_abc: assert property(reject_on (!a)
		  @(posedge b) 1'b1 |-> @(posedge c) 1'b1); 
		  
    initial repeat(2000) 
	   begin 
	     #10; 
	     if (!randomize(a1, b, c1) with 
	     		{a1 dist {1:=10, 0:=1};}) $display("error"); 
	     #1 c=c1;
	     #2 a=a1;
	   end   
endmodule

The reject_on (expression_or_dist) property_expr rejects the property as false if the abort condition is true. Otherwise, with the abort condition as false, the property expression evaluates to completion. The abort condition with the reject_on is asynchronous, whereas the sync_ reject_on is synchronous to the clock under current consideration for the property.

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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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 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
3

In reply to ben@SystemVerilog.us:

Hi Ben,

   If in between B and C there may be any number of clock cycles like [1:$] in a given simulation but A should not be become high in between B and C.

In that case how your code looks like?

Regarding “reject_on”

I don’t know about this.As per our requirement we should reject property when A is high right ?
in that why you have written like "assert property(reject_on (!a) " it should be “assert property(reject_on (a)”.

Could you please explain ?

Does below cod work ?


assert property (@(posedge clk) $rose(b) |-> (reject_on(a) c[1:$]);

[/code]

4

In reply to cool_cake20:

What I initially wrote was correct for the original requirements:
“Pulse A should not fall between these two pulses(B and C). It be either before B or after C.”
meaning (my interpretation) that if A==0, it should fail.
ap_abc: assert property(reject_on (!a) // reject if a==0, since !a==1, and abort condition is true
@(posedge b) 1’b1 |-> @(posedge c) 1’b1); / is correct.

For this requirement
“If in between B and C there may be any number of clock cycles like [1:$] in a given simulation but A should not be become high(meaning must be 0, if 1 → fail) in between B and C.” then
ap_abc: assert property(reject_on (a)
@(posedge b) 1’b1 |-> @(posedge c) 1’b1); / is correct.

From the syntax of a property
property_expr ::= // includes
reject_on ( expression_or_dist ) property_expr
Thus,

assert property (@(posedge clk) rose(b) |-> (reject_on(a) ##[1:] c); // is correct
// The " c[1:]" is incorect, unless you mean c[*1:], which is a repeat operator

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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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 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
5

In reply to ben@SystemVerilog.us:

Thanks Ben for clarification ,

i went by subject of post “Assertion to check if A does not rise between pulse B and Pulse C”