Assertion - which assertion should I use and where?

[saritr]

I have the following interface:

interface tx_interface (input bit clk, input bit srstn);
   //dut input
   logic [15:0] xi;
   logic [15:0] xq;
   logic 	cyc_tic;
   logic 	xn_valid;
   logic        rd_en;
   
   
   //dut output
   logic [15:0] yi;
   logic [15:0] yq;
endinterface

The signal xn_valid, xi, xq should follow the followig protocol.

When rd_en == 1 xn_valid should be 1 also after 5 clock cycles.
which assertion should I use and where for this?

p.s
The rd_en can change to 1 several time inside those 5 clock cycles…

[ben2]

In reply to saritr:
// Requirements are ambiguous as to should happen with the responses to the "rd_en"s in between the
// first rd_en and xn_valid. For example,

//                0  1  2  3  4  5  6  7  8  9  A  B  C
// rd_en          0  0  1  0  1  1  0  0  0  0  0  0  0
// xn_valid       0  0  0  0  0  0  0  1  ?  ?  ?  ?  ?
//                      ^--------------^
//                            ^--------------^
//                                ^--------------^

// What should xn_valid be in response to rd_en==1 @ cycle 4 and 5?
Below is one understandng where the rd_en excudes other rd_en to be considered in the assertion. You need to clarify your requirements, and that is the beauty of assertions, they force to be clear on intent.

interface tx_interface (input bit clk, input bit srstn);
	//dut input
	logic [15:0] xi;
	logic [15:0] xq;
	logic 	cyc_tic;
	logic 	xn_valid;
	logic   rd_en;
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  	
	bit go=1'b1;  // used for exclusivity 
	function void set_go(bit a); 
		go=a; 
	endfunction : set_go  	
    // Assertion with exclusivity 
	ap_exclusive: assert property((rd_en && go, set_go(1'b0)) 
                           |-> ##5 (xn_valid, set_go(1'b1)) ) else set_go(1'b1);  
	
	// Assertion that for every rd_en then 5 cycles later xn_valid
	ap_every: assert property(rd_en |-> ##5 xn_valid);  
 
	//dut output
	logic [15:0] yi;
	logic [15:0] yq;
endinterface 

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 978-1539769712
• 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

---

[saritr]

In reply to ben@SystemVerilog.us:

Each rd_en must followed by xn_valid.

//                0  1  2  3  4  5  6  7  8  9  A  B  C  D  E  F
// rd_en          0  0  1  0  1  1  0  0  0  0  1  0  0  0  0  0
// xn_valid       0  0  0  0  0  0  0  1  0  1  1  0  0  0  0  1    
//                      ^--------------^
//                            ^--------------^
//                                ^-------------^
//                                              ^--------------^

[ben2]

In reply to saritr:

In reply to ben@SystemVerilog.us:
Each rd_en must followed by xn_valid.

//                0  1  2  3  4  5  6  7  8  9  A  B  C  D  E  F
// rd_en          0  0  1  0  1  1  0  0  0  0  1  0  0  0  0  0
// xn_valid       0  0  0  0  0  0  0  1  0  1  1  0  0  0  0  1    
//                      ^--------------^
//                            ^--------------^
//                                ^-------------^
//                                              ^--------------^

// Assertion that for every rd_en then 5 cycles later xn_valid

ap_every: assert property(rd_en |-> ##5 xn_valid);

That does it. It says that for every match of the antecedent, which is attempted at every clock, the consequent must be true.
Ben