Write SVA assertion without accept_on

SystemVerilog
1

Hi,
I need to write a compact assertion equivalent with the version below , which contains sync_accept_on . My problem is that the property uses a local variable, consequently I cannot use sync_accept_on.

(in != 0, in_save = in) |-> sync_accept_on(erase == in_save)
      ##1 enable_out[->3] ##0 out == in_save;

“in_save” is the local variable.

How should be handled this situation in order to write a succinct assertion?

2 
/* You'll need to call a function from the sequence match item to set a module variable.  
The following code compiles and elaborates OK on Questa. 
I added an action block to reset the save to a non-used value. 
Note that there must be exclusivity when this assertion fires until it passes or fails, otherwise other successful attempts will reset the value of save. 
You can do that with a go. */

module saccept;
	bit clk, enable_out, go=1; 
	int in1, erase, out1, save=-1, in_save; // save==-1 assuming in_save is never -1
	function void set_save(int v, bit b); 
		save=v; 
		go=b;
	endfunction
	
	property p1; 
	  int  in_save; 
	  sync_accept_on(erase == save)
	  (go && in1 != 0, in_save = in1, set_save(in_save, 1'b0)) |-> 
      ##1 enable_out[->3] ##0 out1 == in_save;
    endproperty 
    
    ap1: assert property(@(posedge clk) p1) set_save(-1, 1'b1); else  set_save(-1, 1'b1);
 endmodule

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

Another solution without the accept_on


property p1b; 
	  int  in_save; 
	  //sync_accept_on(erase == save)
	  (go && in1 != 0, in_save = in1) |-> 
      (##1 enable_out[->3] ##0 out1 == in_save) or (erase == save [->1]);
    endproperty 
    
    ap1b: assert property(@(posedge clk) p1b);

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
4

Ben,

Many thanks for your suggestions. This is what I was looking for .

Best Regards,
Florin

5

In reply to Florin:

Note that the accept_on/reject_onfamily of operators terminates the property as an accept (true vacuously, with no contribution to the pass statistics) or reject (false vacuously, with contributions to the failed statistics). The previous solution (reiterated below) terminates the property as an accept true nonvacuously with contribution to the pass statistics; a difference.


    property p1b; 
	  int  in_save; 
	  //sync_accept_on(erase == save)
	  (go && in1 != 0, in_save = in1) |-> 
      (##1 enable_out[->3] ##0 out1 == in_save) or (erase == save [->1]);
    endproperty

Ben Cohen