Range issue in systemverilog property

SystemVerilog
, , , ,
1

Hello,
I’ve a property that is needed to be asserted(located in an interface):


property p1; //When a Tx complete interrupt is asserted, assert phy_ce is dropped after ble_tx_phy_ce_dly bits
      @(posedge ble_clk) disable iff(!ble_rst_n || !ble_ena)
	ble_irq_sts[0] |-> ##(int'(ble_tx_phy_ce_dly*(ble_div+1))) !phy_ce;
   endproperty

I get this compilation errors:

  • ** Error: Range must be bounded by constant expressions
  • ** Error: Left bound of SVA range expression does not evaluate to a constant or parametric value.
  • ** Error: Right bound of SVA range expression does not evaluate to a constant or parametric value.

the delay and clk division ratio are transaction ranadom values
Thank you in advance

2

In reply to Dilip Bagadi:

Hi Dilip,
Thanks for response, but there something I don’t understand
It’s my first time to see the expression before and after the implication:
1- req_delay=delay+1’b1, this an initialization to the delay to the desired value, correct ?
So it can be req_delay = ble_tx_phy_ce_dly*(ble_div+1)

2- What follows the implication (till the CONSEQUENT) is confusing a bit, could you please clarify more or use a simpler example ?

Thank you for cooperation.

3

In reply to Mustafa:

Hi,

The delay inside property should be a CONSTANT VALUE or a PARAMETER.
But an alternate is there to specify a variable in delay.

Pls follow the example below in your case to specify VARIABLE DELAY in a property
(ANTECEDENT, req_delay=delay+1’b1) |-> (1, req_delay=req_delay-1’b1)[*0:$] ##1 req_delay==0 ##0 CONSEQUENT;

Regards,
Dilip

4

You need to do something like the following, basically setting a local variable to the desired delay, and then do a repeat while decrementing the counter until the value is 0.

module range1;
	int ble_tx_phy_ce_dly, ble_div;
	bit[15:0] ble_irq_sts; 
	bit ble_clk, phy_ce, ble_rst_n, ble_ena ;
	
	/* property p1; //When a Tx complete interrupt is asserted, assert phy_ce is dropped after ble_tx_phy_ce_dly bits
		@(posedge ble_clk) disable iff(!ble_rst_n || !ble_ena)
			ble_irq_sts[0] |-> ##(int'(ble_tx_phy_ce_dly*(ble_div+1))) !phy_ce;
	endproperty */ 
	
    // assume that (int'(ble_tx_phy_ce_dly*(ble_div+1'b1))) is of value 1 or greater
	property p1; //When a Tx complete interrupt is asserted, assert phy_ce is dropped after ble_tx_phy_ce_dly bits
	  int v; 
          @(posedge ble_clk) disable iff(!ble_rst_n || !ble_ena)
	   (ble_irq_sts[0], v= (int'(ble_tx_phy_ce_dly*(ble_div+1'b1))))  |=> 
		(1, v=v-1'b1)[*1:$] ##0 v<= 0 ##0 !phy_ce;
        endproperty

        assert property(p1); 
endmodule

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

  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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