Formal arguments to properties / sequences

SystemVerilog
, ,
1

Hi All,

Consider the following property declaration

  property param_prop( N_bit );
    logic [(N_bit-1):0] val;  // bit-width legal ?
    
    (1,val=N_bit-1,$display("val is 'd%0d",val) )[*N_bit]; // [*N_bit] legal ?   
  endproperty  
  
  a1:assert property(@(posedge clk) param_prop(8) );
  
  a2:assert property(@(posedge clk) param_prop(2) );

On testing it on EDA I see 2 tools accept this whereas one tool throws compilation error

Error-[TCF-CETE] Cannot evaluate the expression
testbench.sv, 10
"(N_bit - 1)"
  Cannot evaluate the expression in left dimension bound.
  The expression must be compile time constant.

Generally the bit width of a variable is fixed at compilation stage or elaboration stage ( using parameter / localparam ). In the above code I use the argument to set the bit width as well the repetition for the sequence expression.

(1) Is the above code legal from LRM perspective ?

(2) Are a1 & a2 similar to an instance of a parametrized module / interface or specialization of parametrized class ? ( i.e Resolved at Elaboration time )

2

Yes, this is legal. Section 16.8 Declaring sequences says

For example, a reference to an untyped formal argument may appear in the specification of a cycle_delay_range, a boolean_abbrev, or a sequence_abbrev (see 16.9.2) only if the actual argument is an elaboration-time constant. The following example illustrates such usage of formal arguments:

sequence delay_example(x, y, min, max, delay1);
   x ##delay1 y[*min:max];
endsequence

// Legal
a1: assert property (@(posedge clk) delay_example(x, y, 3, $, 2));

int z, d;
// Illegal: z and d are not elaboration-time constants
a2_illegal: assert property (@(posedge clk) delay_example(x, y, z, $, d));

Section 16.12 Declaring Properties explains that the same rules for argument passing apply to both declaring sequences and properties.

Instances of properties and sequences are resolved during elaboration, but I see it more like the text expansion of a macro, with the exception that there is a scope around the body that prevents name collisions for locally declared variables.