Can I please get some help in writing an assertion with this question :-

signal1 will be high for few number of clock cycles, signal2 can only be high for one clock cycle when signal1 is high, we don’t care about signal2 when signal1 is not high.

Requirement :
Sig1 will be high for a few numbers of clock cycles. // Number of clocks are unknown
sig2 can only be high for one clock cycle while sig1 is high.
sig2 toggles do not care if sig1 is not high.
property
@(posedge clk)
$rose(sig1) |-> sig2[->1] ##1 !sig2[*1:$] intersect sig1[*1:$];
endproperty

Requirement :
Sig1 will be high for a few numbers of clock cycles. // Number of clocks are unknown
sig2 can only be high for one clock cycle while sig1 is high.
sig2 toggles do not care if sig1 is not high.

I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))? rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
when the sequence sig2 ##1 !sig2occurs, the consequent is satisfied.
However, it fails to check if sig2 occurs again for one or more cycles when sig1 remains high for more cycles.
How about something like: Edit code - EDA Playground // code EPWave Waveform Viewer // wave

I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))?

My interpretation was that only if both sig1 and sig2 are high then , sig2 should be de-asserted at next posedge of clk . Hence I used **$fell( sig2 )** in the consequent

(2) Consider scenario where sig1 is high throughout from posedge T1 to T10 .
My understanding is that Sig2 could be asserted and de-asserted multiple times during this time. However if we use $rose(sig1) as the antecedent we would miss out on 2nd $rose(Sig2).

(3) Out of curiosity , what is considered the left sequence_expr for intersect operator ?

I split that to two properties as below. Untested though.

// Sig1 will be high for a few numbers of clock cycles.
// Number of clocks are unknown
// sig2 can only be high for one clock cycle while sig1 is high.
$rose (sig1) |-> sig1 until_with sig2;
$rose (sig2) |=> !sig2;
// sig2 toggles do not care if sig1 is not high.

In reply to MICRO_91:
Comments about the replies:
I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))? rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
when the sequence sig2 ##1 !sig2occurs, the consequent is satisfied.
However, it fails to check if sig2 occurs again for one or more cycles when sig1 remains high for more cycles.
How about something like: Edit code - EDA Playground // code EPWave Waveform Viewer // wave

Hi Ben.
I think I might miss something with “intersect”. In the below property you gave, Let us say if (sig1 && sig2)[=1] happens at T5 and sig2 drops at T6, !(sig1)[->1] happens at T10. At which point they intersect ?

On item 1, I wrote the model with my understanding of the requirements. If there is are different requirements, then the model needs to change.
In any case, the nice thing about writing SVA is that it puts on the dots on the requirements.

on

(3) Out of curiosity , what is considered the left sequence_expr for intersect operator ? rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];

This is resolved in 1800 by the definition of
1800: 16.9.1 Operator precedence Operator precedence and associativity are listed in Table 16-1 . The highest precedence is listed first. Table 16-1—Operator precedence and associativity
Here ## has higher precedence than intersect. Thus,
sig2[->1] ##1 !sig2[*1:] is computed first. In other words,
sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:]
is same as
(sig2[->1] ##1 !sig2[*1:]) intersect sig1[*1:$]