SVA- How we can write property such that it will check the value which is getting generated either by increments or decrements as below

SystemVerilog
,
1

There are below Input signals- WE,WR,RD.
and output signal - USED
When WE(Write Empty) = 1, WR(Write Request) = 1, RD(READ REQUEST) = 0 , USED == 0. on first clock cycle, // Need to start Assertion on this
then till `depth-1 cycle , WE=0,WR=1,RD=0, //Need to check in entire depth-1 cycle.
then finally on N cycle, USED should be equal to depth. //Need to check on the Nth Cycle
We need to check on the N Cycle.

But if in between WR = 0 and RD =1 then Depth should increase by 1 for every such clock.

Any lead …

2

In reply to ADITYA ABHISHEK:

see reply in
https://verificationacademy.com/forums/systemverilog/sva-how-we-can-write-property-such-it-will-check-value-which-getting-generated-either-increments-or-decrements-below