Assertion - which assertion should I use and where?

SystemVerilog
,
2

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