Formal SVA: Ensure primary input is low out of reset?

SystemVerilog
,
1

Hi, in formal I am writing assertions for a simple valid/data interface. On the first cycle of valid, data must be 0 and increment continuously for each consecutive cycle of valid.

However, the tool can use valid as a formal input, and may have it high out of reset (X->1). I have tried various assumptions but this feels like it should be easy to do. If valid is high out of reset, that is fine, but the data must be 0. Or if there is a concise way of ensure it is always low

property low_in_reset;
      @(posedge clk)  !reset |-> !valid ;
endproperty;
2

Your requirements are not clear. Is this what you need?

//  Inputs:  valid,  data, clk, reset_n (active low)
 intital 
        asm_1: assume property(@ (posedge clk) reset_n==0[->1] |-> 
                                    data==0 && valid==0[*1:$] intersect reset_n[->1] );

I address a similar issue in my
SVA paper: (intersect) vs (throughout, until, until_with, within)
*** MUST READ FOR REAL SVA USERS!!! ***
It addresses misunderstandings in the use of these operators, often caused by inherent misconceptions arising from their English-like syntax.

3

Thanks Ben, although I tried and it doesn’t work, I think my requirement was too complicated.

I guess the main requirement is how to ensure a primary input is low in the cycle after reset in formal? Using resetn in the antecedent doesn’t seem to produce results I would expect.

4

Formal tools often have a boundary case issue on the first cycle after reset, since reset is handled separately by a simulation engine. The easiest solution may be to provide a reset value of 0 for the valid and data inputs.vs (throughout, until, until_with, within)

Inputs:  valid,  data, clk, reset_n (active low)
    asm_1: assume property(@ (posedge clk) reset_n==0 |-> 
                                    data==0 && valid==0);