How to write pulse width systemverilog assertion when width is configurable

Question

The scenario is: Signal active can be either 1 cycle, 2 cycle, 3 cycle or 4 cycle wide depending on config[1:0] input to the module

Easiest way to write property for this is:

property p_PropA;
    @(posedge clk) $rose active ##config ~active;
endproperty

But it is syntactically wrong. What is correct way of writing this assertion?

Answer 1

You need to use a local variable, see IEEE Std 1800-2012 § 16.10 Local variables

Here is a simple example:

property p_PropA;
  int count;
  @(posedge clk)
  ($rose(active),count=config) |->
    (active,count--)[*] ##1 (~active && count==0);
endproperty