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?

4

But will it check for the second A, I thought it need to use strong statement to make sure second A is asserted before end of the sim. I want to catch that if something like below happen, second A never assert before sim end, it will result error.
A __||__________
B _______||_____

So the assertion that you wrote is checking ABAABA… ?
And if I want to check ABABAB… that B must be assert after A before end of the sim, should I use
$rose(A) |-> s_eventually((##[1:$] $rose(B)) && ! $rose(A)) with the two one_cycle?

5

Just add strong operator to the consequent in Dave’ solution

Have you tested Dave’ solution ? ( I suggest try a few different types of stimulus )

He has already mentioned this via

with this assertion, it will start a new assertion thread. Is that OK or do you need to keep them separated?

I don’t think you have tested your own code.

Hint1: It’s missing the 2nd assertion of A

Hint2: What if B is asserted along with 1st $rose(A) ?

6

It would be very helpful to create a test case that tests the scenarios you’re concerned about. This makes it easier for everyone to test their suggestions.

7

Hi Dave,

Any pointers on the latter part ?

If user wants to check for ABA..ABA ..,how to ensure that the 2nd assertion of A doesn’t result in start of 2nd attempt ( due to antecedent match ) ?

2nd attempt should start only on 3rd assertion of A i.e 3rd $rose(A)