Help needed for an assertion question

SystemVerilog
,
1

Hi, I am trying to write an assertion for the following question.

A high for 5 cycles and B high after 4 non-continuous highs of A and finally both A and B are high.
Can you please help me write an assertion for this.

2

In reply to sruthikrapa:

If there is a clock for this particular check simple way to write this one. 

property abcheck ;
@(posedge clk) a |-> a[->4] ##0 b ##1 a ##0 b;
endproperty
3

In reply to sruthikrapa:

sequence s1;
A[=4];
endsequence

property p1;
@(posedge clk) s1 |=> [0:$] (A&&B == 1) ##1 (A||B == 0) ;
endproperty

Is this what you needed?

4

Thank you yourcheers and kddholak for your answers.
They are useful.

-Sruthi.

5

I was asked this assertion in an interview,
Property ppt;
@(posedge clk) $rose(a)|->a[->4]|->b##1$stable(a)&&b;
endproperty.
Can anyone please validate my answer, i am a beginner stage in assertions.
That would mean a lot

6

There can be only 1 implication poperator in a property. You have 2 ones.

7

A few things ::
(1) Please reiterate the question. The one at the top is ambiguous.
Give a few examples of passing and failing scenarios
(2) B high after 4 non-continuous highs of A
It specifically says 4 non-continuous . A[->4] matches when A is true 4 continuous times or when A is true 4 non-continuous times
(3) A high for 5 cycles and B high after 4 non-continuous highs of A.
Out of the 5 cycles , A must be high 4 non-continuous times before b is high ?
Is B high on the same 4 non-consecutive occurrence of A or the next clock ?
(4) finally both A and B are high.
So A is high for the 5th time whereas B is high for the 1st time ?

1 Like
8

@chr_sue
Please clarify, Will this work?

1’b1 |-> ( A[->4] ##[0:$] (A&&B) ##1 ((A||B)==0) ) ;

9

thank you for response ,will definitely look into that.

10

thank you for response sir,this would help me learn more about assertions more.