SVA on intersect

SystemVerilog
1

I’m trying to check B is assert between 2 pulses of A, where both A and B should only be high for 1 cycle, A can be close together or far apart, second pulse of A must be assert. I tried to write the assertion be either it’s way too complicate or it’s keep missing some situation.

A __||______||__

B_______||_________

    $rose(A) | = > 
        !A throughout (##[0:$]$rose(B) ##1 !B[*1:$\]) s_eventually $rose(A) | = > $fell(A);

but B may be high or abnormal but still true for b is high for 1 cycle?

A __||______||__

B _|           |_||_______

($rose(A) intersect (!B[*1:$])) |=> (!A) intersect (##[0:$] $rose(B) ##1 !B[*1:$]) s_eventually ($rose(A) |=> $fell(A)) intersect (!B[*1:$])

I asked gpt, it said it’s way too complicated and may result error

Can anyone give a hint where should I start on or did I overthinking it?

2

Using multiple implications in one property almost never works the way you wanted to. I would also separate the assertion that both A and B have to be high for one cycle.

I think the within operator might be more appropriate in this context. Here’s an example that I haven’t tried, so consider this a hint.

assert property (@(posedge clk) disable iff (!rst_n)
  // Start on each rising edge of A
  $rose(A)
  |->
  // B must rise after this A and before the next A
  (##[1:$] $rose(B))
    within
  ( (! $rose(A))[->1] ##1 $rose(A) )
);
property one_cycle(sig);
  @(posedge clk) $rose(sig) |=> !sig;
endproperty
assert property(one_cycle(A));
assert property(one_cycle(B));

You need to clarify the situation for the second pulse of A. with this assertion, it will start a new assertion thread. Is that OK or do you need to keep them separated?

3

Hi Dave,

Any pointers on the latter part ?

How to ensure that the 2nd assertion of A doesn’t result in antecedent match