Stability signal when another signals is asserted

UVM
,
1

Hi.

I want to code an assert to validate if signal data remains stable while the CS signal is enabled. The data signal could change its state just in the posedge or negegde of the CS signal, in these cases, the assertion must pass anyways.

What is the best way to do that?

Thanks!

2

In reply to kevinvig:

Is there another clock involved for sampling stability, or is this all asynchronous? And if asynchronous, what do you mean by “just in the posedge or negegde of the CS signal”. There would only be before or after.

3

Hi Dave.

It is all synchronous, the signals change just in the clk posedge at the same time.

4

In reply to kevinvig:

Hi.
I want to code an assert to validate if signal data remains stable while the CS signal is enabled. The data signal could change its state just in the posedge or negegde of the CS signal, in these cases, the assertion must pass anyways.

You have to specify your problem more accurately. How long is your CS signal and are you really sure data are changing on the edges of CS?

5

In reply to chr_sue:

Hi,

The CS signal could be from 4 cycles to practically any number of cycles. I need to be sure the ‘din’, and ‘dout’ signals remain stable while the CS signal is asserted., Also consider that Din and Dout signal could change just when CS goes high or low (in this case the assertion must pass). The CS, din, and dout signals are all synchronous.

I have this option, but I am not sure if it is the best way to do it:

 
property dout_stable_property;
    @(posedge clk) $rose(
        cs
    ) |-> ##1 ($stable(
        dout
    ) throughout cs);
  endproperty

Thanks in advance.

6

In reply to kevinvig:

That works. Also

property dout_stable_property;
    @(posedge clk) $rose(
        cs
    ) |-> ##1 ($stable(
        dout
    ) until $fell(
        cs);
  endproperty
7

In reply to dave_59:

Hi Dave ,
Please correct me if my understanding is incorrect .
Shouldn’t we use ’ until_with ’ instead ? i.e alternative for ’ throughout ’ operator is ’ until_with ’ .
For ’ until ’ operator the LHS need not be true when the RHS is true whereas using ’ until_with ’ the LHS needs to be True when RHS is True .

8

In reply to Have_A_Doubt:

I am not using the same RHS. Try it.

9

In reply to dave_59:

Thanks Dave ,


 property dout_stable_property;
    @(posedge clk) $rose( cs ) |=> ( $stable( dout ) throughout cs );
  endproperty

This would cause assertion to pass as soon as consequent is evaluated , whereas


 property dout_stable_property;
    @(posedge clk) $rose( cs ) |=> ( $stable( dout ) until $fell( cs ) );
  endproperty

checks that ’ dout ’ is stable till the clock edge that ’ cs ’ goes low .

10

In reply to Have_A_Doubt:

Hi,

I have a doubt, why do you say this case will pass as soon as the consequent is evaluated?

 property dout_stable_property;
    @(posedge clk) $rose( cs ) |=> ( $stable( dout ) throughout cs );
  endproperty

I understand this checks that ’ dout ’ is stable till the clock edge that ’ cs ’ goes low. Just like with the “until”, like Dave mentioned before. Am I missing something?

11

In reply to kevinvig:

will pass as soon as the consequent is evaluated

This is assuming $stable( dout ) is True i.e signal ’ dout ’ doesn’t change between 2 clock event.

Check the following link : edalink .

Via throughout operator the consequent is evaluated at T:25 .
As signal ’ dout ’ has same value at clock event T:15 and T:25 , $stable( dout ) is True .
Hence assertion passes at T:25

Using until operator although the consequent starts evaluation at T:25 , the assertion passes at T:45 .
Now $stable( dout ) needs to be True till signal ’ cs ’ is de-asserted .

My guess is your intent might the latter one .

12

In reply to Have_A_Doubt:

Thank you so much, very clear.

I don’t know why my simulator doesn’t recognize the “until” keyword, could be a UVM version problem? Is there another alternative to write this in a clear way?

Thanks!

13

In reply to kevinvig:

I don’t know why my simulator doesn’t recognize the “until” keyword

Seems like a tool limitation . 3 out of the 4 tools on edaplayground support ’ until ’ operator .

Is there another alternative to write this in a clear way?


property dout_stable_property;
    @(posedge clk) $rose( cs ) |=> ( $stable( dout ) throughout ( $fell( cs ) ) [->1] );
 endproperty

This is supported on all 4 tools available on edaplayground .

14

In reply to Have_A_Doubt:

I understand. Very clear, thank you so much for your explanation.

Regards!

15

In reply to Have_A_Doubt:

I notice if you do:

property dout_stable_property;
    @(posedge clk) $rose( cs ) |=> ( $stable( dout ) throughout ( $fell( cs ) ) [->1] );
 endproperty

The property will fail if the dout signal changes precisely at the falling of the cs signal.

What is the best way to do that without the until operator?

Thanks!

16

In reply to Have_A_Doubt:

here is an alternative:

property dout_stable_throughout_fell_property;
    @(posedge clk) $rose( cs ) |=> ( $stable( dout)[*1:$] ##1 !cs);
 endproperty

I tested and it works