Assertion for PowerDown transitions

SystemVerilog
,
1

Hi ,

I wanted to write an assertion for PowerDown signal.
Valid Transitions:
0->1
0->2
2->0
1->0
0->4
0->5
Invalid Transitions
2->4
2->5
5->2
4->2
etc

How can i write an asserttion for that?

2

In reply to naaj_ila:
Below is sample code.


/*I wanted to write an assertion for PowerDown signal.
Valid Transitions:
0->1
0->2
2->0
1->0
0->4
0->5
Invalid Transitions
2->4
2->5
5->2
4->2 */
import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk;
	bit[2:0] pd;
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   
	ap0: assert property(pd==0 |=> 
				(pd==1) || (pd==2) || (pd==4) || (pd==5)
				);  // Could simplify this with Karnaugh map, you do the analysis
	ap21: assert property((pd==2) || (pd==1) |=> pd==0);
	
	apn2: assert property( not( pd==2 ##1 pd==4 || pd==5) );  
	apn5: assert property( not( pd==5 ##1 pd==2) );  // option 1
	apn4: assert property( not( pd==4 ##1 pd==2) );  // option 1
	apn54: assert property( not( pd==2 ##0 $past(pd)==4 || $past(pd)==5) );  // option 2
	cv: cover sequence (pd==4 ##1 pd==2);  
 initial begin 
     repeat(2000) begin 
       @(posedge clk);   
       if (!randomize(pd)) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule

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

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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 ,
Thanks for the reply
apn4: assert property( not( pd==4 ##1 pd==2) ); // option 1
For this, ##1 will take which sampling point value as there is no sampling point.

4

In reply to naaj_ila:

For this, ##1 will take which sampling point value as there is no sampling point.

When you talked about “transitions”, I assumed that these transactions came from a synchronous register (pd). Now, you’re saying that pd has no clocks, and it looks like you have an asynchronous machine. Hopefully, this machine is powered during the power-down sequence!
SVA’s fundamental philosophy is based on the sampling of signals. Thus, if you want to use SVA, your asynchronous machine needs to be sampled in your testbench with a high-speed clock, high enough in speed that would not miss a transaction; that will be expensive though in simulation. The assertion would look like

apn4: assert property( not( strong( pd==4 ##[1:$] pd==2)) ); // option 1

Maybe a solution outside SVA will work best for you.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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